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

2013/10/23 by Bozianu, Rodica, Dima, Catalin, Enea, Constantin
#Computer Science and Game Theory (cs.GT) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1310.6434

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.

Related

• Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
• Certification for mu-calculus with winning strategies
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
• Approximating Strategic Abilities under Imperfect Information: a Naive\n Approach