Cited By
View all- Kurpiewski DJamroga WKnapik MElkind EVeloso MAgmon NTaylor M(2019)STVProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3332116(2372-2374)Online publication date: 8-May-2019
On Domination and Control in Strategic Ability
Pages 197 - 205
Abstract
We propose a technique to compare partial strategies for agents and coalitions in multi-agent environments with imperfect information. The proposed relation mimics the game-theoretic notion of strategic dominance: a stronger partial strategy can replace a weaker one in a full strategy, while preserving the enforceability of a given goal. Our version of dominance is based on a new notion of input/output characteristics for partial strategies. Intuitively, the inputs are the states where the strategy gains control over execution, and the outputs are the states where it returns the control to the environment. Moreover, we identify the sources of dependence between partial strategies, and show conditions under which they can be analysed in a fully independent way. We evaluate our approach on two scalable benchmarks from the literature. The experiments are carried out for the tasks of incremental synthesis of uniform strategies and optimization of a winning strategy, with very promising results.
References
[1]
N. Alechina, B. Logan, N.H. Nga, and A. Rakib. 2009. A Logic for Coalitions with Bounded Resources. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI). 659--664.
[2]
N. Alechina, B. Logan, H.N. Nguyen, and A. Rakib. 2010. Resource-Bounded Alternating-Time Temporal Logic. Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS) . 481--488.
[3]
R. Alur, T. A. Henzinger, and O. Kupferman. 2002. Alternating-Time Temporal Logic. J. ACM, Vol. 49 (2002), 672--713.
[4]
F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, and A.V. Jones. 2017. Bisimulations for Verification of Strategic Abilities with Application to ThreeBallot Voting Protocol. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2017 . IFAAMAS, 1286--1295.
[5]
F. Belardinelli and A. Lomuscio. 2017. Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS) . ACM, 1259--1267.
[6]
M. Benedetti, A. Lallouet, and J. Vautard. 2008. Quantified Constraint Optimization. In Principles and Practice of Constraint Programming, 14th International Conference, CP 2008, Sydney, Australia, September 14--18, 2008. Proceedings (Lecture Notes in Computer Science), Vol. 5202. Springer, 463--477.
[7]
J. Bernet, D. Janin, and I. Walukiewicz. 2002. Permissive strategies: from parity games to safety games. ITA, Vol. 36, 3 (2002), 261--275.
[8]
R. Berthon, B. Maubert, A. Murano, S. Rubin, and M. Y. Vardi. 2017. Strategy Logic with Imperfect Information. In Proceedings of LICS. 1--12.
[9]
P. Bouyer, N. Markey, J. Olschewski, and M. Ummels. 2011. Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited. In Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11--14, 2011. Proceedings (Lecture Notes in Computer Science), Vol. 6996. Springer, 135--149.
[10]
T. Brazdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky. 2015. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. In Proceedings of CAV. 158--177.
[11]
T. Brazdil, K. Chatterjee, J. Kretinsky, and V. Toman. 2018. Strategy Representation by Decision Trees in Reactive Synthesis. In Proceedings of TACAS. To appear.
[12]
R. E. Bryant. 1986. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers, Vol. 35, 8 (1986), 677--691.
[13]
N. Bulling, J. Dix, and W. Jamroga. 2010. Model Checking Logics of Strategic Ability: Complexity. Specification and Verification of Multi-Agent Systems, M. Dastani, K. Hindriks, and J.-J. Meyer (Eds.). Springer, 125--159.
[14]
N. Bulling and B. Farwer. 2010a. Expressing Properties of Resource-Bounded Systems: The Logics RTL* and RTL. In Proceedings of Computational Logic in Multi-Agent Systems (CLIMA) (Lecture Notes in Computer Science), Vol. 6214. 22--45.
[15]
N. Bulling and B. Farwer. 2010b. On the (Un-)Decidability of Model Checking Resource-Bounded Agents. In Proceedings of ECAI (Frontiers in Artificial Intelligence and Applications), Vol. 215. IOS Press, 567--572.
[16]
N. Bulling and W. Jamroga. 2011. Alternating Epistemic Mu-Calculus. In Proceedings of IJCAI-11. 109--114.
[17]
Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. 1990. Symbolic Model Checking: 10^ 20 States and Beyond. In Proc. of 4th Ann. IEEE Symp. on Logic in Computer Science (LICS). IEEE Computer Society, 428--439.
[18]
S. Busard. 2017. Symbolic Model Checking of Multi-Modal Logics: Uniform Strategies and Rich Explanations . Ph.D. Dissertation. Universite Catholique de Louvain.
[19]
S. Busard, C. Pecheur, H. Qu, and F. Raimondi. 2015. Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Information and Computation, Vol. 242 (2015), 128--156.
[20]
J. Calta, D. Shkatov, and B.-H. Schlingloff. 2010. Finding Uniform Strategies for Multi-agent Systems. In Proceedings of Computational Logic in Multi-Agent Systems (CLIMA) (Lecture Notes in Computer Science), Vol. 6245. Springer, 135--152.
[21]
P. Cermak, A. Lomuscio, F. Mogavero, and A. Murano. 2014. MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. In Proc. of Computer Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 8559. Springer, 525--532.
[22]
P. Dembi'nski, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Wo'zna, and A. Zbrzezny. 2003. Verics: A Tool for Verifying Timed Automata and Estelle Specifications. Proceedings of the of the 9th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03). Lecture Notes in Computer Science, Vol. 2619. Springer, 278--283.
[23]
C. Dima, B. Maubert, and S. Pinchinat. 2015. Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus. In Proceedings of Mathematical Foundations of Computer Science (MFCS) (Lecture Notes in Computer Science), Vol. 9234. Springer, 179--191.
[24]
L. Doyen and J.-F. Raskin. 2011. Games with Imperfect Information: Theory and Algorithms. Lecture Notes in Game Theory for Computer Scientists. Cambridge University Press, 185--212.
[25]
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. 1995. Reasoning about Knowledge .MIT Press.
[26]
P. Gammie and R. van der Meyden. 2004. MCK: Model Checking the Logic of Knowledge. In Proc. of the 16th Int. Conf. on Computer Aided Verification (CAV'04) (LNCS), Vol. 3114. Springer-Verlag, 479--483.
[27]
W. Jamroga and J. Dix. 2006. Model Checking ATL$_ir$ is Indeed Δ_2^P$-complete. In Proceedings of European Workshop on Multi-Agent Systems (EUMAS) (CEUR Workshop Proceedings), Vol. 223. CEUR-WS.org.
[28]
W. Jamroga, M. Knapik, and D. Kurpiewski. 2017a. Fixpoint Approximation of Strategic Abilities under Imperfect Information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2017. IFAAMAS, 1241--1249.
[29]
W. Jamroga, M. Knapik, D. Kurpiewski, and Łukasz Mikulski. 2018. Approximate Verification of Strategic Abilities under Imperfect Information. Artificial Intelligence (2018). To appear.
[30]
W. Jamroga, V. Malvone, and A. Murano. 2017b. Reasoning about Natural Strategic Ability. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2017 . IFAAMAS, 714--722.
[31]
A. Lomuscio, H. Qu, and F. Raimondi. 2015. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems. International Journal on Software Tools for Technology Transfer (2015).
[32]
A. Lomuscio and F. Raimondi. 2006. Model Checking Knowledge, Strategies, and Games in Multi-Agent Systems. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS). 161--168.
[33]
V. Malvone, A. Murano, and L. Sorrentino. 2018. Additional Winning Strategies in Reachability Games. Fundam. Inform., Vol. 159, 1--2 (2018), 175--195.
[34]
F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. 2014. Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions on Computational Logic, Vol. 15, 4 (2014), 1--42.
[35]
F. Mogavero, A. Murano, and M.Y. Vardi. 2010. Reasoning About Strategies. In Proceedings of FSTTCS. 133--144.
[36]
D. Neider. 2011. Small Strategies for Safety Games. In Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11--14, 2011. Proceedings (Lecture Notes in Computer Science), Vol. 6996. Springer, 306--320.
[37]
J. Pilecki, M.A. Bednarczyk, and W. Jamroga. 2017. SMC: Synthesis of Uniform Strategies and Verification of Strategic Ability for Multi-Agent Systems. Journal of Logic and Computation, Vol. 27, 7 (2017), 1871--1895.
[38]
F. Raimondi and A. Lomuscio. 2007. Automatic Verification of Multi-agent Systems by Model Checking via Ordered Binary Decision Diagrams. J. Applied Logic, Vol. 5, 2 (2007), 235--251.
[39]
P. Y. Schobbens. 2004. Alternating-Time Logic with Imperfect Recall. Electronic Notes in Theoretical Computer Science, Vol. 85, 2 (2004), 82--93.
Index Terms
- On Domination and Control in Strategic Ability
Recommendations
Pretty Good Strategies and Where to Find Them
Multi-Agent SystemsAbstractSynthesis of bulletproof strategies in imperfect information scenarios is a notoriously hard problem. In this paper, we suggest that it is sometimes a viable alternative to aim at “reasonably good” strategies instead. This makes sense not only ...
STV: Model Checking for Strategies under Imperfect Information
AAMAS '19: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent SystemsWe present an experimental tool for verification of strategic abilities under imperfect information, as well as strategy synthesis. The problem is well known to be hard, both theoretically and in practice. The tool, called StraTegic Verifier (STV), ...
Knowledge-based strategies for multi-agent teams playing against Nature
AbstractWe study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2019
2518 pages
ISBN:9781450363099
- General Chairs:
- Edith Elkind,
- Manuela Veloso,
- Program Chairs:
- Noa Agmon,
- Matthew E. Taylor
Sponsors
Publisher
International Foundation for Autonomous Agents and Multiagent Systems
Richland, SC
Publication History
Published: 08 May 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- The National Centre for Research and Development Poland
Conference
AAMAS '19
Sponsor:
AAMAS '19: International Conference on Autonomous Agents and Multiagent Systems
May 13 - 17, 2019
Montreal QC, Canada
Acceptance Rates
AAMAS '19 Paper Acceptance Rate 193 of 793 submissions, 24%;
Overall Acceptance Rate 1,155 of 5,036 submissions, 23%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 53Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
Cited By
View all- Kurpiewski DJamroga WKnapik MElkind EVeloso MAgmon NTaylor M(2019)STVProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3332116(2372-2374)Online publication date: 8-May-2019
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in