Report Number: CS-TR-94-1524
Institution: Stanford University, Department of Computer Science
Title: Continuous Verification by Discrete Reasoning
Author: de Alfaro, Luca
Author: Manna, Z ohar
Date: September 1994
Abstract: Two semantics are commonly used for the behavior of real-time and hybrid systems: a discrete semantics, in which the temporal evolution is represented as a sequence of snapshots describing the state of the system at certain times, and a continuous semantics, in which the temporal evolution is represented by a series of time intervals, and therefore corresponds more closely to the physical reality. Powerful verification rules are known for temporal logic formulas based on the discrete semantics. This paper shows how to transfer the verification techniques of the discrete semantics to the continuous one. We show that if a temporal logic formula has the property of finite variability, its validity in the discrete semantics implies its validity in the continuous one. This leads to a verification method based on three components: verification rules for the discrete semantics, axioms about time, and some temporal reasoning to bring the results together. This approach enables the verification of properties of real-time and hybrid systems with respect to the continuous semantics.
http://i.stanford.edu/pub/cstr/reports/cs/tr/94/1524/CS-TR-94-1524.pdf