We present a new formal framework for generalized planning (GP) based on the situation calculus extended with LTL constraints. The GP problem is specified by a first-order basic action theory whose models are the problem instances. This low-level theory is then abstracted into a high-level propositional nondeterministic basic action theory with a single model. A refinement mapping relates the two theories. LTL formulas are used to specify the temporally extended goals as well as assumed trace constraints. If all LTL trace constraints hold at the low level and the high-level model can simulate all the low-level models with respect to the mapping, we say that we have a temporally lifted abstraction. We prove that if we have such an abstraction and the agent has a strategy to achieve a LTL goal under some trace constraints at the abstract level, then there exists a refinement of the strategy to achieve the refinement of the goal at the concrete level. We use LTL synthesis to generate the strategy at the abstract level. We illustrate our approach by synthesizing a program that solves a data structure manipulation problem.
In generalized planning (GP), one tries to generate a typically iterative policy that solves an infinite set
of similar planning problem instances [
Our framework is based on the nondeterministic situation calculus [
Here, we assume that the modeler specifies a propositional high-level (HL) action theory/model with
a limited set of HL fluents and nondeterministic actions, which abstracts over a concrete low-level (LL)
action theory with multiple models, with a given refinement mapping . At the LL, in each model we
have complete information about the state of the world, while at the HL, we have actions that may have
several outcomes, e.g., after advancing to the next item in a list, we may or may not reach the list’s end.
We extend the HL theory with LTL trace constraints to impose fairness assumptions on the possible
sequences of nondeterministic actions, e.g., ensuring that if we keep advancing we will eventually reach
the list’s end. To do this, we leverage the axiomatization of infinite paths introduced by [
. ( 1 2, ) = ∃, ′, ′.(, ) ∧ ⪯ ′ ∧ Suffix (′, , ′) ∧ ( 2, ′) ∧ ∀′′, ′′.
( ⪯ ′′ ≺ ′ ∧ Suffix (′′, , ′′)) ⊃ ( 1, ′′)
Finally, we define a notion of temporally lifted abstraction, where every LL trace that is a refinement of a sequence of HL actions is -similar to a trace involving this action sequence in the HL model, and where the LTL trace constraints are satisfied by the LL theory. The NDBATs represent our GP problem, where each LL model specifies the planning problem instances, and the HL model abstracts away the LL details, retaining only the shared features. We then provide a method for solving all the planning problem instances simultaneously. In particular, we show that given such an abstraction, if we can use LTL synthesis on the HL model to obtain a HL strategy that achieves a LTL goal under the given trace constraints, then we can automatically refine it to get a LL strategy that achieves the mapped LTL goal in all concrete instances of the problem.
We illustrate how our approach works by using it to synthesize a program to find the minimum value
of a list. This application is inspired by [
Our methodology involves the following main steps: 1. Formalize the concrete planning problem instances in situation calculus - this consists of writing the specification for the domain of interest; hence, it is straightforward 2. Specify a propositional temporally lifted abstraction as a HL NDBAT - this abstracts over some details and includes nondeterministic actions; some LTL trace constraints will also be introduced to capture restrictions on the possible future histories; obtaining the HL NDBAT is similar to the previous step and, in many cases, we can reuse (part of) the specification of one GP task for other similar tasks (i.e., involving the same data structure) 3. Write the LTL goals - this step is domain-dependent 4. Run a LTL synthesis engine on the HL abstraction - this automatically derives a HL strategy to reach the goals; note that our HL propositional abstraction can always be interpreted as an LTL specification 1 is a ground situation-suppressed formula defined over an NDBAT; [] is the formula obtained by restoring the situation . 5. Translate the HL strategy to a LL program - this step can be simply addressed by using the refinement mapping This methodology yields provably correct solutions; the following sections will be devoted to providing strong formal guarantees. Note that there should be no need to generate the entire situation calculus specifications from scratch. Instead, one could build a library of specifications and reuse them in a modular way. This means that the modeler can just specify her problem in terms of HL trace and goal constraints, exploiting this library, and then run the automatic synthesis engines.
Step 1: Consider the task of finding the minimum value stored in a singly-linked list. We can construct a NDBAT
with two actions and two functional fluents. The actions are , which moves a cursor that scans the nodes of the list, and , which writes the value of the current pointed node into a dedicated register. Additionally, we have a _ action, with no precondition and no efect. Note that, at the LL, we have only one possible environment reaction Success for each action. The functional fluents will be (), whose value represents the position of the current node within the list, and (), which represents whether the current node contains a lower value than the register.
Step 2:
NDBAT ℎ models the HL action theory with two (propositional) fluents: ℎ (), signaling whether the cursor points at the last node of the list, and ℎ(), signaling whether the value of the node pointed by the cursor is lower than the value stored in the register. The actions used for our task will be , which moves the cursor if possible and performs the comparison between the node and register values, and , which updates the register’s value to the node’s. The environment reaction of tells us if the successor node’s value is lower than the register’s and if the end is reached. Here is a fragment of the refinement mapping : ((ℎ)) = ( ); if < ℎ
if = LT else endIf if = LT then ℎ = LT_NE? else ℎ = GEQ_NE? endIf then ℎ = LT_E? else ℎ = GEQ_E? endIf Additionally, we introduce two LL actions and which make () false and true respectively at the beginning and at the end of the program of each HL action. We also use a HL fluent for each action, namely and , to signal the last action executed. Finally, we consider the HL trace constraint for specifying that moving repeatedly to the next node of the list eventually leads to the last one:
Step 3: The HL LTL goals that must be satisfied are: (□♢ ) → ♢ ¬ℎ □♢
¬ℎ □ ( ℎ ↔ ○ ) The first says that the list must be scanned till the end, while the second says that the value of the register must be updated if the pointed node has a lower value than the register.
Step 4: A HL strategy that satisfies the goals is: ℎ() = ⎨ ⎧⎪ if ℎ()
⎪⎩ if ¬ ℎ() ∧ ℎ () otherwise This strategy prescribes updating the value of the register whenever the node has a lower value and moving the cursor when it is not at the end of the list. As stated before, since we have a propositional HL specification, we can write it in LTL and rely on LTL synthesis engines to automatically derive this strategy (this needs an intermediate translation from the HL specification to an LTL one). Figure 1 shows the controller obtained by using the engine Strix [22], as done by (B20). It is easy to see that ℎ is consistent with the controller.
Step 5: At the LL the strategy can be refined as follows:
⎧⎪ if = LT () = ⎨ if = GEQ ∧ < ℎ
⎪⎩_ otherwise
As mentioned previously, we want to specify a GP problem at the concrete level by a BAT , with the various basic planning problems being models of this BAT. We will then define an abstract version of the theory by providing a propositional NDBAT ℎ, for which we have a single model and incomplete information, with the nondeterminism capturing the diferences between the diferent concrete instances. We will also specify some LTL trace constraints on the abstract model that characterize the traces that can actually arise in the concrete theory instances. We refer to this framework as a temporally lifted abstraction. With this structure in place, we can approach solving the GP problem by performing LTL synthesis on the abstraction.
For this to work, we need to ensure that executions of refinements of HL actions in models of the LL theory correspond to executions in the HL theory/model. So we will specify the relationship between the HL NDBAT and the LL BAT by a refinement mapping . For this, we extend the notion of refinement mapping for NDBAT abstractions from (BDL23) to handle LTL trace constraints. We will then ensure that executions of HL actions in the models correspond through a form of simulation relative to the refinement mapping .
ping is a triple ⟨, , ⟩ where (i) associates each HL agent action to a ConGolog agent program (i.e., ((⃗)) = (⃗)), (ii) associates each system action to a ConGolog system program (i.e., ((⃗, )) = (⃗, )), (iii) maps each situation-suppressed HL fluent (⃗) to a formula .
Our revisited definition of NDBAT mapping maintains the previous elements and includes a new component , which specifies how HL trace constraints are mapped to the LL: Definition 1 (Refinement Mapping for Trace Constraints) . Let be an LTL trace constraint and a distinguished symbol that signals that a HL action is completed. A NDBAT refinement mapping is a tuple ⟨, , , ⟩, where , and are defined as usual and is a mapping for trace constraints defined as follows:
() =. . () (¬ ) = ¬.( ) ( 1 ∨ .2) = ( 1) ∨ ( 2) (○ ) = ○ .(¬ ( ∧ ( ))) ( 1 2) = ( ⊃ ( 1)) ( ∧ ( 2))
As in [
((((⃗)), , ′) ≡ ∃ .(((⃗, )), , ′)) Constraint 3. ∪ |= () if and only if there exists a HL system action sequence⃗ such that ∪ |= (⃗( ), 0, ).
Temporally lifted abstractions. Finally, we can present the concept of temporally lifted abstractions. To relate the HL and LL models, we first need to present the notion of -isomorphic situations. Definition 4 (m-isomorphic situations). We say that situation ℎ in ℎ is m-isomorphic to situation ℎ, , if and only if in , written ℎ ≃
ℎ, [/ℎ] |= (⃗, ) if , [/] |= ( (⃗))[] for every high-level primitive fluent (⃗) in ℎ and every variable assignment .
(BDL23) define a variant of bisimulation [ 24, 25] to establish a relation based on the refinement mapping. Here, we stick to a unidirectional version: Definition 5 (-simulation). A relation ⊆ if ⟨ℎ, ⟩ ∈ implies
Δℎ × Δ is an m-simulation relation between ℎ and 1. ℎ is m-isomorphic to 2. for every HL system action A, if there exists ′ such that , [/, ′/′] |= (((⃗)), , ′), then there exists ′ℎ such that ℎ, [/ℎ, ′/′ℎ] |= ((⃗), ) ∧ ′ = ((⃗), ) and ⟨′ℎ, ′⟩ ∈ We say that ℎ is m-similar to wrt the mapping (written ℎ ∼ ← ) if there exists an m-simulation relation between ℎ and such that ⟨0ℎ , 0 ⟩ ∈ .
At last, exploiting -simulation together with the use of LTL trace constraints, we can talk about the notion of temporally lifted abstractions. Intuitively, we have a temporally lifted abstraction if there is an -simulation between an HL model/theory and all the models of a LL theory, and every trace constraint is satisfied both on some path at the HL and on all paths at the LL.
Definition 6 (Temporally Lifted Abstraction). Consider an HL NDBAT ℎ equipped with a set of HL state constraint Ψ, a model ℎ of ℎ, a LL NDBAT and a refinement mapping . We say that (ℎ, ℎ, Ψ) is a temporally lifted abstraction wrt if and only if • ℎ -simulates every model of • for every high-level LTL trace constraint ∈ Ψ, ℎ |= ∃ℎ.(ℎ, 0ℎ ) ∧ (, ℎ) and |= ∀.(, 0 ) ⊃ (( ), )
It is possible to verify that one has a temporally lifted abstraction by using the following theorem. Theorem 7. Suppose that we have a HL NDBAT ℎ, a model ℎ of ℎ, a set of HL LTL state constraints Ψ, a LL NDBAT , and a refinement mapping . If (a) ℎ0 is a complete theory, i.e. the initial state is completely specified, (b) 0 ∪ ∪ |= (), for all ∈ ℎ0 ,
(c) for all high-level action sequence⃗s , ∪ |= ∀.(⃗( ), 0, ) ⊃ ⋀︀∈ℎ ∀⃗.(∃′(((⃗)), , ′)) ⊃ ( (⃗))[]
where (⃗) is the right-hand side (RHS) of the precondition axiom for action (⃗), (d) for all high-level action sequence⃗s , ∪ |= ∀.(⃗( ), 0, ) ⊃ ⋀︀⋀︀∈ℎ ∀⃗, ′.((((⃗)), , ′) ⊃
∈ℱℎ ∀⃗.( (, (⃗, ⃗))[] ≡ ((⃗))[′])) where
, (⃗, ⃗) is the RHS of the successor state axiom for instantiated with action (⃗) where action terms have been eliminated using ℎ, and (e) for every high-level LTL trace constraint ∈ Ψ, ℎ |= ∃ℎ.(ℎ, 0ℎ ) ∧ (, ℎ) and |= ∀.(, 0 ) ⊃ (( ), ), then (ℎ, ℎ, Ψ) is a temporally lifted abstraction of wrt .
Now we want to address the problem of synthesis in the context of temporally lifted abstractions, that is, generating strategies that achieve given goals at the abstract and at the concrete level. These strategies are the solutions for the GP problem defined by the abstraction.
For NDBATs, a strong plan is a strategy for the agent that guarantees the achievement of a goal no matter how the environment reacts. (DL21) formalize this notion for state goals and finite traces. They define a strategy as a function from situations to agent actions, i.e. f () = (⃗) (note that the value may depend on the entire history). The special agent action (with no efects and preconditions) may be returned when the strategy wants to stop (for a finite strategy).
Here, we extend their definition to handle LTL goals and LTL trace constraints over infinite paths. We define AgtCanForceByIf (, , , ), meaning that the agent can force a LTL to hold no matter how the environment responds to her actions by following strategy in situation if we assume that the LTL trace/path constraint holds, as follows: where
AgtCanForceByIf (, , , ) =.
(, ) ∧ ∀.(, , ) ∧ (, ) ⊃ (, ) (, ) =. ∃.[∀. () ⊃
[ ( (), )] ∧ [∀′.( (), , ′) ⊃ (′)]] ∧ () (, , ) =. ∀.∀. ℎ(, ) ∧ ℎ(, (, )) ⊃
( (), , (, )) (, ) captures the requirement that the strategy never prescribes an action that is not executable; (, , ) means that path is a possible outcome of the agent executing strategy in . We also define AgtCanForceIf (, , ) =. ∃.AgtCanForceByIf (, , , ).
We also need to consider whether the agent is able to execute a program to completion, i.e., the implementation of a HL action, no matter how the environment reacts. For this, (DL21) introduce (, , f ), meaning that the agent can ensure that it executes program to completion by following strategy : (, f , ) =. ∀.[. . . ⊃ (, )] where . . . stands for [(f () = ∧ (, )) ⊃ (, )] ∧ [∃.∃⃗.(f () = (⃗) ̸= ∧ ∃.∃ ′. (, , ′, ((⃗, ), )) ∧ ∀.(∃ ′. (, , ′, ((⃗, ), ))) ⊃ ∃ ′. (, , ′, ((⃗, ), )) ∧ ( ′, ((⃗, ), )) ⊃ (, )]
Now we can talk about planning with abstractions and how a plan at the abstract level is related to one at the concrete level. As in (BDL23), we impose an additional constraint on action implementation which requires that for any HL agent action that is executable at the LL, the agent has a strategy to execute it no matter how the environment reacts: Constraint 8 (Agent Can Always Execute HL actions). For every HL action , there exists a LL strategy such that for every HL system action sequence⃗ : |= ∀.(⃗(, 0, ) ⊃ (∀⃗.∃′.(((⃗)), , ′) ⊃
(((⃗)), , ))
Then, we can prove our main result, that is, given a temporally lifted abstraction, if the agent has a strategy to achieve a LTL goal assuming some LTL constraints at the high level, then there exists a refinement of the HL strategy that ensures it achieves the refinement of the goal at the low level: Theorem 9. Let (ℎ, ℎ, ) be a temporally lifted abstraction of wrt refinement mapping s.t. Constraints 3 and 8 hold, and be an LTL goal. Then we have that: if ℎ |= AgtCanForceIf (, , 0), then there exists a LL strategy such that |= AgtCanForceByIf ((), True, , 0)
Let be an additional LL LTL goal. We say that a strategy is a solution with respect to if |= AgtCanForceByIf (, , , 0). It is easy to see that the LL strategy obtained by Theorem 9 is a solution for a GP problem if |= ∀.(, 0) ⊃
[((), ) ⊃ (, )]
This work has been partially supported by the ERC Advanced Grant WhiteMech (No. 834228), the PNRR MUR project FAIR (No. PE0000013), the Italian National Ph.D. on Artificial Intelligence at Sapienza University of Rome, the National Science and Engineering Research Council of Canada, and York University. [21] A. Pnueli, R. Rosner, On the synthesis of a reactive module, in: Proceedings of the 16th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages, 1989, pp. 179–190. [22] P. J. Meyer, S. Sickert, M. Luttenberger, Strix: Explicit reactive synthesis strikes back!, in: CAV (1), volume 10981 of Lecture Notes in Computer Science, Springer, 2018, pp. 578–586. [23] Y. Lespérance, G. D. Giacomo, M. Rostamigiv, S. M. Khan, Abstraction of situation calculus concurrent game structures, in: Proceedings of the AAAI Conference on Artificial Intelligence, AAAI 2024, 2024, pp. 10624–10634. URL: https://doi.org/10.1609/aaai.v38i9.28933. doi:10.1609/ AAAI.V38I9.28933. [24] R. Milner, An algebraic definition of simulation between programs, in: Proceedings of the 2nd International Joint Conference on Artificial Intelligence. London, UK, September 1-3, 1971, William Kaufmann, 1971, pp. 481–489. URL: http://ijcai.org/Proceedings/71/Papers/044.pdf. [25] R. Milner, Communication and concurrency, PHI Series in computer science, Prentice Hall, 1989.