Tableau-based decision procedures for logics of strategic ability in multi-agent systems

We develop decision procedures based on sound, complete, and terminating incremental tableaux for the satisfiability problem of the Alternating-time temporal logic ATL and related modal logics for reasoning about abilities of agents in multiagent systems.