TY - GEN
AU - Nicholas Barton
AU - Goldman, Nick G
ID - 4306
T2 - Nature
TI - Genetics and geography
VL - 357
ER -
TY - CHAP
AU - Nicholas Barton
ED - Stenseth, Nils C
ED - Lidicker, William Z
ID - 4307
T2 - Animal dispersal: small mammals as a model
TI - The genetic consequences of dispersal
ER -
TY - JOUR
AU - Nicholas Barton
ID - 4308
IS - 2
JF - Evolution; International Journal of Organic Evolution
TI - On the spread of new gene combinations in the third phase of Wright's shifting balance
VL - 46
ER -
TY - CONF
AU - Thomas Henzinger
AU - Manna, Zohar
AU - Pnueli,Amir
ID - 4504
TI - What good are digital clocks?
VL - 623
ER -
TY - CONF
AB - We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space.
For this purpose, we introduce a mu-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed mu-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs--those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
AU - Thomas Henzinger
AU - Nicollin, Xavier
AU - Sifakis, Joseph
AU - Yovine, Sergio
ID - 4505
TI - Symbolic model checking for real-time systems
ER -
TY - CHAP
AB - We incorporate time into an interleaving model of concurrency. In timed transition systems, the qualitative fairness requirements of traditional transition system are replaced (and superseded) by quantitative lower-bound and upperbound timing constraints on transitions. The purpose of this paper is to explore the scope of applicability for the abstract model of timed transition systems. We demonstrate that the model can represent a wide variety of phenomena that routinely occur in conjunction with the timed execution of concurrent processes. Our treatment covers both processes that are executed in parallel on separate processors and communicate either through shared variables or by message passing, and processes that time-share a limited number of processors under a given scheduling policy. Often it is this scheduling policy that determines if a system meets its real-time requirements. Thus we explicitly address such questions as time-outs, interrupts, static and dynamic priorities.
AU - Thomas Henzinger
AU - Manna, Zohar
AU - Pnueli,Amir
ID - 4507
T2 - Real Time: Theory in Practice
TI - Timed transition systems
VL - 600
ER -
TY - JOUR
AB - It has been observed repeatedly that the standard safety-liveness classification for properties of reactive systems does not fit for real-time properties. This is because the implicit “liveliness” of time shifts the spectrum towards the safety side. While, for example, response—that “something good” will happen eventually—is a classical liveness property, bounded response—that “something good” will happen soon, within a certain amount of time—has many characteristics of safety. We account for this phenomenon formally by defining safety and liveness relative to a given condition, such as the progress of time.
AU - Thomas Henzinger
ID - 4517
IS - 3
JF - Information Processing Letters
TI - Sooner Is Safer Than Later
VL - 43
ER -
TY - CHAP
AB - We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification.
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4593
T2 - Real Time: Theory in Practice
TI - Logics and models of real time: A survey
VL - 600
ER -
TY - CONF
AB - The authors introduce two-way timed automata-timed automata that can move back and forth while reading a timed word. Two-wayness in its unrestricted form leads, like nondeterminism, to the undecidability of language inclusion. However, if they restrict the number of times an input symbol may be revisited, then two-wayness is both harmless and desirable. The authors show that the resulting class of bounded two-way deterministic timed automata is closed under all boolean operations, has decidable (PSPACE-complete) emptiness and inclusion problems, and subsumes all decidable real-time logics we know. They obtain a strict hierarchy of real-time properties: deterministic timed automata can accept more languages as the bound on the number of times an input symbol may be revisited is increased. This hierarchy is also enforced by the number of alternations between past and future operators in temporal logic. The combination of the results leads to a decision procedure for a real-time logic with past operators
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4594
TI - Back to the future: Towards a theory of timed regular languages
ER -
TY - JOUR
AU - László Erdös
ID - 2714
IS - 1-2
JF - Acta Mathematica Hungarica
TI - On some problems of P. Turán concerning power sums of complex numbers
VL - 59
ER -