Reasoning about Strategic Abilities: Agents wit h Truly Perfect Recall

被引:0
作者
Bulling, Nils [1 ]
Jamroga, Wojciech [2 ]
Popovici, Matei [3 ]
机构
[1] Tech Univ Clausthal, Dept Informat, Julius Albert Str 4, D-38678 Clausthal Zellerfeld, Germany
[2] Polish Acad Sci, Inst Comp Sci, 5 Jana Kazimierza Str, PL-01248 Warsaw, Poland
[3] Univ Politehn Bucuresti, Splaiul Independentei 313, Bucharest, Romania
基金
欧盟第七框架计划;
关键词
Alternating-Time temporal logic; perfect-recall semantics; MODEL-CHECKING; KNOWLEDGE; LOGIC; ATL;
D O I
10.1145/3309761
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus, effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past. In this article, we investigate the alternative semantics for ATL* where the past is not forgotten in nested games. We show that the standard semantics of ATL* coincides with the "truly perfect recall" semantics for agents with perfect information and in case of so-called "objective" abilities under uncertainty. On the other hand, the two semantics differ significantly for the most popular ("subjective") notion of ability under imperfect information. The same applies to the standard vs. "truly perfect recall" semantics of ATL* with persistent strategies. We compare the relevant variants of ATL* by looking at their expressive power, sets of validities, and tractability of model checking.
引用
收藏
页数:46
相关论文
共 76 条
  • [1] A logic of strategic ability under bounded memory
    Ågotnes T.
    Walther D.
    [J]. Journal of Logic, Language and Information, 2009, 18 (1) : 55 - 77
  • [2] Action and knowledge in alternating-time temporal logic
    Ågotnes, T
    [J]. SYNTHESE, 2006, 149 (02) : 121 - 153
  • [3] Alechina N., 2009, P LOG AG MOB LAM 09
  • [4] ALECHINA N, 2004, P 3 INT JOINT C AUT, P606, DOI [10.1109/AAMAS.2004.10090, DOI 10.1109/AAMAS.2004.10090]
  • [5] Model-checking for Resource-Bounded ATL with production and consumption of resources
    Alechina, Natasha
    Logan, Brian
    Hoang Nga Nguyen
    Raimondi, Franco
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2017, 88 : 126 - 144
  • [6] Logic for coalitions with bounded resources1
    Alechina, Natasha
    Logan, Brian
    Hoang Nga Nguyen
    Rakib, Abdur
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2011, 21 (06) : 907 - 937
  • [7] Alternating-time temporal logic
    Alur, R
    Henzinger, TA
    Kupferman, O
    [J]. 38TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 1997, : 100 - 109
  • [8] Alternating-time temporal logic
    Alur, R
    Henzinger, TA
    Kupferman, O
    [J]. JOURNAL OF THE ACM, 2002, 49 (05) : 672 - 713
  • [9] JMOCHA: A model checking tool that exploits design structure
    Alur, R
    De Alfaro, L
    Grosu, R
    Henzinger, TA
    Kang, M
    Kirsch, CM
    Majumdar, R
    Mang, F
    Wang, BY
    [J]. PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2001, : 835 - 836
  • [10] [Anonymous], 2007, P TARK 2007, DOI DOI 10.1145/1324249.1324256