Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-89439-1_15 | LPAR |
Keywords | Field | DocType |
infinite system,regular relation,transitive closure,regular ground tree,recurrent reachability predicate,initial state,transition relation,recurrent reachability,regular set,regular model checking,recurrent reachability analysis,transition system,polynomial time,satisfiability,model checking,process algebra | Transition system,Model checking,Transitive reduction,Computer science,Algorithm,Decidability,Reachability,Transitive closure,Time complexity,Transitive relation | Conference |
Volume | ISSN | Citations |
5330 | 0302-9743 | 10 |
PageRank | References | Authors |
0.75 | 20 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Anthony Widjaja To | 1 | 113 | 6.13 |
| Leonid Libkin | 2 | 3446 | 764.02 |