Abstract
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.
Users
Please
log in to take part in the discussion (add own reviews or comments).