Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints

  • Nima Roohi
  • Mahesh Viswanathan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8711)


Initialized hybrid automata with linear differential inclusions and rectangular constraints are hybrid automata where the invariants, guards, resets, and initial values are given by rectangular constraints, the flows are described by linear differential inclusions of the form \(ax + b \lhd_1\dot{x} \lhd_2 cx+d\) (with ⊲ 1, ⊲ 2 ∈ { < , ≤ }), and a variable x is reset on mode change whenever the differential inclusion describing the dynamics for x changes. Such automata strictly subsume initialized rectangular automata. Our main result is that while the control state reachability problem for such automata is undecidable, the time-bounded reachability problem is decidable.


Hybrid System Rectangular Region Contraction Operator Hybrid Automaton Reachability Problem 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Agrawal, M., Thiagarajan, P.S.: The discrete time behavior of lazy linear hybrid automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 55–69. Springer, Heidelberg (2005)Google Scholar
  2. 2.
    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)CrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Alur, R., Kurshan, R.P., Viswanathan, M.: Membership questions for timed and hybrid automata. In: RTSS 1998, pp. 254–263. Press (1998)Google Scholar
  5. 5.
    Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. TCS 138(1), 35–65 (1995)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Asarin, E., Schneider, G., Yovine, S.: Algorithmic analysis of polygonal hybrid systems, Part I: Reachability. TCS 379(1-2), 231–265 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73–88. Springer, Heidelberg (2000)Google Scholar
  9. 9.
    Brent, R.P.: Fast algorithms for high-precision computation of elementary functions (invited talk). In: Seventh Conference on Real Numbers and Computers (RNC7), vol. (7-8), July 10-12 (2006)Google Scholar
  10. 10.
    Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: On reachability for hybrid automata over bounded time. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 416–427. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: Complexity and fixed points. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 55–70. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  12. 12.
    Casagrande, A., Piazza, C., Policriti, A., Mishra, B.: Inclusion dynamics hybrid automata. Inf. Comput. 206(12), 1394–1424 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Chadha, R., Kini, D., Viswanathan, M.: Quantitative information flow in boolean programs. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 103–119. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  14. 14.
    Duggirala, P.S., Tiwari, A.: Safety verification for linear systems. In: Proceedings of EMSOFT (2013)Google Scholar
  15. 15.
    Fränzle, M.: Analysis of hybrid systems: An ounce of realism can save an infinity of states. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 126–140. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Gentilini, R.: Reachability problems on extended O-minimal hybrid automata. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 162–176. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  17. 17.
    Henzinger, T.A.: The theory of hybrid automata. In: Proceeding of IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)Google Scholar
  18. 18.
    Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control 43(4), 540–554 (1998)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences, 373–382 (1995)Google Scholar
  20. 20.
    Hesse, W., Allender, E., Barrington, D.A.M.: Uniform constant-depth threshold circuits for division and iteratd multiplication. Journal of Computer and System Sciences 65(4), 695–716 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  21. 21.
    Jenkins, M., Ouaknine, J., Rabinovich, A., Worrell, J.: Alternating timed automata over bounded time, pp. 60–69. IEEE Computer Society, Los Alamitos (2010)Google Scholar
  22. 22.
    Lafferriere, G., Pappas, G., Sastry, S.: o-minimal hybrid systems. MCSS 13, 1–21 (2000)zbMATHMathSciNetGoogle Scholar
  23. 23.
    Maler, O., Pnueli, A.: Reachability analysis of planar multi-linear systems. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 194–209. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  24. 24.
    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)Google Scholar
  25. 25.
    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)Google Scholar
  26. 26.
    Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 496–510. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  27. 27.
    Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 48–67. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  28. 28.
    Prabhakar, P., Vladimerou, V., Viswanathan, M., Dullerud, G.E.: A decidable class of planar linear hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 401–414. Springer, Heidelberg (2008)Google Scholar
  29. 29.
    Reif, J.H., Tate, S.R.: On threshold circuits and polynomial computation. SIAM Journal on Computing 21(5), 896–908 (1992)CrossRefzbMATHMathSciNetGoogle Scholar
  30. 30.
    Roohi, N., Viswanathan, M.: Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. Technical report, University of Illinois at Urbana-Champaign (2014),
  31. 31.
    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)CrossRefGoogle Scholar
  32. 32.
    Yap, C.: Pi is in log space,

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Nima Roohi
    • 1
  • Mahesh Viswanathan
    • 1
  1. 1.Department of Computer ScienceUniversity of Illinois at Urbana-ChampaignUSA

Personalised recommendations