X. Huang and M. Kwiatkowska, “Model Checking Probabilistic Knowledge: A PSPACE Case”, AAAI, vol. 30, no. 1, Mar. 2016.