A complete axiom system for propositional interval temporal logic with infinite time

Simple item page
dc.contributor.authorMoszkowski, B. C.en
dc.date.accessioned2012-08-20T14:51:53Z
dc.date.available2012-08-20T14:51:53Z
dc.date.issued2012-08
dc.description.abstractInterval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the longstanding open problem of finding a complete axiom system for basic quantifier-free propositional ITL (PITL) with infinite time for analysing nonterminating computational systems. Our completeness proof uses a reduction to completeness for PITL with finite time and conventional propositional linear-time temporal logic. Unlike completeness proofs of equally expressive logics with nonelementary computational complexity, our semantic approach does not use tableaux, subformula closures or explicit deductions involving encodings of omega automata and nontrivial techniques for complementing them. We believe that our result also provides evidence of the naturalness of interval-based reasoning.en
dc.identifier.citationMoszkowski, B. (2012) A complete axiom system for propositional interval temporal logic with infinite time. Logical Methods in Computer Science, 8 (3), Paper 10, pp. 1-56en
dc.identifier.doihttps://doi.org/10.2168/LMCS-8(3:10)2012
dc.identifier.issn1860-5974
dc.identifier.urihttp://hdl.handle.net/2086/6876
dc.language.isoenen
dc.publisherTech Univ Braunschweigben
dc.researchgroupSoftware Technology Research Laboratory (STRL)en
dc.subjectInterval Temporal Logicen
dc.subjectaxiom systemen
dc.subjectaxiomatic completenessen
dc.subjectomega-regular languagesen
dc.subjectomega-regular logicsen
dc.subjectcompositionalityen
dc.titleA complete axiom system for propositional interval temporal logic with infinite timeen
dc.typeArticleen

Files

License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
3.18 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

School of Computer Science and Informatics