Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

Abstract

We identify a subproblem of the model-checking problem for the epistemic μ-calculus which is decidable. Formulas in the instances of this subproblem allow free variables within the scope of epistemic modalities in a restricted form that avoids embodying any form of common knowledge. Our subproblem subsumes known decidable fragments of epistemic CTL/LTL, may express winning strategies in two-player games with one player having imperfect information and non-observable objectives, and, with a suitable encoding, decidable instances of the model-checking problem for ATLiR.

10 pages, Poster presentation at TARK 2013 (arXiv:1310.6382) http://www.tark.org

References in corpus (2)

• Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
• Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

Cited by in corpus (2)

• Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
• Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics