Executability

Context

Executability isolates which action histories are legal in a situation-calculus action theory. Cerexhe2011 - Executability in the Situation Calculus uses this lens to compare subclasses of basic action theories with deterministic automata.

Formal Statement

Let $Poss(a,s)$ say that action $a$ is executable in situation $s$. Reiter’s recurrence for executability is

$$exec(do(a,s))\equiv exec(s)\wedge Poss(a,s),$$

with $exec(S_0)$ taken as trivially true.

For a basic action theory BAT with a designated halting or goal condition $fhalt(s)$, the accepted action sequences are

$$w\in E(BAT)⟺BAT\models fhalt(do(w,S_0))\wedge exec(do(w,S_0)).$$

The paper’s main correspondence result is that literal-based finite BATs can be mapped to deterministic finite-state automata, with context-free action theories forming a more restricted special case.

Derivation / Construction

• Situation terms are histories built from $S_0$ and repeated applications of $do(a,s)$.
• Precondition axioms define when a single next action is legal.
• The recurrence above lifts one-step legality into legality of whole action strings.
• Once executable histories are treated as a language over actions, automata-theoretic tools become applicable.
• Cerexhe and Pagnucco then compare specific BAT subclasses against DFA classes to characterize expressivity and implementation complexity.

Implications

• Planning and legality checking can be studied as language-recognition problems rather than only as proof search.
• Automata correspondences suggest alternate implementations for action theories, planners, or Golog-like interpreters.
• The result is about restricted action-theory classes, so it should not be read as “all situation-calculus theories are just DFAs.”

Links

• Parent concept: Situation Calculus
• Source anchor: Cerexhe2011 - Executability in the Situation Calculus
• Related area: Logic and Action Formalisms