Bounded approaches for verification of infinite-state systems

Many verification problems involve checking and synthesis of infinite state systems. In this thesis we study how to solve general verification problems by means of instances of, possibly different, problems of bounded size. Informally, we say that a problem is of bounded size when the object (or solution) which we take into consideration while solving the problem can be defined by a bounded representation with respect to the dimension of the initial problem. In particular, we will face with the satisfiability problem of qualitative specification defined by formulae of linear temporal logic and model-checking problem defined for a specific class of counter systems. We define the problem of $k$-bounded satisfiability for formulae of $\LTL(\foL)$, which is a language obtained by adding to linear temporal logic (LTL) a first-order language, and we give an encoding in the decidable theory of equality and uninterpreted functions. Moreover, we consider a fragment of this general logic and we show that the satisfiability problem for LTL (with past operators) over arithmetical constraints can be answered by solving a finite amount of instances of \emph{bounded} satisfiability problems when atomic formulae belong to certain suitable fragments of Presburger arithmetic. A formula is boundedly satisfiable when it admits an ultimately periodic model of the form $uv^\omega$, where $u$ and $v$ are finite sequences of \emph{symbolic valuations}. Therefore, for every formula there exists a \emph{completeness bound} $c$, such that, if there is no ultimately periodic model with $|uv|\le c$, then the formula is unsatisfiable. In this case, we say that the language has the completeness property. Whenever a fragment of $\LTL(\foL)$ benefits of such a completeness property then $k$-bounded satisfiability can be exploited to solve the satisfiability problem for the language. Most verification problems on counter systems are known to be undecidable in general; decidability can be retained by considering a more specific problem than the general one which is defined with respect to runs with bounded features. We study model-checking problems on counter systems when the specification languages are LTL-like dialects with arithmetical constraints. Guards characterizing transitions of counter systems are Presburger definable formulae and runs are restricted to reversal-bounded ones. We introduce a generalization of reversal-boundedness that captures both original Ibarra's notion as well as more recent ones. We show the \nexptime-completeness of the reversal-bounded model-checking problem and the reversal-bounded reachability problem. We show the effective Presburger definability for reachability sets and for sets of configurations for which there is a reversal-bounded run verifying a given temporal formula. Moreover, we show that reversal-bounded model-checking problem can be solved by looking for ultimately periodic runs with bounded length satisfying a given property. Therefore, since we are restricting the analysis to bounded runs, we can exploit a reduction to $k$-bounded satisfiability of a temporal formula encoding the transition relation of a counter systems and the semantics of a given temporal specification over ultimately periodic runs.

Molti problemi di verifica consistono nell'analisi e sintesi di sistemi a stati infiniti. In questa tesi viene presentato un metodo di risoluzione di una classe di questi problemi che utilizza istanze di problemi di dimensione bounded. Informalmente, diciamo che un problema ha dimensione bounded quando la sua soluzione può essere rappresentata in modo finito rispetto alla dimensione del problema iniziale. In dettaglio, i due principali problemi studiati sono il problema di soddisfacibilità di formule definite mediante formule di logiche temporali ed il problema di model-checking definito rispetto ad una classe specifica di counter systems. In prima istanza, definiremo il problema di $k$-bounded satisfiability per formule di $\LTL(\foL)$, che è il linguaggio ottenuto estendendo Linear Temporal Logic ($\LTL$) mediante un linguaggio del primo ordine, e proporremo un encoding nella teoria (decidibile) dell'uguaglianza combinata alla teoria delle funzioni non interpretate. Inoltre, considereremo un frammento di questa logica generale e mostreremo che il problema di soddisfacibilità di $\LTL$ (con operatori al passato) con vincoli aritmetici può essere risolto mediante un numero finito di istanze di problemi di $k$-bounded satisfiability quando le formule atomiche di tale logica appartengono ad uno specifico frammento della logica di Presburger. Diremo che una formula \`e \emph{bounded} satisfiable quando ammette un modello ultimamente periodico della forma $uv^\omega$, dove $u$ e $v$ sono sequenze finite di \emph{symbolic valuations}. Per ogni formula esiste un \emph{bound di completezza} $c$ tale che, se non esiste alcun modello ultimamemente periodico con $|uv|\leq c$, allora la formula è insoddifacibile. In questo caso, diremo che il linguaggio gode della proprietà di completezza. Quando un frammento di $\LTL(\foL)$ gode della proprietà di completezza allora il problema di $k$-bounded satisfiability può essere utilizzato per risolvere il problema di soddisfacibilità generale. Molti problemi definiti su counter systems sono dimostrati essere indecidibili in generale; tuttavia, è possibile preservarne la decidibilità considerando un problema più specifico definito rispetto ad un sottinsieme dei run del sistema soddisfacenti specifiche caratteristiche. Studieremo il problema di model-checking per una classe di counter systems quando il linguaggio di specifica è un frammento di $\LTL$ con vincoli aritmetici. Le formule caratterizzanti le transizioni dei counter systems di questa classe sono formule definibili nell'aritmetica di Presburger ed i run sono ristretti a quelli soddisfacenti la proprietà di reversal-boundedness. Introdurremo una generalizzazione della nozione di reversal-boundedness, che include sia l'originale proposta da Ibarra, che altre di più recente definizione. Dimostreremo che il problema di reversal-bounded model-checking e il problema di reversal-bounded reachability risultano $\nexptime$-completi. Inoltre, dimostreremo che il reachability set e l'insieme di configurazioni raggiungibili da un run reversal-bounded che soddisfa una proprietà definita da una formula temporale nel linguaggio considerato sono definibile nell'aritmetica di Presburger. Il problema di reversal-bounded model-checking può essere risolto ricercando i run ultimamente periodici del counter system in analisi soddisfacenti la proprietà. Pertanto, restringendo l'analisi ai run di lunghezza bounded ed ultimamente periodici, è possibile ridurre il problema di reversal-bounded model-checking al problema di $k$-bounded satisfiability di una formula temporale che codifica la relazione di transizione del counter system e la semantica della formula definita per run ultimamente periodici.