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 expressive class of first-order u0016-calculus temporal epistemic properties is decidable.We also show that if the agent’s knowledge in the initial situation is ebounded and the objective part of an action theory maintains boundedness,then the entire epistemic theory is e-bounded.