2011/07/26 by Alexei Lisitsa, Lisitsa, Alexei · 1 citation
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Safety Systems Engineering in Autonomy #cs.LO
paper · pdf · doi:10.48550/arxiv.1107.5142
18 pages
arxiv created 2011/07/26 · openalex publication_date 2011/07/26 · arxiv updated 2011/07/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.