Abstract
We study the time-bounded reachability problem for monotonic hybrid automata (MHA), i.e., rectangular hybrid automata for which the rate of each variable is either always non-negative or always non-positive. In this paper, we revisit the decidability results presented in [5] and show that the problem is NExpTime-complete. We also show that we can effectively compute fixed points that characterise the sets of states that are reachable (resp. co-reachable) within T time units from a given state.
This work has been partly supported by a grant from the National Bank of Belgium, the ARC project (number AUWB-2010-10/15-UMONS-3), the FRFC project (number 2.4545.11) and a ‘Crédit aux chercheurs’ of the FRS – F.N.R.S.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, Springer, Heidelberg (1993)
Alur, R., Dill, D.: A theory of timed automata. TTCS 126(2), 183–235 (1994)
Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1-2) (2008)
Basu, S.: New results on quantifier elimination over real closed fields and applications to constraint databases. J. ACM 46(4) (1999)
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)
Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for hybrid automata: Complexity and fixpoints. Technical report CoRR abs/1211.1276, Cornell University Library, arXiv.org (2012), http://arxiv.org/abs/1211.1276
Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996. IEEE Computer Society (1996)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A user guide to HyTech. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 41–71. Springer, Heidelberg (1995)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Hytech: A model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata. JCSS 57(1), 94–124 (1998)
Henzinger, T.A., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Comput. Log. 6(1), 1–32 (2005)
Jenkins, M., Ouaknine, J., Rabinovich, A., Worrell, J.: Alternating timed automata over bounded time. In: LICS 2010. IEEE Computer Society (2010)
Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 287–300. Springer, Heidelberg (2007)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, JF., Worrell, J. (2013). Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)