TY - GEN
T1 - Deciding concurrent planar monotonic linear hybrid systems
AU - Prabhakar, Pavithra
AU - Roohi, Nima
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - Decidability results for hybrid automata often exploit subtle properties about dimensionality (number of continuous variables), and interaction between discrete transitions and continuous trajectories of variables. Thus, the decidability results often do not carry over to parallel compositions of hybrid automata, even when there is no communication other than the implicit synchronization of time. In this paper, we show that the reachability problem for concurrently running planar, monotonic hybrid automata is decidable. Planar, monotonic hybrid automata are a special class of linear hybrid automata with only two variables, whose flows in all states are simultaneously monotonic along some direction in the plane. The reachability problem is known to be decidable for this class. Our concurrently running automata synchronize with respect to a global clock, and through labeled discrete transitions. The proof of decidability hinges on a new observation that the timed trace language of a planar monotonic automaton can be recognized by a timed automaton, and the decidability result follows from the decidability of composition of timed automata. Our results identify a new decidable subclass of multirate hybrid automata.
AB - Decidability results for hybrid automata often exploit subtle properties about dimensionality (number of continuous variables), and interaction between discrete transitions and continuous trajectories of variables. Thus, the decidability results often do not carry over to parallel compositions of hybrid automata, even when there is no communication other than the implicit synchronization of time. In this paper, we show that the reachability problem for concurrently running planar, monotonic hybrid automata is decidable. Planar, monotonic hybrid automata are a special class of linear hybrid automata with only two variables, whose flows in all states are simultaneously monotonic along some direction in the plane. The reachability problem is known to be decidable for this class. Our concurrently running automata synchronize with respect to a global clock, and through labeled discrete transitions. The proof of decidability hinges on a new observation that the timed trace language of a planar monotonic automaton can be recognized by a timed automaton, and the decidability result follows from the decidability of composition of timed automata. Our results identify a new decidable subclass of multirate hybrid automata.
UR - http://www.scopus.com/inward/record.url?scp=84944685228&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84944685228&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-22975-1_17
DO - 10.1007/978-3-319-22975-1_17
M3 - Conference contribution
AN - SCOPUS:84944685228
SN - 9783319229744
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 256
EP - 269
BT - Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Proceedings
A2 - Sankaranarayanan, Sriram
A2 - Vicario, Enrico
PB - Springer
T2 - 13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015
Y2 - 2 September 2015 through 4 September 2015
ER -