Skip to main content

A MONA-based Decision Procedure for Propositional Interval Temporal Logic

Gomez, Rodolfo and Bowman, Howard (2003) A MONA-based Decision Procedure for Propositional Interval Temporal Logic. Other. Kent University, Vienna, Austria (Unpublished) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL
http://www.cs.kent.ac.uk/pubs/2003/1624

Abstract

Interval Temporal Logic (ITL) is a finite-time linear temporal logic with applications in hardware verifi-

elementary complexity of its decision problem, efficient ITL-based verification tools have been difficult to de-

efficient automata-based decision procedure for the logic WS1S. Despite the non-elementary complexity of

theorem proving. We have developed a new semantics for PITL based on WS1S formulas, which led us to an

efficiency of the decision procedure is a direct consequence of the many optimisations included in MONA (e.g.

of a decision procedure for PITL with projection, and the first one based on automata.

Item Type: Monograph (Other)
Additional information: Workshop of Interval Temporal Logics and Duration Calculi (part of the 15th European Summer School in Logic, Language and Information
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:00 UTC
Last Modified: 09 Feb 2020 04:01 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/13933 (The current URI for this page, for reference purposes)
Bowman, Howard: https://orcid.org/0000-0003-4736-1869
  • Depositors only (login required):