TY - CONF AB - We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties. AU - Alur, Rajeev AU - Courcoubetis, Costas AU - Henzinger, Thomas A AU - Ho, Pei ED - Grossman, Robert ED - Nerode, Anil ED - Ravn, Anders ED - Rischel, Hans ID - 4618 T2 - Hybrid Systems TI - Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems VL - 736 ER - TY - CONF AB - We present a model checking procedure and its implementation for the automatic verification of embedded systems. Systems are represented by hybrid automata - machines with finite control and real-valued variables modeling continuous environment parameters such as time, pressure, and temperature. System properties are specified in a real-time temporal logic and verified by symbolic computation. The verification procedure, implemented in Mathematica, is used to prove digital controllers and distributed algorithms correct. The verifier checks safety, liveness, time-bounded, and duration properties of hybrid automata AU - Alur, Rajeev AU - Henzinger, Thomas A AU - Ho, Pei ID - 4616 SN - 0-8186-4480-X T2 - 1993 Proceedings Real-Time Systems Symposium TI - Automatic symbolic verification of embedded systems ER - TY - CONF AB - We present a verification algorithm for duration properties of finite-state real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated time during which certain state predicates hold. We formalize the concept of durations by introducing duration measures for (dense-time) timed automata. Given a timed automaton with a duration measure, a start and a target state, and a duration constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the start state to the target state such that the accumulated duration along the run satisfies the constraint. Our main result is a novel decision procedure for solving the duration-bounded reachability problem. We also prove that the problem is PSPACE-complete and demonstrate how the solution can be used to verify interesting duration properties of real-time systems. AU - Alur, Rajeev AU - Courcoubetis, Costas AU - Henzinger, Thomas A ID - 4620 T2 - 5th International Conference on Computer Aided Verification TI - Computing accumulated delays in real-time systems VL - 697 ER - TY - CONF AB - Traditional approaches to the algorithmic verification of real-time systems are limited to checking program correctness with respect to concrete timing properties (e.g., "message delivery within 10 milliseconds"). We address the more realistic and more ambitious problem of deriving symbolic constraints on the timing properties required of real-time systems (e.g., "message delivery within the time it takes to execute two assignment statements"). To model this problem, we introduce parametric timed automata -- finite-state machines whose transitions are constrained with parametric timing requirements. The emptiness question for parametric timed automata is central to the verification problem. On the negative side, we show that in general this question is undecidable. On the positive side, we provide algorithms for checking the emptiness of restricted classes of parametric timed automata. The practical relevance of these classes is illustrated with several verification examples. There remains a gap between the automata classes for which we know that emptiness is decidable and undecidable, respectively, and this gap is related to various hard and open problems of logic and automata theory. AU - Alur, Rajeev AU - Henzinger, Thomas A AU - Vardi, Moshe ID - 4619 T2 - Proceedings of the 25th annual ACM symposium on Theory of Computing TI - Parametric real-time reasoning ER -