Abstract: Halpern and Shoham's modal logic of time intervals (HS in short) is an elegant and highly influential propositional interval-based logic. Its Horn fragments and their hybrid extensions have been recently intensively studied and successfully applied in real-world use cases. Detailed investigation of their decidability and computational complexity has been conducted, however, there has been significantly less research on their expressive power. In this paper we make a step towards filling this gap. We (1) show what time structures are definable in the language of HS, and (2) determine which HS fragments are capable of expressing: hybrid machinery, i.e., nominals and satisfaction operators, and somewhere, difference, and everywhere modal operators. These results enable us to classify HS Horn fragments according to their expressive power and to gain insight in the interplay between their decidability/computational complexity and expressiveness.
@InProceedings{walega:LIPIcs.TIME.2017.22, author = {Walega, Przemyslaw Andrzej}, title = {{On Expressiveness of Halpern-Shoham Logic and its Horn Fragments}}, booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-052-1}, ISSN = {1868-8969}, year = {2017}, volume = {90}, editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.22}, URN = {urn:nbn:de:0030-drops-79307}, doi = {10.4230/LIPIcs.TIME.2017.22}, annote = {Keywords: Temporal Logic, Interval Logic, Expressiveness, Hybrid Logic} }
Feedback for Dagstuhl Publishing