1995 | Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin Varaiya
The paper "What's Decidable about Hybrid Automata?" by A. Puri, P. Varaiya, and J. Sifakis explores the decidability of reachability problems for hybrid automata, which model systems with both digital and analog components. The authors identify the precise boundary between decidability and undecidability of these problems.
On the positive side, they present an optimal PSPACE algorithm for the reachability problem for initialized rectangular automata, where all analog variables follow piecewise-linear trajectories and are reinitialized when the trajectory changes. This algorithm is based on translating an initialized rectangular automaton into a timed automaton that defines the same timed language, ensuring the termination of symbolic procedures for verification.
On the negative side, the authors show that several slight generalizations of initialized rectangular automata lead to undecidable reachability problems. Specifically, they prove that the reachability problem is undecidable for timed automata with a single stopwatch, and for rectangular automata with more general triangular activities.
The paper also discusses the decidability and undecidability results in the context of previous work, providing a systematic identification of the boundary between decidability and undecidability. It includes detailed proofs and examples to support the main results.The paper "What's Decidable about Hybrid Automata?" by A. Puri, P. Varaiya, and J. Sifakis explores the decidability of reachability problems for hybrid automata, which model systems with both digital and analog components. The authors identify the precise boundary between decidability and undecidability of these problems.
On the positive side, they present an optimal PSPACE algorithm for the reachability problem for initialized rectangular automata, where all analog variables follow piecewise-linear trajectories and are reinitialized when the trajectory changes. This algorithm is based on translating an initialized rectangular automaton into a timed automaton that defines the same timed language, ensuring the termination of symbolic procedures for verification.
On the negative side, the authors show that several slight generalizations of initialized rectangular automata lead to undecidable reachability problems. Specifically, they prove that the reachability problem is undecidable for timed automata with a single stopwatch, and for rectangular automata with more general triangular activities.
The paper also discusses the decidability and undecidability results in the context of previous work, providing a systematic identification of the boundary between decidability and undecidability. It includes detailed proofs and examples to support the main results.