Abstract
We consider the reachability problem for timed automata. One of the most well-known solutions for this problem is the zone-based search method. Max bound abstraction and LU-bound abstraction on zones have been proposed to reduce the state space for zone based search. These abstractions use bounds collected from the timed automata structure to compute an abstract state space. In this paper we propose a difference bound constraint abstraction for zones. In this abstraction, sets of difference bound constraints collected from the symbolic run are used to compute the abstract states. Based on this new abstraction scheme, we propose an algorithm for the reachability checking of timed automata. Experiment results are reported on several timed automata benchmarks.
Chapter PDF
References
Benchmarks of Timed Automata, http://www.comp.nus.edu.sg/~pat/bddlib/timedexp.html
Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 346–360. Springer, Heidelberg (1997)
Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003)
Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)
Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 318–343. Springer, Heidelberg (2001)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70. ACM (2002)
Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: FSTTCS 2011, pp. 78–89 (2011)
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 990–1005. Springer, Heidelberg (2013)
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. CoRR abs/1301.3127 (2013)
McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 363–378. Springer, Heidelberg (2004)
Wozna, B., Zbrzezny, A., Penczek, W.: Checking reachability properties for timed automata via sat. Fundam. Inf. 55(2), 223–241 (2003)
Yovine, S.: Model checking timed automata. In: Rozenberg, G., Vaandrager, F.W. (eds.) Lectures on Embedded Systems. LNCS, vol. 1494, pp. 114–152. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wang, W., Jiao, L. (2015). Difference Bound Constraint Abstraction for Timed Automata Reachability Checking. In: Graf, S., Viswanathan, M. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2015. Lecture Notes in Computer Science(), vol 9039. Springer, Cham. https://doi.org/10.1007/978-3-319-19195-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-19195-9_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19194-2
Online ISBN: 978-3-319-19195-9
eBook Packages: Computer ScienceComputer Science (R0)