scholarly journals Verification of Temporal Properties of Concurrent Systems

1993 ◽  
Vol 22 (445) ◽  
Author(s):  
Henrik Reif Andersen
Keyword(s):  
Model Checking ◽  
Concurrent Systems ◽  
Temporal Properties ◽  
Compositional Approach ◽  
Completeness Result ◽  
Finite State ◽  
Infinite State Systems ◽  
Novel Applications ◽  
Infinite State ◽  
Intuitionistic Version

This thesis is concerned with the verification of concurrent systems modelled by process algebras. It provides methods and techniques for reasoning about temporal properties as described by assertions from an expressive modal logic -- the modal µ-calculus. It describes a compositional approach to model checking, efficient local and global algorithms for model checking finite-state systems, a general local fixed-point finding algorithm, a proof system for model checking infinite-state systems, a categorical completeness result for an intuitionistic version of the modal µ-calculus, and finally it shows some novel applications of the logic for expressing behavioural relations.

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.

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 Temporal prophecy for proving temporal properties of infinite-state systems

2021 ◽  
Author(s):  
Oded Padon ◽  
Jochen Hoenicke ◽  
Kenneth L. McMillan ◽  
Andreas Podelski ◽  
Mooly Sagiv ◽  
...  
Keyword(s):  
Order Logic ◽  
Cut Elimination ◽  
Temporal Property ◽  
Deductive Verification ◽  
First Order ◽  
Temporal Properties ◽  
Safety Property ◽  
Infinite State Systems ◽  
Verification Techniques ◽  
Infinite State

AbstractVarious verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.

scholarly journals On Reasoning about Infinite-State Systems in the Modal µ-Calculus

1993 ◽  
Vol 22 (446) ◽  
Author(s):  
Henrik Reif Andersen
Keyword(s):  
Fixed Points ◽  
General Purpose ◽  
Essential Ingredient ◽  
Success Criterion ◽  
Success Criteria ◽  
Tableau Method ◽  
Finite State ◽  
Infinite State Systems ◽  
Proof Tree ◽  
Infinite State

This paper presents a proof method for proving that infinite-state systems satisfy properties expressed in the modal µ-calculus. The method is sound and complete relative to externally proving inclusions of sets of states. It can be seen as a recast of a tableau method due to Bradfield and Stirling following lines used by Winskel for finite-state systems. Contrary to the tableau method, it avoids the use of constants when unfolding fixed points and it replaces the rather involved global success criterion in the tableau method with local success criteria. A proof tree is now merely a means of keeping track of where possible choices are made -- and can be changed -- and not an essential ingredient in establishing the correctness of a proof: A proof will be correct when all leaves can be directly seen to be valid. Therefore, it seems well-suited for implementation as a tool, by, for instance, integration into existing general-purpose theorem provers.

scholarly journals Generalization strategies for the verification of infinite state systems

2012 ◽  
Vol 13 (2) ◽  
pp. 175-199 ◽  
Author(s):  
FABIO FIORAVANTI ◽  
ALBERTO PETTOROSSI ◽  
MAURIZIO PROIETTI ◽  
VALERIO SENNI
Keyword(s):  
Program Analysis ◽  
Second Phase ◽  
Initial State ◽  
Verification Method ◽  
Program Specialization ◽  
Temporal Properties ◽  
Infinite State Systems ◽  
Two Phases ◽  
Constraint Logic Programs ◽  
Infinite State

AbstractWe present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.

Sign in / Sign up

Export Citation Format

Share Document