Satisfiability of Alternating-Time Temporal Epistemic Logic through Tableaux

ABSTRACT. In this paper we present a tableau-based method to decide the satisfiability of formulas in ATEL, an extension of the alternating-time temporal logic ATL including epistemic modalities for individual knowledge. Specifically, we analyse satisfiability of ATEL formulas under a number of conditions. We evaluate the impact of the assumptions of synchronicity and of a unique initial state, which have been proposed in the context of Interpreted Systems. Also, we consider satisfiability at a initial state as opposed to any state in the system. We introduce a tableau-based decision procedure for each of these combinations. Moreover, we adopt an agent-based approach to satisfiability, namely, the decision procedure returns a set of agents inducing a concurrent game structure that satisfies the specification at hand.