# Bounded Situation Calculus Action Theories

arXiv: https://arxiv.org/abs/1509.02012 · HTML: https://mlsanity.com/paper/1509.02012/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Sep 2015.

## Built on by (most cited first, 10 of 10)

- [Lifted Model Checking for Relational MDPs](https://mlsanity.com/paper/2106.11735/) (2021)
- [Abstraction of Nondeterministic Situation Calculus Action Theories -- Extended Version](https://mlsanity.com/paper/2305.14222/) (2023)
- [A Logical Semantics for PDDL+](https://mlsanity.com/paper/2111.11588/) (2021)
- [Planning as Theorem Proving with Heuristics](https://mlsanity.com/paper/2303.13638/) (2023)
- [Current and Future Challenges in Knowledge Representation and Reasoning](https://mlsanity.com/paper/2308.04161/) (2023)
- [LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments](https://mlsanity.com/paper/2410.00726/) (2024)
- [Abstracting Situation Calculus Action Theories](https://mlsanity.com/paper/2410.14712/) (2024)
- [Planning with Dynamically Changing Domains](https://mlsanity.com/paper/2508.02697/) (2025)
- [Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)](https://mlsanity.com/paper/2208.06377/) (2022)
- [Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories](https://mlsanity.com/paper/2402.03164/) (2024)

## Abstract (arXiv)

In this paper, we investigate bounded action theories in the situation calculus. A bounded action theory is one which entails that, in every situation, the number of object tuples in the extension of fluents is bounded by a given constant, although such extensions are in general different across the infinitely many situations. We argue that such theories are common in applications, either because facts do not persist indefinitely or because the agent eventually forgets some facts, as new ones are learnt. We discuss various classes of bounded action theories. Then we show that verification of a powerful first-order variant of the mu-calculus is decidable for such theories. Notably, this variant supports a controlled form of quantification across situations. We also show that through verification, we can actually check whether an arbitrary action theory maintains boundedness.