Progression and Verification of Situation Calculus Agents with Bounded Beliefs

In this paper we investigate agents that have incomplete information and make decisions based on their beliefs, expressed as situation calculus bounded action theories. Such theories have an infinite object domain, but the number of objects that belong to fluents at each time point is bounded by a given constant. Recently it has been shown that verifying temporal properties over such theories is decidable. Here, we first show that we can actually check whether an arbitrary action theory maintains boundedness. Secondly, we examine progression. Progression can be thought of as capturing the notion of belief states resulting from actions in the situation calculus. In the general case, such belief states can be expressed only in second-order logic. Here, we show that for bounded action theories, progression, and hence belief states, can always be represented in first-order logic. Based on this result, we further prove decidability of temporal verification over online executions, i.e., those executions resulting from agents performing only actions that are feasible according to their beliefs.