2013/03/04 by Dimitar P. Guelev
Computer Science · #cs.LO #cs.AI #cs.MA
paper · pdf · doi:10.4204/eptcs.112.13
published as EPTCS 112, 2013, pp. 81-89 · In Proceedings SR 2013, arXiv:1303.0071
arxiv created 2013/03/04 · arxiv updated 2013/03/05
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.