Skip to main content

Research Repository

Advanced Search

Decidable Model Checking with Uniform Strategies

Alechina, Natasha; Logan, Brian; Dastani, Mehdi

Authors

Natasha Alechina

Brian Logan

Mehdi Dastani



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
Publicly Available Date
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