Proceedings:
Hybrid Systems and AI: Modeling Analysis and Control of Discrete Plus Continuous Systems
Volume
Issue:
Papers from the 1999 AAAI Spring Symposium
Track:
Contents
Downloads:
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.
Spring
Papers from the 1999 AAAI Spring Symposium