Reducing Validity in Epistemic ATL to Validity in Epistemic CTL

Dimitar P. Guelev
(Institute of Mathematics and Informatics, Bulgarian Academy of Sciences)

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.

In Fabio Mogavero, Aniello Murano and Moshe Y. Vardi: Proceedings 1st International Workshop on Strategic Reasoning (SR 2013), Rome, Italy, March 16-17, 2013, Electronic Proceedings in Theoretical Computer Science 112, pp. 81–89.
Published: 1st March 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: