Informatics Report Series


Report   

EDI-INF-RR-1261


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Recurrent Reachability Analysis in Regular Model Checking
Authors: Anthony Lin ; Leonid Libkin
Date:Jun 2008
Publication Type:Conference Paper Publication Status:Submitted
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh