Hybrid Games

T. Henzinger

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.