Expressiveness issues in interval temporal logics

Mattia Guiotto

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 case-by-case 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 long-standing 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

1. Ben C. Moszkowski and Zohar Manna,Reasoning in Interval Temporal Logic,Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings(Edmund M. Clarke and Dexter Kozen),vol. 164,Springer,1983,pp. 371–382.
2. Halpern, Joseph Y and Shoham, Yoav,A propositional modal logic of time intervals,Journal of the ACM (JACM),vol. 38 (1991), no. 4, pp. 935–962.
3. Allen, James F,Maintaining knowledge about temporal intervals,Communications of the ACM,vol. 26 (1983), no. 11, pp. 832–843.
4. Luca Aceto, Dario Della Monica, Anna Ing’olfsd’ottir, Angelo Montanari, and Guido Sciavicco,On the expressiveness of the interval logic of {A}llen’s relations over finite and discrete linear orders,Proc. of the 14th European Conference on Logics in Artificial Intelligence (JELIA),vol. 8761,2014,pp. 267–281.
5. Goranko, Valentin and Otto, Martin,Handbook of modal logic,Model Theory of Modal LogicAmsterdam, The Netherlands: Elsevier,2006,pp. 255–325.
6. Mattia Guiotto,Expressiveness issues in Interval Temporal Logic,[Bachelor’s Thesis],University of Udine,2023.https://drive.google.com/file/d/1m6fwreCJg8AUhatlvd9nAiTp96WHD7NX/view?usp=drive_link

 Overview  Program