The Complexity of Symbolic Model Checking for Topological Evidence Models
Paul Fink

Abstract:
We analyze the computational complexity of symbolic model checking for Topological Evidence Models, where the state space is represented succinctly by BDDs. For the full language and already the single-agent fragment without restrictions on the models we establish PSPACE-completeness. We then identify fragments for which the complexity drops to Θ^P_2: in the single-agent setting, both restricting the language to the [∀]-modality and bounding the evidence size to a constant lead to Θ^P_2-complete symbolic model checking. Moreover, we obtain Θ^P_2-membership for the belief-only fragment by reusing the proof scheme developed for the bounded-evidence case, indicating a reusable method for proving ΘP upper 2bounds in related symbolic model-checking problems. Finally, we establish PSPACE-completeness for symbolic model checking the knowledge fragment with unbounded evidence.