Abstract
Reachability becomes undecidable in hybrid automata (HA) that can simulate a Turing (TM) or Minsky (MM) machine. Asarin and Schneider have shown that, between the decidable 2-dim Piecewise Constant Derivative (PCD) class and the undecidable 3-dim PCD class, there lies the “open” class 2-dim Hierarchical PCD (HPCD). This class was shown to be equivalent to the class of 1-dim Piecewise Affine Maps (PAM). In this paper, we first explore 2-dim HPCD’s proximity to decidability, by showing that they are equivalent to 2-dim PCDs with translational resets, and to HPCDs without resets. A hierarchy of intermediates also equivalent to the HPCD class is presented, revealing semblance to timed and initialized rectangular automata. We then explore the proximity to the undecidability frontier. We show that 2-dim HPCDs with zeno executions or integer-checks can simulate the 2-counter MM. We conclude by retreating HPCDs as PAMs, to derive a simple over-approximating algorithm for reachability. This also defines a decidable subclass 1-dim Onto PAM (oPAM). The novel non-trivial transformation of 2-dim HPCDs into “almost decidable” systems, is likely to pave the way for approximate reachability algorithms, and the characterization of decidable subclasses. It is hoped that these ideas eventually coalesce into a complete understanding of the reachability problem for the class 2-dim HPCD (1-dim PAM).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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. Theoretical Computer Science 138, 3–34 (1995)
Alur, R., Dill, D.L.: A Theory of Timed Automata. TCS 126, 183–235 (1994)
Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science 138, 35–65 (1995)
Asarin, E., Schneider, G.: Widening the boundary between decidable and undecidable hybrid systems. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 193–208. Springer, Heidelberg (2002)
Asarin, E., Schneider, G., Yovine, S.: On the decidability of the reachability problem for planar differential inclusions. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 89–104. Springer, Heidelberg (2001)
Berard, B., Dufourd, C.: Timed automata and additive clock constraints. Information Processing Letter 75(1-2), 1–7 (2000)
Henzinger, T., Kopke, P.W., Puri, A., Varaiya, P.: What’s Decidable about Hybrid Automata. In: Symposium on the Theory of Computing (STOC), pp. 373–382 (1995)
Henzinger, T.A., Sastry, S.: Hybrid Systems-Computation and Control. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, Springer, Heidelberg (1998)
Koiran, P.: My favourte problems (1999), http://perso.ens-lyon.fr/pascal.koiran/problems.html
Lafferiere, G., Pappas, G.J., Sastry, S.: O-minimal Hybrid Systems. Mathematics of Control, Signals, and Systems 13(1), 1–21 (2000)
Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001)
Maler, O., Pnueli, A.: Reachability analysis of planar multi-linear systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, Springer, Heidelberg (1993)
Minsky, M.L.: Recursive unsolvability of post’s problem of tag and other topics in theory of turing machines. Ann. of Math. 74, 437–455 (1961)
Mysore, V., Mishra, B.: Algorithmic Algebraic Model Checking III: Approximate Methods. Infinity (2005)
Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic Algebraic Model Checking I: The Case of Biochemical Systems and their Reachability Analysis. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 5–19. Springer, Heidelberg (2005)
Puri, A., Varaiya, P.: Decidebility of hybrid systems with rectangular differential inclusions. Computer Aided Verification, pp. 95–104 (1994)
Schneider, G.: Algorithmic Analysis of Polygonal Hybrid Systems. Ph.D. thesis. VERIMAG - UJF, Grenoble, France (2002)
Tabuada, P., Pappas, G.J.: Model checking ltl over controllable linear systems is decidable. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 498–513. Springer, Heidelberg (2003)
Teschl, G.: Ordinary differential equations and dynamical systems (2004), Lecture Notes from http://www.mat.univie.ac.at/gerald/ftp/book-ode/index.html
Turing, A.: On computable numbers, with an application to the entscheidungs problem. Proceedings of the London Mathematical Society 2(42), 230–265 (1936)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mysore, V., Pnueli, A. (2005). Refining the Undecidability Frontier of Hybrid Automata. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_21
Download citation
DOI: https://doi.org/10.1007/11590156_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30495-1
Online ISBN: 978-3-540-32419-5
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.
