Finite-trace linear temporal logic: Coinductive completeness

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Linear temporal logic (LTL) is suitable not only for infinitetrace systems, but also for finite-trace systems. Indeed, LTL is frequently used as a trace specification formalism in runtime verification. 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 Gödel-Löb axiom. A direct decision procedure for finite-trace LTL satisfiability, a PSPACE-complete problem, is also obtained as a corollary.

Original languageEnglish (US)
Title of host publicationRuntime Verification - 16th International Conference, RV 2016, Proceedings
EditorsYliès Falcone, César Sánchez
PublisherSpringer
Pages333-350
Number of pages18
ISBN (Print)9783319469812
DOIs
StatePublished - 2016
Event16th International Conference on Runtime Verification, RV 2016 - Madrid, Spain
Duration: Sep 23 2016Sep 30 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10012 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other16th International Conference on Runtime Verification, RV 2016
Country/TerritorySpain
CityMadrid
Period9/23/169/30/16

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Finite-trace linear temporal logic: Coinductive completeness'. Together they form a unique fingerprint.

Cite this