Bounded Epistemic Situation Calculus Theories

We define the class of e-bounded theories in the epistemic situation calculus, where the number of fluent atoms that the agent thinks may be true is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We show that for them verification of an expres-sive class of first-order µ-calculus temporal epis-temic properties is decidable. We also show that if the agent’s knowledge in the initial situation is e-bounded and the objective part of an action theory maintains boundedness, then the entire epistemic theory is e-bounded