Abstract
The reachability problem is one of the most important issues in the verification of hybrid systems. Computing the reachable sets of differential equations is difficult, although computing the reachable sets of finite state machines is well developed. Hence, it is not surprising that the reachability of most of hybrid systems is undecidable. In this paper, we identify a family of vector fields and show its reachability problem is decidable. The family consists of all vector fields whose state parts are linear, while input parts are non-linear, possibly with exponential expressions. Such vector fields are commonly used in practice.To the best of our knowledge, the family is one of the most expressive families of vector fields with a decidable reachability problem.The decidability is achieved by proving the decidability of the extension of Tarski’s algebra with some specific exponential functions, which has been proved in [21, 22] due to Strzebonski. In this paper, we propose another decision procedure, which is more efficient when all constraints are open sets. The experimental results indicate the efficiency of our approach, even better than existing approaches based on approximation and numeric computation in general.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Both the tool and the case studies in this section can be found at http://lcs.ios.ac.cn/~chenms/tools/LinR.tar.bz2.
- 2.
References
http://www.math.utah.edu/~gustafso/s2013/2250/systemsExamplesTheory2008.pdf
Achatz, M., McCallum, S., Weispfenning, V.: Deciding polynomial-exponential problems. In: ISSAC 2008 (2008)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138(1), 3–34 (1995)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
Brown, C.W.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput. 32(5), 447–465 (2001)
Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages 2nd GI Conference. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991)
Collins, G.E., Loos, R.: Real zeros of polynomials. In: Computer Algebra - Symbolic and Algebraic Computation, pp. 83–94. Springer (1982)
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1), 29–35 (1988)
Han, J., Dai, L., Xia, B.: Constructing fewer open cells by gcd computation in cad projection. In: ISSAC 2014, pp. 240–247. ACM (2014)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)
Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: ISSAC 1990, pp. 261–264. ACM (1990)
Kong, S., Gao, S., Chen, W., Clarke, E.: dreach: Delta-reachability analysis for hybrid systems. In: TACAS 2015 (2015)
Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. MCSS 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, 231–253 (2001)
McCallum, S.: An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symb. Comput. 5(1), 141–161 (1988)
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573–589. Springer, Heidelberg (2005)
Richardson, D.: How to recognize zero. J. Symb. Comput. 24, 627–645 (1997)
Strzeboński, A.: Solving systems of strict polynomial inequalities. J. Symb. Comput. 29(3), 471–480 (2000)
Strzeboński, A.: Real root isolation for exp-log functions. In: ISSAC 2008, pp. 303–314 (2008)
Strzeboński, A.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46, 1284–1290 (2011)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)
Wing, J.: How can we provide people with cyber-physical systems they can bet their lives on? Computing Research News, 20(1) (2008)
Xu, M., Li, Z.-B., Yang, L.: Quantifier elimination for a class of exponential polynomial formulas. J. Symb. Comput. (2015). doi:10.1016/j.jsc.2014.09.015
Acknowledgements
The first, third and fourth authors are supported partly by NSFC under grants 11290141 and 11271034; the second and fifth authors are supported partly by “973 Program" under grant No. 2014CB340701, by NSFC under grants 91118007 and 91418204, by CDZ project CAP (GZ 1023), and by the CAS/SAFEA International Partnership Program for Creative Research Teams.
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
Gan, T., Chen, M., Dai, L., Xia, B., Zhan, N. (2015). Decidability of the Reachability for a Family of Linear Vector Fields. In: Finkbeiner, B., Pu, G., Zhang, L. (eds) Automated Technology for Verification and Analysis. ATVA 2015. Lecture Notes in Computer Science(), vol 9364. Springer, Cham. https://doi.org/10.1007/978-3-319-24953-7_34
Download citation
DOI: https://doi.org/10.1007/978-3-319-24953-7_34
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24952-0
Online ISBN: 978-3-319-24953-7
eBook Packages: Computer ScienceComputer Science (R0)