Completeness of a Branching-Time Logic with Possible Choices

被引:0
|
作者
Roberto Ciuni
Alberto Zanardo
机构
[1] Delft University of Technology,Department of Philosophy
[2] University of Padova,Department of Pure and Applied Mathematics
来源
Studia Logica | 2010年 / 96卷
关键词
Branching-Time; Agency; Choices; Completeness; BTC;
D O I
暂无
中图分类号
学科分类号
摘要
In this paper we present BTC, which is a complete logic for branchingtime whose modal operator quantifies over histories and whose temporal operators involve a restricted quantification over histories in a given possible choice. This is a technical novelty, since the operators of the usual logics for branching-time such as CTL express an unrestricted quantification over histories and moments. The value of the apparatus we introduce is connected to those logics of agency that are interpreted on branching-time, as for instance Stit Logics.
引用
收藏
页码:393 / 420
页数:27
相关论文
共 50 条
  • [31] Model Checking for Real-time Branching-time Temporal Logic Based on Temporal Testers
    Luo X.-Y.
    Huang X.-Y.
    Gu T.-L.
    Su K.-L.
    Chen Z.-X.
    Zheng L.-X.
    Ruan Jian Xue Bao/Journal of Software, 2022, 33 (08): : 2930 - 2946
  • [32] Branching-time logics and fairness, revisited
    Latte, Markus
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2021, 31 (09) : 1135 - 1144
  • [33] SATISFIABILITY GAMES FOR BRANCHING-TIME LOGICS
    Friedmann, Oliver
    Latte, Markus
    Lange, Martin
    LOGICAL METHODS IN COMPUTER SCIENCE, 2013, 9 (04)
  • [34] "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis
    Gustavo Arellano
    Julián Argil
    Eugenio Azpeitia
    Mariana Benítez
    Miguel Carrillo
    Pedro Góngora
    David A Rosenblueth
    Elena R Alvarez-Buylla
    BMC Bioinformatics, 12
  • [35] On the expressive power of hybrid branching-time logics
    Kernberger, Daniel
    Lange, Martin
    THEORETICAL COMPUTER SCIENCE, 2020, 813 : 362 - 374
  • [36] Satisfying a fragment of XQuery by branching-time reduction
    Halle, Sylvain
    Villemaire, Roger
    TIME 2008: 15TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2008, : 72 - 76
  • [37] Branching-time logics repeatedly referring to states
    Weber V.
    Journal of Logic, Language and Information, 2009, 18 (4) : 593 - 624
  • [38] Which branching-time properties are effectively linear?
    Grumberg, O
    Kurshan, RP
    JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (02) : 201 - 228
  • [39] Oracle circuits for branching-time model checking
    Schnoebelen, P
    AUTOMATA, LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2003, 2719 : 790 - 801
  • [40] Stochastic games with branching-time winning objectives
    Brazdil, Tomas
    Brozek, Vaclav
    Forejt, Vojtech
    Kucera, Antonin
    21ST ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2006, : 349 - +