Speaker
Mattia Guiotto
University of Udine
Talks at this conference:
Wednesday, 15:40, J336 
Expressiveness issues in interval temporal logics 
Authors: Dario Della Monica and Mattia Guiotto Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities [1]. One of the most studied interval temporal logics is Halpern and Shoham’s Modal Logic of Time Intervals (\hs, for short) [2], which features 12 modal operators, one for each binary relation between intervals over linear orders, known as Allen’s relations [3]. It was proved that the satisfiability of \hs formulae is highly undecidable, which motivated the search for syntactic fragments of \hs offering a good balance between expressiveness and computational complexity. Each subset of modal operators gives rise to a syntactically different \hs fragment. Due to the possibility of defining modal operators in terms of others, not all \hs fragments are expressively different. We consider the problem of obtaining a complete classification of the relative expressive power of all \hs fragments over the class of all discrete and the one of all finite linear orders. An almost complete picture has been obtained [4], with a unique, difficult problem being still open. The missing tile of the expressiveness puzzle is that of the definabilities for the modal operator of \hs corresponding to the Allen relation overlaps. The aim of our work is to complete the picture by filling the remaining gap. More precisely, we conjecture that the set of known definabilities for the \hs modal operator corresponding to the relation overlaps is complete for the class of all discrete linear orders. Proving such a conclusion requires the support of an important classic theoretical result, known as the bisimulation invariance property for modal formulae which is at the basis of undefinability results for modal logics [5]. We provide a proposal for a bisimulation construction, and give strong and convincing evidence to support its correctness. A complete formal proof is quite technically involved and tedious, and requires a meticulous casebycase analysis. We managed to give a partial formal proof by completing one of the most difficult cases [6]. In conclusion, the work done paves the way towards the closure of the longstanding open issue of obtaining a complete expressiveness picture of the family of \hs fragments over the class of all discrete and the one of all finite linear orders. Bibliography
