Decidable Model Checking with Uniform Strategies

Alechina, Natasha; Logan, Brian; Dastani, Mehdi

Abstract

The logic of strategic ability Resource-Bounded Alternating Time Syntactic Epistemic Logic (RB+-ATSEL) has a decidable model-checking problem for coalition uniform strategies. A strategy is coalition uniform if agents in a coalition select the same joint action in all states where the knowledge of the coalition is the same. However, this presupposes free and unbounded communication between the agents in the coalition before every action selection. In this paper we present a modified version of RB+-ATSEL, RB+-ATSELc, with explicit (and explicitly costed) communication actions. RB+-ATSELc is interpreted on communication models which have an explicit communication step before every action selection. We show that, unlike standard ATL under imperfect information, the model checking problem for RB+-ATSELc is decidable under perfect recall uniform strategies. Our decidability result also applies to ATL with imperfect information and perfect recall when interpreted on communication models.

Citation

Alechina, N., Logan, B., & Dastani, M. (2019). Decidable Model Checking with Uniform Strategies. In Proceedings of the 18th International Conference on Autonomous Agent and MultiAgent Systems, AAMAS '19, 170--178

• Conference Name: 18th International Conference on Autonomous Agent and MultiAgent Systems, AAMAS '19
• Start Date: May 13, 2019
• End Date: May 17, 2019
• Acceptance Date: Jan 23, 2019
• Publication Date: May 13, 2019
• Deposit Date: Jun 14, 2019
• Publisher: Association for Computing Machinery (ACM)
• Pages: 170--178
• Book Title: Proceedings of the 18th International Conference on Autonomous Agent and MultiAgent Systems, AAMAS '19
• ISBN: 978-1-4503-6309-9
• Public URL: https://nottingham-repository.worktribe.com/output/2173876
• Publisher URL: https://dl.acm.org/citation.cfm?id=3331690