PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic

Journal of Applied Non-Classical Logics 14 (1-2):105-148 (2004)
  Copy   BIBTEX


Interval Temporal Logic is a finite-time linear temporal logic with applications in hardware verification, temporal logic programming and specification of multimedia documents. Due to the logic's non-elementary complexity, efficient ITL-based verification tools have been difficult to develop, even for propositional subsets. MONA is an efficient implementation of an automata-based decision procedure for the logic WS1S. Despite the non-elementary complexity of WS1S, MONA has been successfully applied in problems such as hardware synthesis, protocol verification and theorem proving. Here we consider a rich propositional subset of ITL, PITL, whose expressive power is equivalent to that of WS1S, and in turn to that of regular languages. PITL not only includes operators such as chop, star and projection, but also past operators such as previous, chop in the past and since. We provide an interpretation of PITL formulas in WS1S, which led us to a direct translation from PITL formulas to MONA specifications. We present the tool PITL2MONA as an implementation of such translation. With PITL2MONA acting as a front-end, MONA is used as a decision procedure for PITL. To our knowledge, this is one of the few implementations of a decision procedure for PITL, the first one based on automata, and the only one which handles both projection and past operators. We have tested our implementation on a number of examples; we show in this paper the application of PITL and its MONA-based decision procedure in solutions to the dining-philosophers and a multimedia synchronisation problem, together with some experimental results on these and some other examples.



    Upload a copy of this work     Papers currently archived: 92,100

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
Calendar Logic.Hans Jürgen Ohlbach & Dov Gabbay - 1998 - Journal of Applied Non-Classical Logics 8 (4):291-323.
Relational dual tableaux for interval temporal logics.David Bresolin, Joanna Golinska-Pilarek & Ewa Orlowska - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):251–277.
A Decision Procedure for Evaluating Natural Language Arguments.Moti Mizrahi - 2012 - APA Newsletter on Teaching Philosophy 12 (1):11-12.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
Adding a temporal dimension to a logic system.Marcelo Finger & Dov M. Gabbay - 1992 - Journal of Logic, Language and Information 1 (3):203-233.
A decision procedure for Fitch's propositional calculus.Richmond H. Thomason - 1967 - Notre Dame Journal of Formal Logic 8 (1-2):101-117.
Interval-Related Interpolation in Interval Temporal Logics.Dimitar Guelev - 2001 - Logic Journal of the IGPL 9 (5):677-685.
A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic.Kosta Došen - 1987 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 33 (5):453-456.
Completeness of S4 for the Lebesgue Measure Algebra.Tamar Lando - 2012 - Journal of Philosophical Logic 41 (2):287-316.
Concerted instant-interval temporal semantics. I. Temporal ontologies.Alexander Bochman - 1990 - Notre Dame Journal of Formal Logic 31 (3):403-414.


Added to PP

78 (#213,917)

6 months
2 (#1,203,099)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Add more references