Oxford logo
[HK16] X. Huang, M. Kwiatkowska. Model Checking Probabilistic Knowledge: A PSPACE Case. In Proc. AAAI Conference on Artificial Intelligence (AAAI'16), pages 2516-2522. 2016. [pdf] [bib]
Downloads:  pdf pdf (271 KB)  bib bib
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.