Non-axiomatizability for the linear temporal logic of knowledge with concrete observability

被引:1
|
作者
Dima, Catalin [1 ]
机构
[1] Univ Paris Est Creteil Val de Marne, LACL, F-94010 Creteil, France
关键词
Temporal epistemic logics; undecidability; MODEL CHECKING;
D O I
10.1093/logcom/exq031
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We show that propositional linear temporal logic with knowledge modalities but without common knowledge has an undecidable satisfiability problem when interpreted in a 'concrete' semantics with perfect recall or with perfect recall and synchrony.We then conclude that this concrete semantics is not axiomatizable in the semantics, based on local states.
引用
收藏
页码:939 / 958
页数:20
相关论文
共 50 条
  • [41] A tableau for general linear temporal logic
    Reynolds, Mark Alexander
    JOURNAL OF LOGIC AND COMPUTATION, 2013, 23 (05) : 1057 - 1080
  • [42] Temporal Reference in Linear Tense Logic
    M. J. Cresswell
    Journal of Philosophical Logic, 2010, 39 : 173 - 200
  • [43] A Quantitative Approach for Linear Temporal Logic
    Shi, Hui-Xian
    QUANTITATIVE LOGIC AND SOFT COMPUTING 2016, 2017, 510 : 49 - 57
  • [44] Regular Linear Temporal Logic with Past
    Sanchez, Cesar
    Leucker, Martin
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2010, 5944 : 295 - +
  • [45] Linear temporal logic and finite semigroups
    Wilke, T
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2001, 2001, 2136 : 96 - 110
  • [46] Fuzzy Time in Linear Temporal Logic
    Frigeri, Achille
    Pasquale, Liliana
    Spoletini, Paola
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (04)
  • [47] Query Checking for Linear Temporal Logic
    Huang, Samuel
    Cleaveland, Rance
    CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION (FMICS-AVOCS 2017), 2017, 10471 : 34 - 48
  • [48] Vectorial languages and linear temporal logic
    Serre, O
    THEORETICAL COMPUTER SCIENCE, 2004, 310 (1-3) : 79 - 116
  • [49] A Parallel Linear Temporal Logic Tableau
    McCabe-Dansted, John C.
    Reynolds, Mark
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (256): : 166 - 179
  • [50] On the Translation of Automata to Linear Temporal Logic
    Boker, Udi
    Lehtinen, Karoliina
    Sickert, Salomon
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2022), 2022, 13242 : 140 - 160