Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification

Luca de Alfaro, Arjun Kapur, Zohar Manna,

We present a methodology for the verification of temporal properties of hybrid systems. The methodology is based on the deductive transformation of hybrid diagrams, which represent the system and its properties, and which can be algorithmically checked against the specification. This check either gives a positive answer to the verification problem, or provides guidance for the further transformation of the diagrams. The resulting methodology is complete for quantifier-free linear-time temporal logic.

In Proc. of 14th Symposium on Theoretical Aspects of Computer Science, vol. 1200 of Lecture Notes in Computer Science, pp. 153-164, Springer Verlag, Feb. 1997.

Postscript, PDF. © 1997, Springer Verlag.

Last modified: Thu Mar 29 16:47:34 PST 2001