Title
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 \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.
Year
Venue
Field
2013
TARK
Model checking,Free variables and bound variables,Decidability,Common knowledge,Epistemology,Perfect information,Recall,Calculus,Semantics,Mathematics,Encoding (memory)
DocType
Volume
Citations 
Journal
abs/1310.6434
3
PageRank 
References 
Authors
0.39
19
3
Name
Order
Citations
PageRank
Rodica Bozianu151.10
Cătălin Dima218617.85
Constantin Enea324926.95