TY - JOUR
AB - We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4591
IS - 1
JF - Journal of the ACM
TI - A really temporal logic
VL - 41
ER -
TY - CONF
AB - We develop a theory of equivalences for timed systems. Two systems are equivalent iff external observers cannot observe differences in their behavior. The notion of equivalence depends, therefore, on the distinguishing power of the observers. The power of an observer to measure time results in untimed, clock, and timed equivalences: an untimed observer cannot measure the time difference between events; a clock observer uses a clock to measure time differences with finite precision; a timed observer is able to measure time differences with arbitrary precision.
We show that the distinguishing power of clock observers grows with the number of observers, and approaches, in the limit, the distinguishing power of a timed observer. More precisely, given any equivalence for untimed systems, two timed systems are k-clock congruent, for a nonnegative integer k, iff their compositions with every environment that uses k clocks are untimed equivalent. Both k-clock bisimulation congruence and k-clock trace congruence form strict decidable hierarchies that converge towards the corresponding timed equivalences. Moreover, k-clock bisimulation congruence and k-clock trace congruence provide an adequate and abstract semantics for branching-time and linear-time logics with k clocks.
Our results impact on the verification of timed systems in two ways. First, our decision procedure for k-clock bisimulation congruence leads to a new, symbolic, decision procedure for timed bisimilarity. Second, timed trace equivalence is known to be undecidable. If the number of environment clocks is bounded, however, then our decision procedure for k-clock trace congruence allows the verification of timed systems in a trace model.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
ID - 4614
TI - The observational power of clocks
VL - 836
ER -
TY - CONF
AB - We introduce the class of event- recording timed automata (ERA). An event-recording automaton contains, for every event a, a clock that records the time of the last occurrence of a. The class ERA is, on one hand, expressive enough to model (finite) timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the language inclusion problem is decidable for event-recording automata. We present a translation from timed transition systems to event-recording automata, which leads to an algorithm for checking if two timed transition systems have the same set of timed behaviors.
We also consider event-predicting timed automata (EPA), which contain clocks that predict the time of the next occurrence of an event. The class of event-clock automata (ECA), which contain both event-recording and event-predicting clocks, is a suitable specification language for real-time properties. We provide an algorithm for checking if a timed automaton meets a specification that is given as an event-clock automaton.
AU - Alur, Rajeev
AU - Fix, Limor
AU - Thomas Henzinger
ID - 4615
TI - A determinizable class of timed automata
VL - 818
ER -
TY - CONF
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
AU - Nicollin, Xavier
AU - Olivero,Alfredo
AU - Sifakis, Joseph
AU - Yovine, Sergio
ID - 4617
TI - The algorithmic analysis of hybrid systems
VL - 199
ER -
TY - JOUR
AB - The tra-1 gene is the terminal regulator in the sex determination pathway in C. elegans, directing all aspects of somatic sexual differentiation. Recessive loss-of-function (lf) mutations in tra-1 masculinize XX animals (normally somatically female), while dominant gain-of-function mutations feminize XO animals (normally male). Most tra-1 (lf) mutations can be fitted into a simple allelic series of somatic masculinization, but a small number of lf alleles do not fit into this series. Here we show that three of these mutations are associated with DNA rearrangements 5' to the coding region. One allele is an inversion that may be subject to a position effect. We also report the isolation of a new class of tra-1 alleles that are responsive to mutations in the smg system of RNA surveillance. We show that two of these express RNAs of aberrant size. We suggest that the smg-sensitive mutations may identify a carboxy-terminal domain required for negative regulation of tra-1 activity.
AU - Zarkower, David
AU - de Bono, Mario
AU - Aronoff, Rachel
AU - Hodgkin, Jonathan
ID - 6167
IS - 3
JF - Developmental Genetics
SN - 0192-253X
TI - Regulatory rearrangements and smg-sensitive allels of the C. elegans sex-determining gene tra-1
VL - 15
ER -