Skip to main content

PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic

Gomez, Rodolfo, Bowman, Howard (2004) PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic. Journal of Applied Non-Classical Logics, 14 (1-2). pp. 105-148. ISSN 1166-3081. (doi:10.3166/jancl.14.105-148) (KAR id:14032)

Language: English
Click to download this file (303kB) Preview
[thumbnail of PITL2MONA_Implementing_a_Decision.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Interval Temporal Logic (ITL) 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.

Item Type: Article
DOI/Identification number: 10.3166/jancl.14.105-148
Additional information: Issue on Interval Temporal Logics and Duration Calculi. V. Goranko and A. Montanari guest eds.
Uncontrolled keywords: Interval Temporal Logic, decision procedure, MONA, WS1S
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01 UTC
Last Modified: 09 Mar 2023 11:29 UTC
Resource URI: (The current URI for this page, for reference purposes)
Bowman, Howard:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.