Now showing items 1-7 of 7

    • 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 ...
    • 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 ...
    • The Theory of Rectangular Hybrid Automata 

      Kopke, Peter W. (Cornell University, 1996-08)
      A {\em hybrid automaton\/} consists of a finite automaton interacting with a dynamical system. Hybrid automata are used to model embedded controllers and other systems that consist of interacting discrete and continuous ...
    • 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 ...