Proving safety properties of hybrid systems

We propose a methodology for the speci cation, veri cation, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems (cptss), the speci cation 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 speci cations. The novelty of the approach lies in the continuous-time logic, which allows speci cation 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 veri cation 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.