Paper Info
Title
TAGED Approximations for Temporal Properties Model-Checking
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.
Year
DOI
Venue
2009
10.1007/978-3-642-02979-0_17
CIAA
Keywords
Field
DocType
reachability analysis,complexity analysis,taged-definable language,infinite state,global equality,approximation-based semi-decision procedure,general undecidable,tree automaton,taged-based construction,temporal properties model-checking,taged approximations,reachability problem,model checking
Discrete mathematics,Model checking,Automaton,Linear temporal logic,Theoretical computer science,Reachability,Rewriting,Reachability problem,Temporal logic,Mathematics,Undecidable problem
Conference
Volume
ISSN
Citations 
5642
0302-9743
2
PageRank 
References 
Authors
0.37
29
3
Name
Order
Citations
PageRank
Roméo Courbis1182.02
Pierre-cyrille Héam210117.27
O. Kouchnarenko371646.76