Regular model checking revisited
From MaRDI portal
Abstract: In this contribution we revisit regular model checking, a powerful framework that has been successfully applied for the verification of infinite-state systems, especially parameterized systems (concurrent systems with an arbitrary number of processes). We provide a reformulation of regular model checking with length-preserving transducers in terms of existential second-order theory over automatic structures. We argue that this is a natural formulation that enables us tap into powerful synthesis techniques that have been extensively studied in the software verification community. More precisely, in this formulation the first-order part represents the verification conditions for the desired correctness property (for which we have complete solvers), whereas the existentially quantified second-order variables represent the relations to be synthesized. We show that many interesting correctness properties can be formulated in this way, examples being safety, liveness, bisimilarity, and games. More importantly, we show that this new formulation allows new interesting benchmarks (and old regular model checking benchmarks that were previously believed to be difficult), especially in the domain of parameterized system verification, to be solved.
Recommendations
Cites work
- scientific article; zbMATH DE number 1670791 (Why is no real title available?)
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 5595151 (Why is no real title available?)
- scientific article; zbMATH DE number 1538041 (Why is no real title available?)
- scientific article; zbMATH DE number 1903380 (Why is no real title available?)
- scientific article; zbMATH DE number 2102701 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- Accelerating tree-automatic relations
- Algorithmic metatheorems for decidable LTL model checking over infinite systems
- An automaton learning approach to solving safety games over infinite graphs
- Automata, logics, and infinite games. A guide to current research
- Automated Technology for Verification and Analysis
- CONCUR 2004 - Concurrency Theory
- Computer Aided Verification
- Dafny: an automatic program verifier for functional correctness
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Definable relations and first-order query languages over strings
- Elements of finite model theory.
- Fair termination for parameterized probabilistic concurrent systems
- Finite presentations of infinite structures: Automata and interpretations
- Inference of finite automata using homing sequences
- Learning regular sets from queries and counterexamples
- Liveness of randomised parameterised systems under arbitrary schedulers
- Logic and p-recognizable sets of integers
- Probabilistic bisimulation for parameterized systems (with applications to verifying anonymous protocols)
- Regular symmetry patterns
- The dining cryptographers problem: Unconditional sender and recipient untraceability
- Transforming structures by set interpretations
- Transition Graphs of Rewriting Systems over Unranked Trees
Cited in
(14)- scientific article; zbMATH DE number 1927558 (Why is no real title available?)
- SAT-BASED MODEL CHECKING FOR REGION AUTOMATA
- scientific article; zbMATH DE number 1670791 (Why is no real title available?)
- Model checking, synthesis, and learning
- Regular model checking using inference of regular languages
- scientific article; zbMATH DE number 2081102 (Why is no real title available?)
- A new approach for showing termination of parameterized transition systems
- Automated Technology for Verification and Analysis
- Algorithmic improvements in regular model checking.
- Computer Aided Verification
- Computer Aided Verification
- On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
- An experience in proving regular networks of processes by modular model checking
- Decision procedures for sequence theories
This page was built for publication: Regular model checking revisited
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6045028)
