Now showing items 1-4 of 4

    • 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 ...
    • Hybrid Verification by Exploiting the Environment 

      Fix, Limor; Schneider, Fred B. (Cornell University, 1994-07)
      A method of verifying hybrid systems is given. Such systems involve state components whose values are changed by continuous (physical) processes. The verification method is based on proving that only those executions ...
    • Reasoning About Programs by Exploiting the Environment 

      Fix, Limor; Schneider, Fred B. (Cornell University, 1994-02)
      A method for making aspects of a computational model explicit in the formulas of a programming logic is given. The method is based on a new notion of environment -- an environment augments the state transitions defined ...
    • Verification of Temporal Properties 

      Fix, Limor; Grumberg, Orna (Cornell University, 1993-08)
      The paper presents a relatively complete deductive system for proving branching time temporal properties of reactive programs. No deductive system for verifying branching time temporal properties has been presented before. ...