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 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 Behavioural Equivalence for Infinite Systems—Partially Decidable!

1995 ◽  
Vol 2 (55) ◽  
Author(s):  
Mogens Nielsen ◽  
Kim Sunesen
Keyword(s):  
Petri Nets ◽  
Parallel Processes ◽  
Significant Difference ◽  
Finite State ◽  
Infinite State Systems ◽  
Description Languages ◽  
Traditional Approaches ◽  
Language Equivalence ◽  
Infinite State

For finite-state systems non-interleaving equivalences are computationally<br />at least as hard as interleaving equivalences. In this paper we show<br />that when moving to infinite-state systems, this situation may change<br />dramatically.<br />We compare standard language equivalence for process description languages with two generalizations based on traditional approaches capturing non-interleaving behaviour, pomsets representing global causal dependency, and locality representing spatial distribution of events.<br />We first study equivalences on Basic Parallel Processes, BPP, a process<br />calculus equivalent to communication free Petri nets. For this simple<br />process language our two notions of non-interleaving equivalences agree.<br />More interestingly, we show that they are decidable, contrasting a result of<br />Hirshfeld that standard interleaving language equivalence is undecidable.<br />Our result is inspired by a recent result of Esparza and Kiehn, showing<br />the same phenomenon in the setting of model checking.<br />We follow up investigating to which extent the result extends to larger<br />subsets of CCS and TCSP. We discover a significant difference between<br />our non-interleaving equivalences. We show that for a certain non-trivial<br />subclass of processes between BPP and TCSP, not only are the two equivalences different, but one (locality) is decidable whereas the other (pomsets) is not. The decidability result for locality is proved by a reduction to the reachability problem for Petri nets.

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 Model Completeness, Uniform Interpolants and Superposition Calculus

2021 ◽  
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Automated Reasoning ◽  
Quantifier Elimination ◽  
Effective Solution ◽  
Model Completeness ◽  
Present Contribution ◽  
First Order ◽  
Reduction Strategies ◽  
Infinite State Systems ◽  
Infinite State ◽  
Superposition Calculus

AbstractUniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

scholarly journals Reachability Modulo Theory Library

10.29007/f3rp ◽  
2018 ◽  
Author(s):  
Francesco Alberti ◽  
Roberto Bruttomesso ◽  
Silvio Ghilardi ◽  
Silvio Ranise ◽  
Natasha Sharygina
Keyword(s):  
Reachability Analysis ◽  
Safety Properties ◽  
Standard Language ◽  
Transition Systems ◽  
Smt Solvers ◽  
Verification Tools ◽  
Infinite State Systems ◽  
Infinite State

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.

Sign in / Sign up

Export Citation Format

Share Document