Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic

PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic 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 (proj), but also past operators such as previous (-), chop in the past (˜) and since (S). 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Applied Non-Classical Logics Taylor & Francis

PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic

Download PDF
44 pages

PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic

Abstract

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...
Loading next page...
 
/lp/taylor-francis/pitl2mona-implementing-a-decision-procedure-for-propositional-interval-544J08rGXi
Publisher
Taylor & Francis
Copyright
Copyright Taylor & Francis Group, LLC
ISSN
1958-5780
eISSN
1166-3081
DOI
10.3166/jancl.14.105-148
Publisher site
See Article on Publisher Site

Abstract

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 (proj), but also past operators such as previous (-), chop in the past (˜) and since (S). 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.

Journal

Journal of Applied Non-Classical Logics – Taylor & Francis

Published: Jan 1, 2004

Keywords: Interval Temporal Logic; decision procedure; MONA; WS1S

There are no references for this article.