No big deal: introducing roles to reduce the size of ATL models

TL;DR

This paper introduces a role-based semantics for ATL, reducing model complexity by assigning agents to roles, and demonstrates its advantages, complexity analysis, and equivalence to standard ATL semantics.

Contribution

It presents a novel role-based semantics for ATL, improving model checking efficiency and establishing equivalence with traditional semantics.

Findings

Role-based semantics simplifies ATL models

Model checking complexity is analyzed and optimized

Equivalence with standard ATL semantics is proven

Abstract

In the following paper we present a new semantics for the well-known strategic logic ATL. It is based on adding roles to concurrent game structures, that is at every state, each agent belongs to exactly one role, and the role specifies what actions are available to him at that state. We show advantages of the new semantics, analyze model checking complexity and prove equivalence between standard ATL semantics and our new approach.