DOI:
Abstract:
Verification problems for hybrid systems can be classified on the model of hybrid automata. In particular, linear-time specifications can be verified on rectangular hybrid automata, which induce finite language quotients; universal branching-time specifications can be verified on 2D rectangular automata, which induce finite similarity quotients; and all branching-time specifications can be verified on singular automata, which induce finite bisimilarity quotients. (For nonrectangular automata, even invariance is undecidable.) We offer a similar classification of control problems for hybrid systems.