## Symbolic Model Checking for Rectangular Hybrid Systems

*
Thomas A. Henzinger
and Rupak Majumdar*

An important case of hybrid systems are the rectangular automata. First,
rectangular dynamics can naturally and arbitrarily closely approximate more
general, nonlinear dynamics. Second, rectangular automata are the most
general type of hybrid systems for which model checking --in particular, LTL
model checking-- is decidable. However, on one hand, the original proofs of
decidability did not suggest practical algorithms and, on the other hand,
practical symbolic model-checking procedures --such as those implemented in
HyTech-- were not known to terminate on rectangular automata. We remedy this
unsatisfactory situation: we present a symbolic method for LTL model checking
which can be performed by HyTech and is guaranteed to terminate on all
rectangular automata. We do so by proving that our method for symbolic LTL
model checking terminates on an infinite-state transition system if the
trace-equivalence relation of the system has finite index, which is the case
for all rectangular automata.

*Proceedings of the
Sixth International Conference on Tools and Algorithms for the
Construction and Analysis of Systems*
(TACAS),
Lecture Notes in Computer Science 1785,
Springer, 2000, pp. 142-156.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2000 Springer.