Abstract
Current symbolic techniques for the automated reasoning over undecidable hybrid automata, force one to choose between the refinement of either an overapproximation or an underapproximation of the set of reachable states. When the analysis of branching time temporal properties is considered, the literature has developed a number of abstractions techniques based on the simulation preorder, that allow the preservation of only true universally quantified formulæ.
This paper suggests a way to surmount these difficulties by defining a succession of abstractions of hybrid automata, which not only (1) allow the detection and the refinement of both over- and under-approximated reachable sets symmetrically, but also (2) preserves the full set of branching time temporal properties (when interpreted on a dense time domain). Moreover, our approach imposes on the corresponding set of abstractions a desirable monotonicity property with respect to the set of model-checked formulaæ.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88, 971–984 (2000)
Brihaye, T., Michaux, C., Rivière, C., Troestler, C.: On O-minimal hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 219–233. Springer, Heidelberg (2004)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Fitting, M.: Kleene’s three valued logics and their children. Fundam. Inf. 20(1-3), 113–131 (1994)
Fränzle, M.: What will be eventually true of polynomial hybrid automata? In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 340–359. Springer, Heidelberg (2001)
Gentilini, R., Mishra, B., Schneider, K.: Successive abstractions of hybrid automata for monotonic CTL model checking. Technical report, Kaiserslautern University (2007)
Ghosh, R., Tiwari, A., Tomlin, C.J.: Automated symbolic reachability analysis; with application to delta-notch signaling automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 233–248. Springer, Heidelberg (2003)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proc. of the 27th Symposium on Theory of Computing, pp. 373–382. ACM Press, New York (1995)
Henzinger, T.A.: The theory of hybrid automata. In: Proc. of the 11th IEEE Symp. on Logic in Computer Science, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Kannellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), 43–68 (1990)
Kleene, S.C.: Introduction to Metamathematics. Wolters-Noordhoff, Groningen (1971)
Lafferriere, G., Pappas, G., Sastry, S.: O-minimal hybrid systems. Mathematics of Control, Signals, and Systems 13, 1–21 (2000)
Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 137–151. Springer, Heidelberg (1999)
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)
Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic algebraic model checking I: Challenges from systems biology. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 5–19. Springer, Heidelberg (2005)
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)
Schneider, K.: Verification of Reactive Systems. Springer, Heidelberg (2004)
Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002)
van den Dries, L.: O-minimal structures. In: Hodges, W. (ed.) Logic: From Foundations to Applications, pp. 99–108. Clarendon Press, Oxford (1996)
van den Dries, L.: Tame topology and o-minimal structures. London Math. Soc. Lecture Note Ser., vol. 248. Cambridge University Press, Cambridge (1998)
Wilkie, A.J.: Schanuel conjecture and the decidability of the real exponential field. In: Algebraic Model Theory, pp. 223–230 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Gentilini, R., Schneider, K., Mishra, B. (2007). Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking. In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-72734-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72732-3
Online ISBN: 978-3-540-72734-7
eBook Packages: Computer ScienceComputer Science (R0)