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 Bozianu | 1 | 5 | 1.10 |
Cătălin Dima | 2 | 186 | 17.85 |
Constantin Enea | 3 | 249 | 26.95 |