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

TL;DR

This paper identifies a decidable subproblem in model checking for an epistemic mu-calculus, enabling analysis of certain knowledge-based properties and strategies in multi-agent systems.

Contribution

It introduces a new decidable fragment of the epistemic mu-calculus that avoids common knowledge, extending known decidable cases and applications.

Findings

Subproblem is decidable and encompasses known fragments.

Can express winning strategies with imperfect information.

Applicable to model-checking in multi-agent systems.

Abstract

We identify a subproblem of the model-checking problem for the epistemic \mu-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.