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 [
is accompanied by an environment reaction outside the agent’s control that determines the action’s outcome, e.g., a flipped coin may fall head or tail. A nondeterministic basic action theory (NDBAT) can be seen as a special kind of action theory, where we have system actions ( ,⃗) , successor state axioms , describing how predicates and functions change after system actions are performed, and action precondition axioms
, stating when each system action can occur. [
CEUR
ceur-ws.org
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. 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 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 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 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 with 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. Thus, 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.
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. [19] A. Church, Logic, arithmetics, and automata, in: Proc. Int. Congress of Mathematicians, 1963, pp.
23–35. [20] M. Abadi, L. Lamport, P. Wolper, Realizable and unrealizable specifications of reactive systems, in:
ICALP, volume 372 of Lecture Notes in Computer Science, Springer, 1989, pp. 1–17. [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.