Report Number: CS-TR-97-1594
Institution: Stanford University, Department of Computer Science
Title: Interval and Point-Based Approaches to Hybrid System Verification
Author: Kapur, Arjun
Date: September 1997
Abstract: Hybrid systems are real-time systems consisting of both continuous and discrete components. This thesis presents deductive and diagrammatic methodologies for proving point-based and interval-based properties of hybrid systems, where the hybrid system is modeled in either a sampling semantics or a continuous semantics. Under a sampling semantics the behavior of the system consists of a discrete number of system snapshots, where each snapshot records the state of the system at a particular moment in time. Under a continuous semantics, the system behavior is given by a function mapping each point in time to a system state. Two continuous semantics are studied: a continuous interval semantics, where at any given point in time the system is in a unique state, and a super-dense semantics, where no such requirement is needed. We use Linear-time Temporal Logic for expressing properties under either a sampling semantics or a super-dense semantics, and we introduce Hybrid Temporal Logic for expressing properties under a continuous interval semantics. Linear-time Temporal Logic is useful for expressing point-based properties, whose validity is dependent on individual states, while Hybrid Temporal Logic is useful for expressing both interval-based properties, whose validity is dependent on intervals of time, and point-based properties. Finally, two different verification methodologies are presented: a diagrammatic approach for verifying properties specified in Linear-time Temporal Logic, and a deductive approach for verifying properties specified in Hybrid Temporal Logic.
http://i.stanford.edu/pub/cstr/reports/cs/tr/97/1594/CS-TR-97-1594.pdf