Now showing items 15-22 of 22

    • 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 ...