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.
The research was supported in part by the National Science Foundation under grant CCR-9527927, by the Defense Advanced Research Projects Agency under contract NAG2-892, by ARO under grant DAAH04-95-1-0317, and by ARO under the MURI grant DAAH04-96-1-0341.