Computer Science – Logic in Computer Science
Scientific paper
2010-03-25
EPTCS 21, 2010, pp. 99-108
Computer Science
Logic in Computer Science
Scientific paper
10.4204/EPTCS.21.9
The tree automaton completion is an algorithm used for proving safety properties of systems that can be modeled by a term rewriting system. This representation and verification technique works well for proving properties of infinite systems like cryptographic protocols or more recently on Java Bytecode programs. This algorithm computes a tree automaton which represents a (regular) over approximation of the set of reachable terms by rewriting initial terms. This approach is limited by the lack of information about rewriting relation between terms. Actually, terms in relation by rewriting are in the same equivalence class: there are recognized by the same state in the tree automaton. Our objective is to produce an automaton embedding an abstraction of the rewriting relation sufficient to prove temporal properties of the term rewriting system. We propose to extend the algorithm to produce an automaton having more equivalence classes to distinguish a term or a subterm from its successors w.r.t. rewriting. While ground transitions are used to recognize equivalence classes of terms, epsilon-transitions represent the rewriting relation between terms. From the completed automaton, it is possible to automatically build a Kripke structure abstracting the rewriting sequence. States of the Kripke structure are states of the tree automaton and the transition relation is given by the set of epsilon-transitions. States of the Kripke structure are labelled by the set of terms recognized using ground transitions. On this Kripke structure, we define the Regular Linear Temporal Logic (R-LTL) for expressing properties. Such properties can then be checked using standard model checking algorithms. The only difference between LTL and R-LTL is that predicates are replaced by regular sets of acceptable terms.
Boyer Benoît
Genet Thomas
No associations
LandOfFree
Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-555893