# 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

- Ben C. Moszkowski and Zohar Manna,
*Reasoning in Interval Temporal Logic*,(Edmund M. Clarke and Dexter Kozen),vol. 164,Springer,1983,pp. 371–382.*Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings* - Halpern, Joseph Y and Shoham, Yoav,
*A propositional modal logic of time intervals*,,vol. 38 (1991), no. 4, pp. 935–962.*Journal of the ACM (JACM)* - Allen, James F,
*Maintaining knowledge about temporal intervals*,,vol. 26 (1983), no. 11, pp. 832–843.*Communications of the ACM* - 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*,,vol. 8761,2014,pp. 267–281.*Proc. of the 14th European Conference on Logics in Artificial Intelligence (JELIA)* - Goranko, Valentin and Otto, Martin,
*Handbook of modal logic*,Amsterdam, The Netherlands: Elsevier,2006,pp. 255–325.*Model Theory of Modal Logic* - 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