A Decidability Result for the Model Checking of Infinite-State Systems

2010 ◽  
Vol 48 (1) ◽  
pp. 1-42
Author(s):  
Daniele Zucchelli ◽  
Enrica Nicolini
Keyword(s):  
Model Checking ◽  
Decidability Result ◽  
Infinite State Systems ◽  
Infinite State

AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES

2013 ◽  
Vol 24 (02) ◽  
pp. 211-232 ◽  
Author(s):  
ALESSANDRO CARIONI ◽  
SILVIO GHILARDI ◽  
SILVIO RANISE
Keyword(s):  
Model Checking ◽  
Sufficient Conditions ◽  
Order Logic ◽  
Satisfiability Modulo Theories ◽  
First Order Logic ◽  
Reachability Problem ◽  
First Order ◽  
Recent Advances ◽  
Infinite State Systems ◽  
Infinite State

We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic.

scholarly journals Automatic verification of timed concurrent constraint programs

2006 ◽  
Vol 6 (3) ◽  
pp. 265-300 ◽  
Author(s):  
MORENO FALASCHI ◽  
ALICIA VILLANUEVA
Keyword(s):  
Model Checking ◽  
Infinite Number ◽  
Reactive Systems ◽  
Finite Model ◽  
Computation Model ◽  
Huge Number ◽  
Finite State ◽  
Infinite State Systems ◽  
Infinite State ◽  
Concurrent Constraint Programming

The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.

scholarly journals Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

2021 ◽  
pp. 113-132
Author(s):  
Makai Mann ◽  
Ahmed Irfan ◽  
Alberto Griggio ◽  
Oded Padon ◽  
Clark Barrett
Keyword(s):  
Model Checking ◽  
State Of The Art ◽  
Inductive Reasoning ◽  
Auxiliary Variables ◽  
Abstraction Refinement ◽  
Free Induction ◽  
Induction Proofs ◽  
Infinite State Systems ◽  
Infinite State

AbstractWe develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.

Sign in / Sign up

Export Citation Format

Share Document