Paper Info
Title
Finite countermodels for safety verification of parameterized tree systems
Abstract
In this paper we deal with verification of safety properties of parameterized systems with a tree topology. 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 method is shown is at least as powerful as regular tree model checking and as the methods based on monotonic abstraction and backwards symbolic reachability. The practical efficiency of the method is illustrated on a set of examples taken from the literature.
Year
Venue
Keywords
2011
CoRR
first order,model checking
Field
DocType
Volume
Monotonic function,Discrete mathematics,Parameterized complexity,Abstraction,Algorithm,Decision tree model,Reachability,Network topology,Theoretical computer science,Model finding,Mathematics
Journal
abs/1107.5142
Citations 
PageRank 
References 
2
0.37
6
Authors
1
Name
Order
Citations
PageRank
Alexei Lisitsa127245.94