Paper Info
Title
First-order finite satisfiability vs tree automata in safety verification
Abstract
In this paper we deal with verification of safety properties of term-rewriting systems. The verification problem is translated to a purely logical problem of finding a finite countermodel for a first-order formula, which further resolved by a generic finite model finding procedure. A finite countermodel produced during successful verification provides with a concise description of the system invariant sufficient to demonstrate a specific safety property. We show the relative completeness of this approach with respect to the tree automata completion technique. On a set of examples taken from the literature we demonstrate the efficiency of finite model finding approach as well as its explanatory power.
Year
Venue
Keywords
2011
CoRR
first order,satisfiability
Field
DocType
Volume
Quantum finite automata,Discrete mathematics,Finite satisfiability,Automata theory,First order,Automaton,Algorithm,Theoretical computer science,Invariant (mathematics),Completeness (statistics),Mathematics,ω-automaton
Journal
abs/1107.0349
Citations 
PageRank 
References 
0
0.34
10
Authors
1
Name
Order
Citations
PageRank
Alexei Lisitsa127245.94