Continuous Verification by Discrete Reasoning,
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1994
- Accession Number
- ADA324421
Entities
People
- Luca De Alfaro
- Zohar Manna
Organizations
- Stanford University