Alessandro Mosca, Daniele Codecasa, Ignazio Gentile, Luca ManzoniThe 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}, } |