Model checking an epistemic μ-calculus with synchronous and perfect recall semantics

Rodica Bozianu; Cǎtǎlin Dima; Constantin Enea

Model checking an epistemic _μ-calculus with synchronous and perfect recall semantics

Rodica Bozianu
, Cǎtǎlin Dima
, Constantin Enea

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 ATL_iR.

Original language	English
Title of host publication	Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013
Editors	Burkhard C. Schipper
Publisher	Institute of Mathematical Sciences
Pages	176-185
Number of pages	10
ISBN (Electronic)	9780615747163
Publication status	Published - 1 Jan 2013
Externally published	Yes
Event	14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013 - Chennai, India Duration: 7 Jan 2013 → 9 Jan 2013

Publication series

Name	Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013

Conference

Conference	14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013
Country/Territory	India
City	Chennai
Period	7/01/13 → 9/01/13

Cite this

Bozianu, R., Dima, C., & Enea, C. (2013). Model checking an epistemic _μ-calculus with synchronous and perfect recall semantics. In B. C. Schipper (Ed.), Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013 (pp. 176-185). (Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013). Institute of Mathematical Sciences.

Bozianu, Rodica ; Dima, Cǎtǎlin ; Enea, Constantin. / Model checking an epistemic _μ-calculus with synchronous and perfect recall semantics. Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013. editor / Burkhard C. Schipper. Institute of Mathematical Sciences, 2013. pp. 176-185 (Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013).

@inproceedings{3a7eeca03adb46e69ae1e87129371a0a,

title = "Model checking an epistemic μ-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.",

author = "Rodica Bozianu and Cǎtǎlin Dima and Constantin Enea",

year = "2013",

month = jan,

day = "1",

language = "English",

series = "Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013",

publisher = "Institute of Mathematical Sciences",

pages = "176--185",

editor = "Schipper, \{Burkhard C.\}",

booktitle = "Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013",

}

Bozianu, R, Dima, C & Enea, C 2013, Model checking an epistemic _μ-calculus with synchronous and perfect recall semantics. in BC Schipper (ed.), Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013. Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013, Institute of Mathematical Sciences, pp. 176-185, 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013, Chennai, India, 7/01/13.

Model checking an epistemic _μ-calculus with synchronous and perfect recall semantics. / Bozianu, Rodica; Dima, Cǎtǎlin; Enea, Constantin.
Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013. ed. / Burkhard C. Schipper. Institute of Mathematical Sciences, 2013. p. 176-185 (Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Model checking an epistemic μ-calculus with synchronous and perfect recall semantics

AU - Bozianu, Rodica

AU - Dima, Cǎtǎlin

AU - Enea, Constantin

PY - 2013/1/1

Y1 - 2013/1/1

N2 - 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.

AB - 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.

M3 - Conference contribution

AN - SCOPUS:85087097086

T3 - Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013

SP - 176

EP - 185

BT - Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013

A2 - Schipper, Burkhard C.

PB - Institute of Mathematical Sciences

T2 - 14th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2013

Y2 - 7 January 2013 through 9 January 2013

ER -