A Probabilistic Temporal Epistemic Logic: Strong Completeness

被引:4
|
作者
Ognjanovic, Zoran [1 ]
Stepic, Angelina Ilic [1 ]
Perovic, Aleksandar [2 ]
机构
[1] Serbian Acad Arts & Sci, Math Inst, Belgrade 11000, Serbia
[2] Univ Belgrade, Fac Transport & Traff Engn, Belgrade 11000, Serbia
关键词
DECIDABILITY; KNOWLEDGE;
D O I
10.1093/jigpal/jzac072
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
The paper offers a formalization of reasoning about distributed multi-agent systems. The presented propositional probabilistic temporal epistemic logic PTEL is developed in full detail: syntax, semantics, soundness and strong completeness theorems. As an example, we prove consistency of the blockchain protocol with respect to the given set of axioms expressed in the formal language of the logic. We explain how to extend PTEL to axiomatize the corresponding first-order logic.
引用
收藏
页码:94 / 138
页数:45
相关论文
共 50 条
  • [41] Temporal probabilistic logic programs
    Dekhtyar, A
    Dekhtyar, MI
    Subrahmanian, VS
    LOGIC PROGRAMMING: PROCEEDINGS OF THE 1999 INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING, 1999, : 109 - 123
  • [42] Focus games for satisfiability and completeness of temporal logic
    Lange, M
    Stirling, C
    16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, : 357 - 365
  • [43] COMPLETENESS OF TEMPORAL AND SPATIAL LOGIC ETSL.
    Iwanuma, Koji
    Harao, Masateru
    Noguchi, Shoichi
    Systems and Computers in Japan, 1987, 18 (06) : 1 - 14
  • [44] A hierarchical completeness proof for propositional temporal logic
    Moszkowski, B
    VERIFICATION: THEORY AND PRACTICE: ESSAYS DEDICATED TO ZHOAR MANNA ON THE OCCASION OF HIS 64TH BIRTHDAY, 2003, 2772 : 480 - 523
  • [45] Supervisory Control Theory in Epistemic Temporal Logic
    Aucher, Guillaume
    AAMAS'14: PROCEEDINGS OF THE 2014 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2014, : 333 - 340
  • [46] Dynamic epistemic logic with branching temporal structures
    Hoshi, Tomohiro
    Yap, Audrey
    SYNTHESE, 2009, 169 (02) : 259 - 281
  • [47] Parallel Model Checking for Temporal Epistemic Logic
    Kwiatkowska, Marta
    Lomuscio, Alessio
    Qu, Hongyang
    ECAI 2010 - 19TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2010, 215 : 543 - 548
  • [48] Automata for Epistemic Temporal Logic with Synchronous Communication
    Mohalik S.
    Ramanujam R.
    Journal of Logic, Language and Information, 2010, 19 (4) : 451 - 484
  • [49] Dynamic epistemic logic with branching temporal structures
    Tomohiro Hoshi
    Audrey Yap
    Synthese, 2009, 169 : 259 - 281
  • [50] A strong completeness theorem in intuitionistic quantified modal logic
    Hengshan Gao
    Science in China Series E: Technological Sciences, 2000, 43 : 60 - 70