Difference between revisions of "Finite-Trace Linear Temporal Logic: Coinductive Completeness"

From FSL
Jump to: navigation, search
(Created page with "<pubbib id='rosu-2013-mfcs-submission' template='PubDefaultWithAbstractAndTitle'/>")
(One intermediate revision by one user not shown)
Line 1: Line 1:
<pubbib id='rosu-2016-rv' template='PubDefaultWithAbstractAndTitle'/>
=== Submission MFCS 2013 ===
<pubbib id='rosu-2013-mfcs-submission' template='PubDefaultWithAbstractAndTitle'/>
<pubbib id='rosu-2013-mfcs-submission' template='PubDefaultWithAbstractAndTitle'/>

Latest revision as of 23:20, 1 October 2016

Finite-Trace Linear Temporal Logic: Coinductive Completeness
Grigore Rosu
RV'16, LNCS 10012, pp 333-350. 2016
Abstract. Linear temporal logic (LTL) is suitable not only for infinite-trace systems, but also for finite-trace systems. The completeness of LTL with only infinite or with both infinite and finite traces has been extensively studied, but similar direct results for LTL with only finite traces are missing. This paper proposes a sound and complete proof system for finite-trace LTL. The axioms and proof rules are natural and expected, except for one rule of coinductive nature, reminiscent of the Goedel-Loeb axiom. A direct decision procedure for finite-trace LTL satisfiability, a PSPACE-complete problem, is also obtained as a corollary.
PDF, Slides(PPTX), Matching Logic, DOI, RV'16, BIB

Personal tools