Abstract
We consider the problem of recurrent reachability over infinite systems given by regular relations on words and trees, i.e, whether a given regular set of states can be reached infinitely often from a given initial state in the given transition system. Under the condition that the transitive closure of the transition relation is regular, we show that the problem is decidable, and the set of all initial states satisfying the property is regular. Moreover, our algorithm constructs an automaton for this set in polynomial time, assuming that a transducer of the transitive closure can be computed in poly-time. We then demonstrate that transition systems generated by pushdown systems, regular ground tree rewrite systems, and the well-known process algebra PA satisfy our condition and transducers for their transitive closures can be computed in poly-time. Our result also implies that model checking EF-logic extended by recurrent reachability predicate (EGF) over such systems is decidable.
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.: Undecidable verification problems for programs with unreliable channels. Inf. Comput. 130(1), 71–90 (1996)
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., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004)
Baeten, J., Weijland, W.: Process Algebra. In: CUP (1990)
Benedikt, M., Libkin, L., Neven, F.: Logical definability and query languages over ranked and unranked trees. ACM Trans. Comput. Logic 8(2), 11 (2007)
Blumensath, A., Grädel, E.: Automatic structures. In: LICS 2000, pp. 51–60 (2000)
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)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in (ω-)regular model checking. In: INFINITY, pp. 101–115 (2004)
Caucal, D.: On the regular structure of prefix rewriting. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol. 431, pp. 61–86. Springer, Heidelberg (1990)
Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106(1), 61–86 (1992)
Comon, H., et al.: Tree Automata: Techniques and Applications (2007), http://www.grappa.univ-lille3.fr/tata
Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: LICS 1990, pp. 242–248 (1990)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003)
Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: POPL 2000, USA, pp. 1–11. ACM, New York (2000)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 220–234. Springer, Heidelberg (2000)
Löding, C.: Model-checking infinite systems generated by ground tree rewriting. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 280–294. Springer, Heidelberg (2002)
Löding, C.: Reachability problems on regular ground tree rewriting graphs. Theory Comput. Syst. 39(2), 347–383 (2006)
Lugiez, D., Schnoebelen, P.: The regular viewpoint on PA-processes. Theor. Comput. Sci. 274(1-2), 89–115 (2002)
Lugiez, D., Schnoebelen, P.: Decidable first-order transition logics for PA-processes. Inf. Comput. 203(1), 75–113 (2005)
Mayr, R.: Process rewrite systems. Inf. Comput. 156(1-2), 264–286 (2000)
Mayr, R.: Decidability of model checking with the temporal logic EF. Theor. Comp. Sci. 256(1-2), 31–62 (2001)
Thomas, W.: Constructing infinite graphs with a decidable MSO-theory. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 113–124. Springer, Heidelberg (2003)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Proc. Banff Higher-Order Workshop, pp. 238–266
Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. JCSS 32(2), 183–221 (1986)
Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
To, A.W., Libkin, L. (2008). Recurrent Reachability Analysis in Regular Model Checking. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)