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

TL;DR

This paper introduces an incremental tableau-based decision procedure for ATL and its variants, which is theoretically sound, practically efficient, and adaptable to different logic variants in multi-agent systems.

Contribution

The paper presents a new tableau-based decision procedure for ATL that is both efficient in practice and easily adaptable to variants, improving upon existing methods.

Findings

The procedure operates within the established complexity bounds.

It demonstrates better average-case efficiency than existing decision procedures.

It is flexible and adaptable to various ATL variants.

Abstract

We develop an incremental tableau-based decision procedures for the Alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we claim that our tableau is practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure.