What's Decidable about Hybrid Automata?

What's Decidable about Hybrid Automata?

© 1995 ACM | Thomas A. Henzinger², Peter W. Kopke², Anuj Puri³, Pravin Varaiya³
The paper investigates the decidability of the reachability problem for hybrid automata, which model systems with both digital and analog components. It identifies the boundary between decidability and undecidability for hybrid automata. On the positive side, it presents an optimal PSPACE algorithm for the reachability problem for initialized rectangular automata, where analog variables follow piecewise-linear envelopes and are reinitialized when the envelope changes. This algorithm translates initialized rectangular automata into timed automata, enabling efficient verification. On the negative side, it shows that several generalizations of initialized rectangular automata lead to undecidable reachability problems, including timed automata with a single stopwatch. The paper also discusses the implications of these results for the broader class of hybrid automata, highlighting the importance of restrictions on variable dynamics and transitions. It provides a systematic analysis of the decidability and undecidability of the reachability problem for various types of hybrid automata, including those with triangular activities and generalized update functions. The results demonstrate that while certain restricted classes of hybrid automata are decidable, more general classes are undecidable, emphasizing the role of structural constraints in determining the complexity of verification problems.The paper investigates the decidability of the reachability problem for hybrid automata, which model systems with both digital and analog components. It identifies the boundary between decidability and undecidability for hybrid automata. On the positive side, it presents an optimal PSPACE algorithm for the reachability problem for initialized rectangular automata, where analog variables follow piecewise-linear envelopes and are reinitialized when the envelope changes. This algorithm translates initialized rectangular automata into timed automata, enabling efficient verification. On the negative side, it shows that several generalizations of initialized rectangular automata lead to undecidable reachability problems, including timed automata with a single stopwatch. The paper also discusses the implications of these results for the broader class of hybrid automata, highlighting the importance of restrictions on variable dynamics and transitions. It provides a systematic analysis of the decidability and undecidability of the reachability problem for various types of hybrid automata, including those with triangular activities and generalized update functions. The results demonstrate that while certain restricted classes of hybrid automata are decidable, more general classes are undecidable, emphasizing the role of structural constraints in determining the complexity of verification problems.
Reach us at info@study.space
[slides and audio] What's decidable about hybrid automata%3F