Reducing Validity in Epistemic ATL to Validity in Epistemic CTL

  • Guelev D
N/ACitations
Citations of this article
6Readers
Mendeley users who have this article in their library.

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.

Cite

CITATION STYLE

APA

Guelev, D. P. (2013). Reducing Validity in Epistemic ATL to Validity in Epistemic CTL. Electronic Proceedings in Theoretical Computer Science, 112, 81–89. https://doi.org/10.4204/eptcs.112.13

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free