TY - JOUR
T1 - Finite-trace linear temporal logic
T2 - coinductive completeness
AU - Roşu, Grigore
N1 - Funding Information:
Acknowledgements We would like to warmly thank Yliès Falcone and César Sánchez for organizing the RV’16 conference, and them as well as Martin Steffen and Fred Schneider for lively discussions and debates related to the Coinduction proof rule. We also thank Moshe Vardi for referring us to recent work on finite-trace LTL published in artificial intelligence conferences [10–12,25,48]; we were not aware of these efforts when we published the RV’16 conference version of this paper [35]. Special thanks to my student Xiaohong Chen, who helped double-check the correctness of the proofs and the appropriateness of the results. Last but not least, we would like to warmly thank the anonymous reviewers for substantial suggestions on how to improve this paper. The work presented in this paper was supported in part by NSF Grants CCF-1421575 and CNS-1619275, and by an IOHK gift (http://iohk.io).
Publisher Copyright:
© 2018, Springer Science+Business Media, LLC, part of Springer Nature.
PY - 2018/8/1
Y1 - 2018/8/1
N2 - Linear temporal logic (LTL) is suitable not only for infinite-trace systems, but also for finite-trace systems. In particular, LTL with finite-trace semantics is frequently used as a specification formalism in runtime verification, in artificial intelligence, and in business process modeling. The satisfiability of LTL with finite-trace semantics, a known PSPACE-complete problem, has been recently studied and both indirect and direct decision procedures have been proposed. However, the proof theory of LTL with finite traces is not that well understood. Specifically, complete proof systems of LTL with only infinite or with both infinite and finite traces have been proposed in the literature, but complete proof systems directly for LTL with only finite traces are missing. The only known results are indirect, by translation to other logics, e.g., infinite-trace LTL. This paper proposes a direct 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.
AB - Linear temporal logic (LTL) is suitable not only for infinite-trace systems, but also for finite-trace systems. In particular, LTL with finite-trace semantics is frequently used as a specification formalism in runtime verification, in artificial intelligence, and in business process modeling. The satisfiability of LTL with finite-trace semantics, a known PSPACE-complete problem, has been recently studied and both indirect and direct decision procedures have been proposed. However, the proof theory of LTL with finite traces is not that well understood. Specifically, complete proof systems of LTL with only infinite or with both infinite and finite traces have been proposed in the literature, but complete proof systems directly for LTL with only finite traces are missing. The only known results are indirect, by translation to other logics, e.g., infinite-trace LTL. This paper proposes a direct 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.
KW - Coinduction
KW - Complete deduction
KW - Linear temporal logic
KW - Satisfiability
UR - http://www.scopus.com/inward/record.url?scp=85049101192&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85049101192&partnerID=8YFLogxK
U2 - 10.1007/s10703-018-0321-3
DO - 10.1007/s10703-018-0321-3
M3 - Article
AN - SCOPUS:85049101192
SN - 0925-9856
VL - 53
SP - 138
EP - 163
JO - Formal Methods in System Design
JF - Formal Methods in System Design
IS - 1
ER -