PhD Alumni


Bersani Marcello Maria

Present position:
 

Thesis title:  Bounded Approaches for Verification of Infinite-State Systems
Advisor:  Pierluigi San Pietro
Research area:  Advanced software architectures and methodologies
Thesis abstract:  
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.