Model Checking Probabilistic Knowledge: A PSPACE Case
Abstract
Model checking probabilistic knowledge of memoryful semantics is undecidable, even for a simple formula concerning the reachability of probabilistic knowledge of a single agent. This result suggests that the usual approach of tackling undecidable model checking problems, by finding syntactic restrictions over the logic language, may not suffice. In this paper, we propose to work with an additional restriction that agent's knowledge concerns a special class of atomic propositions. A PSPACE-complete case is identified with this additional restriction, for a logic language combining LTL with limit-sure knowledge of a single agent.
Cite
Text
Huang and Kwiatkowska. "Model Checking Probabilistic Knowledge: A PSPACE Case." AAAI Conference on Artificial Intelligence, 2016. doi:10.1609/AAAI.V30I1.10122Markdown
[Huang and Kwiatkowska. "Model Checking Probabilistic Knowledge: A PSPACE Case." AAAI Conference on Artificial Intelligence, 2016.](https://mlanthology.org/aaai/2016/huang2016aaai-model/) doi:10.1609/AAAI.V30I1.10122BibTeX
@inproceedings{huang2016aaai-model,
title = {{Model Checking Probabilistic Knowledge: A PSPACE Case}},
author = {Huang, Xiaowei and Kwiatkowska, Marta},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2016},
pages = {2516-2522},
doi = {10.1609/AAAI.V30I1.10122},
url = {https://mlanthology.org/aaai/2016/huang2016aaai-model/}
}