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 -
TY - JOUR
AB - A version of the one-dimensional Rayleigh gas is considered: a point particle of mass M (molecule), confined to the unit interval [0,1], is surrounded by an infinite ideal gas of point particles of mass 1 (atoms). The molecule interacts with the atoms and with the walls via elastic collision. Central limit theorems are proved for a wide class of additive functionals of this system (e.g. the number of collisions with the walls and the total length of the molecular path).
AU - László Erdös
AU - Tuyen, Dao Quang
ID - 2722
IS - 3
JF - Communications in Mathematical Physics
TI - Central limit theorems for the one-dimensional Rayleigh gas with semipermeable barriers
VL - 143
ER -
TY - JOUR
AB - The effects of ultra-low (10(-18)-10(-14) M) doses (ULD) of biologically active substances have been reviewed in terms of common regularities of ULD effects and peculiarities of action of various groups of compounds. The most common and at the same time paradoxical regularities of ULD action are bi- or polymodal patterns of dose dependence, absence or presence of an inverse effect at higher doses, and instability of ULD effect. Possible mechanisms of ULD action including the mechanism based on the adaptation theory are discussed.
AU - Leonid Sazanov
AU - Zaǐtsev, Sergei V
ID - 1945
IS - 10
JF - Biokhimiya
TI - Effect of superlow doses (10(-18)-10-(-14) M) of biologically active substances: general rules, features, and possible mechanisms
VL - 57
ER -