Ghilardi, Silvio ;
Ranise, Silvio ;
Nicolini, Enrica ;
Zucchelli, Daniele
From NonDisjoint Combination to Satisfiability and ModelChecking of Infinite State Systems
Abstract
In the first part of our contribution, we review recent results on combined constraint satisfiability for first order theories in the nondisjoint signatures case: this is done mainly in view of the applications to temporal satisfiability and modelchecking covered by the second part of our talk, but we also illustrate in more detail some casestudy where nondisjoint combination arises. The first case deals with extensions of the theory of arrays where indexes are endowed with a Presburger arithmetic structure
and a length expressing `dimension' is added; the second case deals with the algebraic counterparts of fusion in modal logics. We then recall the basic features of the NelsonOppen method and investigate sufficient conditions for it to be complete and terminating in the nondisjoint signatures case: for completeness we rely on a modeltheoretic $T_0$compatibility condition (generalizing stable infiniteness) and for termination we impose a noetherianity requirement on positive constraints chains. We finally supply examples of theories matching these combinability hypotheses.
In the second part of our contribution, we develop a framework for integrating firstorder logic (FOL) and discrete Linear time Temporal Logic (LTL). Manna and Pnueli have extensively shown how a mixture of FOL and LTL is sufficient to precisely state verification problems for the class of
reactive systems: theories in FOL model the (possibly infinite) data structures used by a reactive system while LTL specifies its (dynamic) behavior. Our framework for the integration is the following: we fix a theory $T$ in a firstorder signature $Sigma$ and consider as a temporal model a sequence $cM_1, cM_2, dots$ of standard (firstorder) models of $T$ and assume such models to share the same carrier (or, equivalently, the domain of the temporal model to be `constant'). Following Plaisted, we consider symbols from a subsignature $Sigma_r$ of $Sigma$ to be emph{rigid}, i.e. in a temporal model $cM_1, cM_2, dots$, the
$Sigma_r$restrictions of the $cM_i$'s must coincide. The symbols
in $Sigmasetminus Sigma_r$ are called `flexible' and their
interpretation is allowed to change over time (free variables are
similarly divided into `rigid' and `flexible'). For modelchecking,
the emph{initial states} and the emph{transition relation} are
represented by firstorder formulae, whose role is that of
(nondeterministically) restricting the temporal evolution of the
model.
In the quantifierfree case, we obtain sufficient conditions for %undecidability and decidability for both satisfiability and modelchecking of safety properties emph{by lifting combination methods} for emph{nondisjoint} theories in FOL: noetherianity and $T_0$compatibility
(where $T_0$ is the theory axiomatizing the rigid subtheory) gives decidability of satisfiability, whereas $T_0$compatibility and local finiteness give safety modelchecking decidability. The proofs of these decidability results suggest how decision procedures for the constraint satisfiability problem of theories in FOL and algorithms for checking the satisfiability of propositional LTL formulae can be integrated. This paves the way to employ efficient Satisfiability Modulo Theories solvers in the
modelchecking of infinite state systems. We illustrate our
techniques on some examples and discuss further work in the area.
BibTeX  Entry
@InProceedings{ghilardi_et_al:DSP:2007:1247,
author = {Silvio Ghilardi and Silvio Ranise and Enrica Nicolini and Daniele Zucchelli},
title = {From NonDisjoint Combination to Satisfiability and ModelChecking of Infinite State Systems},
booktitle = {Deduction and Decision Procedures},
year = {2007},
editor = {Franz Baader and Byron Cook and J{\"u}rgen Giesl and Robert Nieuwenhuis},
number = {07401},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2007/1247},
annote = {Keywords: Non disjoint combination, linear temporal logic, model checking}
}
29.11.2007
Keywords: 

Non disjoint combination, linear temporal logic, model checking 
Seminar: 

07401  Deduction and Decision Procedures

Issue date: 

2007 
Date of publication: 

29.11.2007 