TY - JOUR
AB - We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
ID - 4607
IS - 2
JF - Formal Methods in System Design
TI - Computing accumulated delays in real-time systems
VL - 11
ER -
TY - CONF
AB - State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.
AU - Alur, Rajeev
AU - Brayton, Robert K
AU - Thomas Henzinger
AU - Qadeer,Shaz
AU - Rajamani, Sriram K
ID - 4608
TI - Partial-order reduction in symbolic state-space exploration
VL - 1254
ER -
TY - CONF
AB - Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Kupferman, Orna
ID - 4609
TI - Alternating-time temporal logic
ER -
TY - JOUR
AB - Diamagnetism of the magnetic Schrödinger operator and paramagnetism of the Pauli operator are rigorously proven for nonhomogeneous magnetic fields in the large field, in the large temperature and in the semiclassical asymptotic regimes. New counterexamples are presented which show that neither dia-nor paramagnetism is true in a robust sense (without asymptotics). In particular, we demonstrate that the recent diamagnetic comparison result by Loss and Thaller [M. Loss and B. Thaller, Commun. Math. Phys. (submitted)] is essentially the best one can hope for.
AU - László Erdös
ID - 2727
IS - 3
JF - Journal of Mathematical Physics
TI - Dia- and paramagnetism for nonhomogeneous magnetic fields
VL - 38
ER -
TY - JOUR
AB - We give the leading order semiclassical asymptotics for the sum of the negative eigenvalues of the Pauli operator (in dimension two and three) with a strong non-homogeneous magnetic field. As in [LSY-II] for homogeneous field, this result can be used to prove that the magnetic Thomas-Fermi theory gives the leading order ground state energy of large atoms. We develop a new localization scheme well suited to the anisotropic character of the strong magnetic field. We also use the basic Lieb-Thirring estimate obtained in our companion paper [ES-I].
AU - László Erdös
AU - Solovej, Jan P
ID - 2729
IS - 3
JF - Communications in Mathematical Physics
TI - Semiclassical eigenvalue estimates for the Pauli operator with strong non-homogeneous magnetic fields, II. Leading order asymptotic estimates
VL - 188
ER -