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

From FSL

Line 1: | Line 1: | ||

<pubbib id='rosu-2016-rv' template='PubDefaultWithAbstractAndTitle'/> | <pubbib id='rosu-2016-rv' template='PubDefaultWithAbstractAndTitle'/> | ||

+ | <private> | ||

+ | === Submission MFCS 2013 === | ||

<pubbib id='rosu-2013-mfcs-submission' template='PubDefaultWithAbstractAndTitle'/> | <pubbib id='rosu-2013-mfcs-submission' template='PubDefaultWithAbstractAndTitle'/> | ||

+ | </private> |

## Latest revision as of 23:19, 1 October 2016

**Finite-Trace Linear Temporal Logic: Coinductive Completeness**- Grigore Rosu
, LNCS 10012, pp 333-350. 2016**RV'16**

*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