Finite-Trace Linear Temporal Logic: Coinductive Completeness

被引：0
|
作者：
Rosu, Grigore [1 ]
机构：
[1] Univ Illinois, Champaign, IL 61820 USA
来源：
RUNTIME VERIFICATION, (RV 2016) | 2016年 / 10012卷
关键词：
SEMANTICS; LTL;
D O I：
10.1007/978-3-319-46982-9_21
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Linear temporal logic (LTL) is suitable not only for infinite-trace 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 Godel-Lob axiom. A direct decision procedure for finite-trace LTL satisfiability, a PSPACE-complete problem, is also obtained as a corollary.
引用
收藏
页码：333 / 350
页数：18
相关论文
共 50 条
  • [1] Finite-trace linear temporal logic: coinductive completeness
    Rosu, Grigore
    FORMAL METHODS IN SYSTEM DESIGN, 2018, 53 (01) : 138 - 163
  • [2] Finite-trace linear temporal logic: coinductive completeness
    Grigore Roşu
    Formal Methods in System Design, 2018, 53 : 138 - 163
  • [3] Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
    Ben Greenman
    Prasad, Siddhartha
    Di Stasio, Antonio
    Zhu, Shufang
    De Giacomo, Giuseppe
    Krishnamurthi, Shriram
    Montali, Marco
    Nelson, Tim
    Zizyte, Milda
    FORMAL METHODS, PT I, FM 2024, 2025, 14933 : 579 - 599
  • [4] Finite-trace and generalized-reactivity specifications in temporal synthesis
    Giuseppe De Giacomo
    Antonio Di Stasio
    Lucas M. Tabajara
    Moshe Y. Vardi
    Shufang Zhu
    Formal Methods in System Design, 2022, 61 : 139 - 163
  • [5] ?????????????????????Finite-trace and generalized-reactivity specifications in temporal synthesis
    De Giacomo, Giuseppe
    Di Stasio, Antonio
    Tabajara, Lucas M.
    Vardi, Moshe Y.
    Zhu, Shufang
    FORMAL METHODS IN SYSTEM DESIGN, 2022, 61 (2-3) : 139 - 163
  • [6] Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
    De Giacomo, Giuseppe
    Di Stasio, Antonio
    Tabajara, Lucas M.
    Vardi, Moshe
    Zhu, Shufang
    PROCEEDINGS OF THE THIRTIETH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, IJCAI 2021, 2021, : 1852 - 1858
  • [7] Unified Classical Logic Completeness A Coinductive Pearl
    Blanchette, Jasmin Christian
    Popescu, Andrei
    Traytel, Dmitriy
    AUTOMATED REASONING, IJCAR 2014, 2014, 8562 : 46 - 60
  • [8] Linear temporal logic and finite semigroups
    Wilke, T
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2001, 2001, 2136 : 96 - 110
  • [9] Weak Completeness Theorem for Propositional Linear Time Temporal Logic
    Giero, Mariusz
    FORMALIZED MATHEMATICS, 2012, 20 (03): : 227 - 234
  • [10] Applications of Finite Linear Temporal Logic to Piecewise Linear Aggregates
    Pranevicius, Henrikas
    Norgela, Stanislovas
    INFORMATICA, 2012, 23 (03) : 427 - 441
12345