文章基本信息

标题：ATL with Strategy Contexts: Expressiveness and Model Checking
本地全文：下载
作者：Arnaud Da Costa ; Fran{\c{c}}ois Laroussinie ; Nicolas Markey 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2010
卷号：8
页码：120-132
DOI：10.4230/LIPIcs.FSTTCS.2010.120
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we~prove that their model-checking problems remain decidable by~designing a tree-automata-based algorithm for model-checking ATLsc* on the full class of $n$-player concurrent game structures.
关键词：alternating temporal logic; agent; strategy quantifier