Executability in the Situation Calculus

Summary

This partial ingest is based on the abstract plus the opening technical sections from the extracted text. The paper relates classes of situation-calculus action theories to deterministic finite-state automata in order to characterize executability and expressivity.

Key Claims

• Executable action sequences in a situation-calculus theory can be studied as a language over actions.
• Special classes of action theories correspond to classes of deterministic finite-state automata.
• This correspondence can inform planning, legality checking, and efficient implementation.

Methods / Formalism

• Problem setup: a finite basic action theory is presented as $B={\Sigma }_{sitcalc}\cup B_{una}\cup B_{ss}\cup B_{ap}\cup B_{S0}$ over finite sets of fluents, actions, and objects.
• Executability rule: $exec(do(a,s))\equiv exec(s)\wedge poss(a,s)$, with $exec(S_0)$ treated as trivially true.
• Acceptance view: a BAT accepts an action sequence $w$ when $BAT\models fhalt(do(w,S_0))\wedge exec(do(w,S_0))$.
• Main result: literal-based BATs are matched to DFAs, and context-free action theories are identified as a special case inside that correspondence; see Executability.

Evidence / Experiments

• This appears to be a theory-heavy paper rather than an empirical benchmark paper.
• Full proofs and construction details still need full ingest.

Connections

• Primary source for Situation Calculus.
• Connects symbolic action reasoning to automata-theoretic structure inside Logic and Action Formalisms.
• Relevant when thinking about logical interfaces for safe or verifiable agents.
• Executability stores the reusable recurrence, acceptance, and DFA-correspondence details extracted from this paper.

Open Questions

• Can these expressivity results help structure symbolic constraints for RL environments?
• Which parts transfer to multi-agent or partially observed domains?

Citation

Cerexhe, T., and Pagnucco, M. (2011). Executability in the Situation Calculus. AI 2011, LNAI 7106, 677-686.