• abstraction-refinement
• astrazione e raffinamento
• complexity
• logic
• logica
• logica modale
• logica spaziale
• logica spazio-temporale
• logica temporale
• modal logic
• model checking
• model checking simbolico
• multi-focus model
• spatial logic
• spatio-temporal logic
• symbolic model checking
• temporal logic

Model checking is a method for formally verifying finite-state concurrent systems, conceived by Edmund M. Clarke and E. Allen Emerson to solve the Concurrent Program Verification problem and then further developed by several authors in the past years. Currently the method is widely applied to develop verification tools both for software and hardware debugging.

The main idea behind this method is to describe a system by means of an appropriate logic and to develop efficient algorithms in order to test the truth of a formula (in case of truth-value semantics) or to find which entities in the model entail a formula (in case of a set-satisfaction semantics). In the literature, the most used logics are temporal ones such as CTL (Computation Tree Logic) and mu-calculus. These logics allow to describe several interesting properties of a model such as reachability and safety, while retaining a low complexity to check which entities satisfy the property.

Roughly, the model checking procedure follows this schema: by traversing the syntax tree of a formula $\phi$ from the leaves to the root, the procedure can recursively compute the semantics of each subformula, thus obtaining the semantics of $\phi$. This is the case of CTL formulas, whose semantics is computable in linear-time over the structure of the formula. For some logics this traverse has to be repeated several times, as in the case of mu-calculus because of its fixed-point operators, which are usually computed by a recursive procedure. In this case the complexity of the procedure becomes exponential in the number of nested fixed-point operators, although maintaining a linear complexity in the size of the system.

But what is the usual size of a system analyzed with this method? Since usually model checkers are implemented to test hardware or to study configurations of a certain system, the model checkers have to deal with really large systems, even with more than 10^20 states. So in some cases a linear-time complexity is not enough. As the procedure needs to have linear-time complexity to be correct (in the case of a satisfaction-set semantics) it cannot be improved in the general case, but several techniques and heuristics have been developed to achieve a consistent speed up when considering particular classes of models. Two important examples are symbolic model checking and abstraction techniques.

Symbolic model checking is a technique developed by McMillan to study large models by eliminating ``redundant information'' in the description of the subsets using OBDDs (ordered binary decision diagrams). This method proves to be really efficient, especially when the model considered is obtained by a parallel product of systems, as in the original problem studied by Clarke and Emerson.

On the other hand, abstraction techniques work by building an approximation of the model called abstraction and by analyzing it to obtain information on how to perform the model checking procedure. This is the case of CEGAR (counter example guided abstraction refinement), a procedure developed in 2003 and now the basis of a large number of abstraction techniques. The main idea of CEGAR is to build an abstraction that is also a simulation of the original model, use it to compute the semantics of a formula and then, if needed, adjust the abstraction obtaining a finer approximation of the original model.

Both those techniques are broadly applied and achieve a significant speed up when compared with the classic procedures. This show us that developing ad hoc algorithms to solve specific problems is a winning strategy in model checking, and also that the priority when searching for an efficient algorithm is to reduce the size of the model.

An interesting case studied in literature is that of systems describing space. A spatial model is a formal description of a geometrical entity (such as a topological space, a metric space, and so on) by means of a logic, that we will refer to with the evocative name spatial logic. As the concept of spatial model is so generic, several formalizations are considered in literature, and for each of them several logics are studied. The model checking problem for these logics assume a different flavor, as the algorithms now have to take into account the spatial structure of the model to be efficient.

An example of spatial logic currently under study and analyzed in this document is SLCS, the spatial logic of closure spaces. This is a modal logic created in 2014 to describe properties of a system using closure spaces, a generalization of topological spaces. The logic can express some fundemantal spatial properties of a system, such as reachability, safety and proximity, while retaining decidability and linear-time complexity for the model checking procedure.

A generalization both of the concept of spatial logic and of temporal logic is that of spatio-temporal logic. The aim of a spatio-temporal logic is to describe formally the properties of a spatio-temporal model (i.e., the formal description of a spatial system that changes over time). These logics are usually much more expressive than the previous ones, as they permit to intertwin spatial and temporal properties. On the other hand, defining an interesting spatio-temporal logic for which the MCP is decidable and has a low complexity is not easy.

In 2015 a spatio-temporal generalization of the logic SLCS was presented, namely STLCS, the spatio-temporal logic of closure spaces. This logic was developed to describe the movement over time of several agents inside a spatial model and was succesfully applied to verify properties of some real-life systems such as New York bike sharing. The author of this document collaborated to implement a prototype model checker for STLCS used for the analysis above mentioned.


The aim of this document is to introduce the basic concepts to understand the theory described above (i.e., model checking, speed-up techniques and spatio-temporal model checking) and to adapt symbolic model checking and CEGAR to solve the SLCS model checking problem. In particular, a nouvelle abstraction algorithm is developed to speed-up the procedure if the spatial model presents a strong hierarchical structure.