Model Checking Abilities of Agents: A Closer Look

摘要

Alternating-time temporal logic (atl) is a logic for reasoning about open computational systems and multi-agent systems. It is well known that ATL model checking is linear in the size of the model. We point out, however, that the size of an ATL model is u