Abstracting Situation Calculus Action Theories

TL;DR

This paper presents a formal framework for abstracting high-level agent actions into low-level implementations within the situation calculus, enabling reasoning, refinement, and monitoring at different abstraction levels.

Contribution

It introduces a formal notion of sound and complete abstraction between high and low-level action theories, with conditions for verification and unique refinement of actions.

Findings

Defined sound and complete abstraction in situation calculus

Provided conditions for verifying abstraction correctness

Ensured unique high-level action sequences for low-level actions

Abstract

We develop a general framework for agent abstraction based on the situation calculus and the ConGolog agent programming language. We assume that we have a high-level specification and a low-level specification of the agent, both represented as basic action theories. A refinement mapping specifies how each high-level action is implemented by a low-level ConGolog program and how each high-level fluent can be translated into a low-level formula. We define a notion of sound abstraction between such action theories in terms of the existence of a suitable bisimulation between their respective models. Sound abstractions have many useful properties that ensure that we can reason about the agent's actions (e.g., executability, projection, and planning) at the abstract level, and refine and concretely execute them at the low level. We also characterize the notion of complete abstraction where all actions (including exogenous ones) that the high level thinks can happen can in fact occur at the low level. To facilitate verifying that one has a sound/complete abstraction relative to a mapping, we provide a set of necessary and sufficient conditions. Finally, we identify a set of basic action theory constraints that ensure that for any low-level action sequence, there is a unique high-level action sequence that it refines. This allows us to track/monitor what the low-level agent is doing and describe it in abstract terms (i.e., provide high-level explanations, for instance, to a client or manager).