Research map / Multi-agent systems and games / Human-AI and goal-conditioned
Situation Calculus Temporally Lifted Abstractions for Generalized Planning
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes a situation-calculus framework for generalized planning in which a propositional nondeterministic high-level abstraction with LTL trace constraints is refined to concrete first-order models, and LTL synthesis on the abstraction yields provably correct programs (demonstrated on finding the minimum in a linked list).
Problem
Generalized planning requires a single strategy solving infinitely many similar planning instances; existing abstraction approaches lack formal guarantees for temporally extended goals and trace constraints over first-order domains.
Approach
Combines nondeterministic situation calculus with LTL trace constraints and a refinement mapping that translates HL LTL formulas to the LL, defining a temporally lifted abstraction (m-simulation plus constraint satisfaction) so that HL LTL-synthesized strategies can be refined to LL strategies achieving the mapped goal.
Key results
- Proves that if a temporally lifted abstraction exists and the HL agent can force an LTL goal under trace constraints, a LL strategy exists achieving the mapped goal (Theorem 16).
- Illustrates the framework on finding the minimum value in a singly-linked list, with a HL strategy synthesized by Strix matching the hand-derived LL program.
- Shows the minimum-in-list mapping satisfies the proper refinement and temporal-lifting conditions (Propositions 11, 12, 17).
Limitations
- Illustrated only on a single worked example (minimum in a linked list); other examples deferred to an extended version.
- First-order setting is undecidable in general, so methodology relies on modeler-provided abstraction and mapping.
- Requires the modeler to supply the HL abstraction, refinement mapping, and LTL constraints.
Experimental setup
Baselines: Bonet et al. 2020 (B20) Cui et al. 2021 QNP abstraction BDL23 bisimulation abstraction
Builds on: nondeterministic situation calculus (DL21) abstraction for NDBATs (BDL23) Bonet et al. 2020 GP program synthesis via LTL synthesis Khan and Lespérance infinite path axiomatization
Closest papers by meaning
- A Syntactic Approach to Computing Complete and Sound Abstraction in the Situation Calculus (AAAI 2025 · similarity 0.89)
- LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments (AAAI 2025 · similarity 0.87)
- One Subgoal at a Time: Zero-Shot Generalization to Arbitrary Linear Temporal Logic Requirements in Multi-Task Reinforcement Learning (NeurIPS 2025 · similarity 0.86)
- Abstraction of Situation Calculus Concurrent Game Structures (AAAI 2024 · similarity 0.85)
- On Action Theories with Iterable First-Order Progression (AAAI 2025 · similarity 0.85)
- Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories (AAAI 2024 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.