Alessandro Mosca, Daniele Codecasa, Ignazio Gentile, Luca Manzoni

The current technological trend depicts a scenario in which space, and more
generally the environment in which the computation takes place, represents a key
aspect that must be considered in order to improve systems context awareness, even
if the kind of information processed is not only of spatial nature.
Past works by one of the authors of this paper have shown that Hybrid Logics
are a powerful and rich formalism to model Qualitative Spatial Reasoning for
context aware systems. Classes of commonsense spatial models can be defined as
classes of relational structures according to the formal properties of the involved
spatial relations. The relational structures can therefore provide the semantics for
spatial hybrid languages, whose formulas represent contextual information (see on
this, S. Bandini, A. Mosca, M. Palmonari, Commonsense Spatial Reasoning for
Information Correlation in Pervasive Computing, Applied Artificial Intelligence,
Taylor&Francis, Vol. 21/3-4, April 2007).
The present research project deals with the design and the implementation of
Model Checker for Hybrid Modal Logics. With this aim in mind, special attention
will be given to the definition and the management of the models and of the hybrid
formulas.
The functionality of the model checker is based on back-end modules that receive
as input a file containing a hybrid modal formula and a file with the specification
of a labeled graph structure, representing a model. Models have been
implemented as XML files, by means of the definition of suitable DTD schema.
We implement two different DTD, the first one is compatible with the Dragone’s
models (see on this, the work Model checking for hybrid logics (with an application
to semistructured data) by M. Franceschet and M. de Rijke, published in
the Journal of Applied Logic, 4:3, 2006), while the second extends the first one
by allowing the possibility to introduce n-ary relations among worlds. The figure
below shows an example of the XML-based specification of a model we proposed,
together with its diagrammatic representation.
Formulas have been specified in a ‘lisp-like’ format, the features of which are
constrained by a clear defined BNF grammar. According to the possibility to introduce
n-ary relations in the model, the specification of the formulas support the exploitation
of n-ary modal operators (of course, formulas may contain also ’binders’,
’existential’ and ’universal’ quantification).
The implementation of the back-end allows to answer different reasoning tasks,
with respect to those inputs, i.e. validity in a model, satisfiability in a model, and
unsatisfiability. The model checker therefore support the checking of the satisfiability
of a formula with respect to some specified world of the model, as well as
with respect to all the set of worlds. Finally, in the case of a unsatisfiable formula,
the model checker is able to provide the list of the worlds of the models that falsify
the formula.
The latest version of the model checker we implemented provides a parallel
implementation of the model checking tasks (as a ‘multi-threaded execution’),
thus optimizing the use of the resources and increasing the efficiency of the model
checker. Further works will consider the introduction of specific optimization techniques
to treat with long formulas and formulas with several nested operators.

pdf    presentation.pdf

@Inproceedings{MoscaBernini,
    author = {Alessandro Mosca and Daniele Codecasa and Ignazio Gentile and Luca Manzoni},
    title  ={Hybrid Modal Model Checking},
    year = {2008},
    month = {december},
    address = {Udine, Italy},
    editor = {Marco Gavanelli and Toni Mancini},
    organization = {RCRA},
    booktitle = {R.i.C.e.R.c.A. 2008: RCRA Incontri E Confronti},
}