Finite-trace linear temporal logic: Coinductive completeness

Grigore Roşu

doi:10.1007/978-3-319-46982-9_21

Finite-trace linear temporal logic: Coinductive completeness

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Runtime Verification - 16th International Conference, RV 2016, Proceedings
Editors	Yliès Falcone, César Sánchez
Publisher	Springer
Pages	333-350
Number of pages	18
ISBN (Print)	9783319469812
DOIs	https://doi.org/10.1007/978-3-319-46982-9_21
State	Published - 2016
Event	16th International Conference on Runtime Verification, RV 2016 - Madrid, Spain Duration: Sep 23 2016 → Sep 30 2016

Publication series

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

Other

Other	16th International Conference on Runtime Verification, RV 2016
Country/Territory	Spain
City	Madrid
Period	9/23/16 → 9/30/16

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-319-46982-9_21

Library availability

Discover UIUC Full Text

Cite this

Roşu, G. (2016). Finite-trace linear temporal logic: Coinductive completeness. In Y. Falcone, & C. Sánchez (Eds.), Runtime Verification - 16th International Conference, RV 2016, Proceedings (pp. 333-350). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10012 LNCS). Springer. https://doi.org/10.1007/978-3-319-46982-9_21

Finite-trace linear temporal logic: Coinductive completeness. / Roşu, Grigore.
Runtime Verification - 16th International Conference, RV 2016, Proceedings. ed. / Yliès Falcone; César Sánchez. Springer, 2016. p. 333-350 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10012 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Roşu, G 2016, Finite-trace linear temporal logic: Coinductive completeness. in Y Falcone & C Sánchez (eds), Runtime Verification - 16th International Conference, RV 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10012 LNCS, Springer, pp. 333-350, 16th International Conference on Runtime Verification, RV 2016, Madrid, Spain, 9/23/16. https://doi.org/10.1007/978-3-319-46982-9_21

Roşu G. Finite-trace linear temporal logic: Coinductive completeness. In Falcone Y, Sánchez C, editors, Runtime Verification - 16th International Conference, RV 2016, Proceedings. Springer. 2016. p. 333-350. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-46982-9_21

@inproceedings{290dad8e34d740188955c033b26ad5ec,

title = "Finite-trace linear temporal logic: Coinductive completeness",

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{\"o}del-L{\"o}b axiom. A direct decision procedure for finite-trace LTL satisfiability, a PSPACE-complete problem, is also obtained as a corollary.",

author = "Grigore Ro{\c s}u",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 16th International Conference on Runtime Verification, RV 2016 ; Conference date: 23-09-2016 Through 30-09-2016",

year = "2016",

doi = "10.1007/978-3-319-46982-9_21",

language = "English (US)",

isbn = "9783319469812",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "333--350",

editor = "Yli{\`e}s Falcone and C{\'e}sar S{\'a}nchez",

booktitle = "Runtime Verification - 16th International Conference, RV 2016, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Finite-trace linear temporal logic

T2 - 16th International Conference on Runtime Verification, RV 2016

AU - Roşu, Grigore

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84990205664&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84990205664&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-46982-9_21

DO - 10.1007/978-3-319-46982-9_21

M3 - Conference contribution

AN - SCOPUS:84990205664

SN - 9783319469812

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 333

EP - 350

BT - Runtime Verification - 16th International Conference, RV 2016, Proceedings

A2 - Falcone, Yliès

A2 - Sánchez, César

PB - Springer

Y2 - 23 September 2016 through 30 September 2016

ER -

Finite-trace linear temporal logic: Coinductive completeness

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this