- 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 effectively 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 polynomial time. We then demonstrate that transition systems generated by pushdown systems, regular ground tree rewrite systems, and PA-processes satisfy our condition and transducers for their transitive closures can be computed in polynomial time. Our result also implies that model checking EF-logic extended by recurrent reachability predicate (EGF) over such systems is decidable.
- Links To Paper
- Preprint (full version)
- Bibtex format
- @InProceedings{EDI-INF-RR-1261,
- author = {
Anthony Lin
and Leonid Libkin
},
- title = {Recurrent Reachability Analysis in Regular Model Checking},
- book title = {},
- year = 2008,
- month = {Jun},
- url = {http://homepages.inf.ed.ac.uk/s0673998/papers/rrr.pdf},
- }
|