Abstract
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 multi-rate hybrid automata.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS 138(1), 3–34 (1995)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science 138(1), 35–65 (1995)
Asarin, E., Schneider, G., Yovine, S.: Algorithmic analysis of polygonal hybrid systems. Part I: Reachability. TCS 379(1–2), 231–265 (2007)
Casagrande, A., Corvaja, P., Piazza, C., Mishra, B.: Decidable compositions of o-minimal automata. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 274–288. Springer, Heidelberg (2008)
Henzinger, T.A.: The theory of hybrid automata. In: Proceeding of IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences 57(1), 373–382 (1995)
Lafferriere, G., Pappas, G., Sastry, S.: o-minimal hybrid systems. MCSS 13, 1–21 (2000)
Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296–309. Springer, Heidelberg (2000)
Mysore, V., Pnueli, A.: Refining the undecidability frontier of hybrid automata. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 261–272. Springer, Heidelberg (2005)
Prabhakar, P., Vladimerou, V., Viswanathan, M., Dullerud, G.: A decidable class of planar linear hybrid systems. Theoretical Computer Science 574, 1–17 (2015)
L. van den Dries: Tame Topology and O-minimal Structures. Cambridge UnivesityPress (1998)
Vladimerou, V., Prabhakar, P., Viswanathan, M., Dullerud, G.E.: STORMED Hybrid Systems. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 136–147. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Prabhakar, P., Roohi, N., Viswanathan, M. (2015). Deciding Concurrent Planar Monotonic Linear Hybrid Systems. In: Sankaranarayanan, S., Vicario, E. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2015. Lecture Notes in Computer Science(), vol 9268. Springer, Cham. https://doi.org/10.1007/978-3-319-22975-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-22975-1_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22974-4
Online ISBN: 978-3-319-22975-1
eBook Packages: Computer ScienceComputer Science (R0)