Now showing items 3-22 of 22

    • The Benefits of Relaxing Punctuality 

      Alur, Rajeev; Feder, Tomas; Henzinger, Thomas A. (Cornell University, 1994-09)
      Abstract
    • A Determinizable Class of Timed Automata 

      Alur, Rajeev; Fix, Limor; Henzinger, Thomas A. (Cornell University, 1995-03)
      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 ...
    • The Expressive Power of Clocks 

      Henzinger, Thomas A.; Kopke, Peter W.; Wong-Toi, Howard (Cornell University, 1995-04)
      We investigate the expressive power of timing restrictions on labeled transition systems. In particular, we show how constraints on clock variables together with a uniform liveness condition---the divergence of time---can ...
    • Hybrid Automata with Finite Mutual Simulations 

      Henzinger, Thomas A.; Kopke, Peter W. (Cornell University, 1995-03)
      Many decidability results for hybrid automata rely upon the finite region bisimulation of timed automata [AD94]. Rectangular automata do not have finite bisimulations [Hen95], yet have many decidable verification problems ...
    • Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems 

      Alur, Rajeev; Courcoubetis, Costas; Henzinger, Thomas A.; Ho, Pei-Hsin (Cornell University, 1993-05)
      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 ...
    • HyTech : The Cornell HYbrid TECHnology Tool 

      Henzinger, Thomas A.; Ho, Pei-Hsin (Cornell University, 1995-06)
      This paper is addressed to potential users of HyTech, the Cornell Hybrid Technology Tool, an automatic tool for analyzing hybrid systems. We review the formal technologies that have been incorporated into HyTech, and ...
    • Logics and Models of Real Time: A Survey 

      Alur, Rajeev; Henzinger, Thomas A. (Cornell University, 1992-01)
      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, ...
    • Model Checking Strategies for Linear Hybrid Systems 

      Henzinger, Thomas A.; Ho, Pei-Hsin (Cornell University, 1994-07)
      Linear hybrid systems are dynamical systems whose variables change both discretely and continuously along piecewise linear trajectories; they are useful for modeling digital real-time programs that are embedded in analog ...
    • Parametric Real-Time Reasoning 

      Alur, Rajeev; Henzinger, Thomas A. (Cornell University, 1993-05)
      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 ...
    • Proving Safety Properties of Hybrid Systems 

      Kapur, Arjun; Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir (Cornell University, 1994-10)
      We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems, the specification language of Hybrid ...
    • Real-Time System = Discrete System + Clock Variables 

      Alur, Rajeev; Henzinger, Thomas A. (Cornell University, 1994-01)
      How can we take a programming language off the shelf and upgrade it into a real-time programming language? Programs such as device drivers and plant controllers must explicitly refer and react to time. For this purpose, ...
    • A Really Temporal Logic 

      Alur, Rajeev; Henzinger, Thomas A. (Cornell University, 1992-11)
      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 ...
    • State Equivalences for Rectangular Hybrid Automata 

      Henzinger, Thomas A.; Kopke, Peter W. (Cornell University, 1996-07)
      Three natural equivalence relations on the infinite state space of a hybrid automaton are language equivalence, simulation equivalence, and bisimulation equivalence. When one of these equivalence relations has a finite ...
    • Symbolic Model Checking for Real-Time Systems 

      Henzinger, Thomas A.; Nicollin, Xavier; Sifakis, Joseph; Yovine, Sergio (Cornell University, 1994-01)
      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 ...
    • Temporal Proof Methodologies for Timed Transition Systems 

      Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir (Cornell University, 1993-03)
      We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of reactive systems. The abstract notion of timed ...
    • Timed Transition Systems 

      Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir (Cornell University, 1992-01)
      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 ...
    • Towards Refining Temporal Specifications into Hybrid Systems 

      Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir (Cornell University, 1993-05)
      We propose a formal framework for designing hybrid systems by stepwise refinement. Starting with a specification in hybrid temporal logic, we make successively more transitions explicit until we obtain an executable system.
    • Undecidability Results for Hybrid Systems 

      Henzinger, Thomas A.; Kopke, Peter W. (Cornell University, 1995-02)
      We illuminate the boundary between decidability and undecidability for hybrid systems. Adding any of the following decorations to a timed automaton makes the reachability problem undecidable: 1. a single stopwatch with ...
    • Verification Methods for the Divergent Runs of Clock Systems 

      Henzinger, Thomas A.; Kopke, Peter W. (Cornell University, 1995-02)
      We present a methodology for proving temporal properties of the divergent runs of reactive systems with real-valued clocks. A run diverges if time advances beyond any bound. Since the divergent runs of a system may ...
    • What's Decidable About Hybrid Automata? 

      Henzinger, Thomas A.; Kopke, Peter W.; Puri, Anuj; Varaiya, Pravin (Cornell University, 1995-09)
      Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving ...