HyLMoC - A Model Checker for Hybrid Logic

The current technological trend depicts a scenario in which space, and more generally the environment in which the computation takes place, rep- resents a key aspect that must be considered in order to improve systems context awareness. Reasoning about such context can be interpreted as spatial reasoning, which means not only to be able to carry out inferences about the space itself, but also inferences about spatially related information according a given background knowledge. Past works have shown that hybrid modal logics are a powerful and rich formalism to model qualitative spatial reasoning and reasoning on informa- tion spread into graph-like structures. In this paper we present the preliminary results we obtained in designing and implementing HyLMoC, a model check- ing system for hybrid modal logics. The functionalities of the model checker are based on backend module that accepts as inputs a list of hybrid modal formu- las and the specification of a labeled graph structure that is compliant with the characteristics of a Kripke model. The current implementation of the backend al- lows to perform different reasoning tasks with respect to those inputs: Local and Global model checking, and All-worlds model checking.