Reducing Validity in Epistemic ATL to Validity in Epistemic CTL

TL;DR

This paper presents a translation method from a subset of epistemic ATL to epistemic CTL, enabling the use of existing CTL techniques to decide validity in ATL, which is otherwise computationally challenging.

Contribution

It introduces a validity-preserving translation from a subset of epistemic ATL to epistemic CTL, facilitating automated deduction for ATL validity problems.

Findings

Decidability of validity in the subset of epistemic ATL

Translation preserves validity between ATL and CTL

Enables use of CTL techniques for ATL validity checking

Abstract

We propose a validity preserving translation from a subset of epistemic Alternating-time Temporal Logic (ATL) to epistemic Computation Tree Logic (CTL). The considered subset of epistemic ATL is known to have the finite model property and decidable model-checking. This entails the decidability of validity but the implied algorithm is unfeasible. Reducing the validity problem to that in a corresponding system of CTL makes the techniques for automated deduction for that logic available for the handling of the apparently more complex system of ATL.