Abstract
This paper introduces two mechanisms for computing over-approximations of sets of reachable states, with the aim of ensuring termination of state-space exploration. The first mechanism consists in over-approximating the automata representing reachable sets by merging some of their states with respect to simple syntactic criteria, or a combination of such criteria. The second approximation mechanism consists in manipulating an auxiliary automaton when applying a transducer representing the transition relation to an automaton encoding the initial states. In addition, for the second mechanism we propose a new approach to refine the approximations depending on a property of interest. The proposals are evaluated on examples of mutual exclusion protocols.
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
Abdulla, P.A., Jonsson, B., Mahata, P., d’Orso, J.: Regular tree model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 555–568. Springer, Heidelberg (2002)
Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, Majumdar (eds.) [18], pp. 158–174
Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Algorithmic improvements in regular model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 236–248. Springer, Heidelberg (2003)
Baier, C., Katoen, J.P., Ebrary, I.: Principles of model checking, vol. 950. MIT Press (2008)
Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 85–100. Springer, Heidelberg (2012)
Boichut, Y., Courbis, R., Héam, P.-C., Kouchnarenko, O.: Finer is better: Abstraction refinement for rewriting approximations. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 48–62. Springer, Heidelberg (2008)
Boigelot, B.: Domain-specific regular acceleration. STTT 14(2), 193–206 (2012)
Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223–235. Springer, Heidelberg (2003)
Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. Technical report, 13 p. (January 2012)
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Bouajjani, A., Touili, T.: Widening techniques for regular tree model checking. STTT, 1–21 (2011)
Clarke, E.M., 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)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking, 2000. MIT Press (2000)
Dams, D.R., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 286–297. Springer, Heidelberg (2001)
Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. Journal of Logic and Algebraic Programming 52, 109–127 (2002)
Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, Majumdar (eds.) [18], pp. 2–22
Esparza, J., Majumdar, R. (eds.): TACAS 2010. LNCS, vol. 6015. Springer, Heidelberg (2010)
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program specialization for verifying infinite state systems: An experimental evaluation. Logic-Based Program Synthesis and Transformation, 164–183 (2011)
Le Gall, T., Jeannet, B.: Lattice automata: A representation for languages on infinite alphabets, and some applications to verification. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 52–68. Springer, Heidelberg (2007)
Gómez, A.C., Guaiana, G., Pin, J.-É.: When does partial commutative closure preserve regularity? 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. 209–220. Springer, Heidelberg (2008)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S. (ed.) TACAS/ETAPS 2000. LNCS, vol. 1785, pp. 220–235. Springer, Heidelberg (2000)
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Legay, A.: Extrapolating (omega-) regular model checking. STTT 14(2), 119–143 (2012)
Touili, T.: Regular model-checking using widening techniques. In: VEPAS. ENTCS, vol. 50, pp. 342–356 (2001)
Yu, F., Bultan, T., Ibarra, O.: Relational string verification using multi-track automata. IJFCS 22, 290–299 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dreyfus, A., Héam, PC., Kouchnarenko, O. (2013). Enhancing Approximations for Regular Reachability Analysis. In: Konstantinidis, S. (eds) Implementation and Application of Automata. CIAA 2013. Lecture Notes in Computer Science, vol 7982. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39274-0_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-39274-0_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39273-3
Online ISBN: 978-3-642-39274-0
eBook Packages: Computer ScienceComputer Science (R0)