Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Proving Safety Properties of Hybrid Systems
Authors: Kapur, Arjun
Henzinger, Thomas A.
Manna, Zohar
Pnueli, Amir
Keywords: computer science
technical report
Issue Date: Oct-1994
Publisher: Cornell University
Abstract: We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems, the specification language of Hybrid Temporal Logic (HTL), the graphical system description language of Hybrid Automata, and a proof system for verifying that hybrid automata satisfy their HTL specifications. The novelty of the approach lies in the continuous-time logic, which allows specification of both point-based and interval-based properties (i.e., properties which describe changes over an interval) and provides direct references to derivatives of variables, and in the proof system that supports verification of point-based and interval-based properties. The proof rules demonstrate that sound and convenient induction rules can be established for continuous-time logics. The proof rules are illustrated on several examples.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
94-1459.pdf287.13 kBAdobe PDFView/Open
94-1459.ps281.02 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us