Paper Info
Title
Reachability Analysis with State-Compatible Automata.
Abstract
Regular tree languages are a popular device for reachability analysis over term rewrite systems, with many applications like analysis of cryptographic protocols, or confluence and termination analysis. At the heart of this approach lies tree automata completion, first introduced by Genet for left-linear rewrite systems. Korp and Middeldorp introduced so-called quasi-deterministic automata to extend the technique to nonleft-linear systems. In this paper, we introduce the simpler notion of state-compatible automata, which are slightly more general than quasi-deterministic, compatible automata. This notion also allows us to decide whether a regular tree language is closed under rewriting, a problem which was not known to be decidable before. Several of our results have been formalized in the theorem prover Isabelle/HOL. This allows to certify automatically generated non-confluence and termination proofs that are using tree automata techniques.
Year
DOI
Venue
2014
10.1007/978-3-319-04921-2_28
Lecture Notes in Computer Science
Field
DocType
Volume
Quantum finite automata,Discrete mathematics,Automata theory,Combinatorics,Programming language,Mobile automaton,Nested word,Computer science,Rewriting,Tree automaton,Regular language,ω-automaton
Conference
8370
ISSN
Citations 
PageRank 
0302-9743
7
0.56
References 
Authors
15
2
Name
Order
Citations
PageRank
Bertram Felgenhauer1387.05
René Thiemann298469.38