Abstract
This paper investigates the use of tree automata with global equalities and disequalities (TAGED for short) in reachability analysis over term rewriting systems (TRSs). The reachability problem being in general undecidable on non terminating TRSs, we provide TAGED-based construction, and then design approximation-based semi-decision procedures to model-check useful temporal patterns on infinite state rewriting graphs. To show that the above TAGED-based construction can be effectively carried out, complexity analysis for rewriting TAGED-definable languages is given. © 2009 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Courbis, R., Héam, P. C., & Kouchnarenko, O. (2009). TAGED approximations for temporal properties model-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5642 LNCS, pp. 135–144). https://doi.org/10.1007/978-3-642-02979-0_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
