PDDL to DFA: A Symbolic Transformation for Effective Reasoning

ltl_f is a variant of ltl interpreted over finite traces [26] instead of infinite traces [35]. ltl_f has the same syntax as ltl. Given a set $AP$ of atomic propositions (aka atoms), the ltl_f formulas over $AP$ are generated by the following grammar:

Where $a\in AP$. Here $\circ$ (Next) and $𝒰$ (Until) are temporal operators. We use standard Boolean abbreviations such as $\vee$ (or), $\supset$ (implies), $\mathrm{𝑡𝑟𝑢𝑒}$ and $\mathrm{𝑓𝑎𝑙𝑠𝑒}$. Moreover, we define the following abbreviations: $\bullet \phi \equiv \neg \circ \neg \phi$ (Weak Next), $\mathrm{◇}\phi \equiv \mathrm{𝑡𝑟𝑢𝑒}𝒰\phi$ (Eventually), and $\mathrm{\square }\phi \equiv \neg \mathrm{◇}\neg \phi$ (Always). The size of $\phi$, written $|\phi |$, is the number of its subformulas. Formulas are interpreted over finite traces $\pi$ over the alphabet $\mathrm{\Sigma }=2^{AP}$, i.e., the alphabet consisting of the propositional interpretations of the atoms. Thus, for $0\le i\le \mathrm{𝗅𝗌𝗍}(\pi )$, ${\pi }_i\in 2^{AP}$ is the $i$-th interpretation of $\pi$. That an ltl_f formula $\phi$ holds at instant $i\le \mathrm{𝗅𝗌𝗍}(\pi )$, written $\pi ,i\vDash \phi$, is defined inductively:

• $\mathrm{■}$

  $\pi ,i\vDash a\text{ iff }a\in {\pi }_i$ (for $a\in AP$);

• $\mathrm{■}$

  $\pi ,i\vDash \neg \phi \text{ iff }\pi ,i\vDash ̸\phi$;

• $\mathrm{■}$

  $\pi ,i\vDash {\phi }_1\wedge {\phi }_2\text{ iff }\pi ,i\vDash {\phi }_1\text{ and }\pi ,i\vDash {\phi }_2$;

• $\mathrm{■}$

  and $\pi ,i+1\vDash \phi$;

• $\mathrm{■}$

  $\pi ,i\vDash {\phi }_1𝒰{\phi }_2$ iff $\exists j$ such that $i\le j\le \mathrm{𝗅𝗌𝗍}(\pi )$ and $\pi ,j\vDash {\phi }_2$, and we have that $\pi ,k\vDash {\phi }_1$.

We say that $\pi$ satisfies $\phi$, written $\pi \vDash \phi$, if $\pi ,0\vDash \phi$.

A deterministic finite automaton (dfa) is a tuple $𝒜=(\mathrm{\Sigma },Q,q_0,\delta ,F)$, where: $\mathrm{\Sigma }$ is a finite input alphabet; $Q$ is a finite set of states; $q_0\in Q$ is the initial state; $\delta :Q\times \mathrm{\Sigma }\to Q$ is the transition function; and $F\subseteq Q$ is the set of final states. The size of $𝒜$ is $|Q|$. Given a finite trace $\alpha ={\alpha }_0{\alpha }_1\mathrm{\dots }{\alpha }_n$ over $\mathrm{\Sigma }$, we extend $\delta$ to be a function $\delta :Q\times {\mathrm{\Sigma }}^{\ast }\to Q$ as follows: $\delta (q,\lambda )=q$, and, if $q_n=\delta (q,{\alpha }_0\mathrm{\dots }{\alpha }_{n-1})$, then $\delta (q,{\alpha }_0\mathrm{\dots }{\alpha }_n)=\delta (q_n,{\alpha }_n)$. A trace $\alpha$ is accepted by $𝒜$ if $\delta (q_0,\alpha )\in F$. The language of $𝒜$, written $ℒ(𝒜)$, is the set of traces that the automaton accepts.

ltl_f reactive synthesis [27] concerns finding a strategy to satisfy an ltl_f goal specification. Goals are expressed as ltl_f formulas over $AP=𝒳\cup 𝒴$, where $𝒳$ and $𝒴$ are disjoint sets of variables. Intuitively, $𝒳$ (resp. $𝒴$) is under the environment’s (resp. agent’s) control. Traces over $\mathrm{\Sigma }=2^{𝒳\cup 𝒴}$ will be denoted $\pi =(X_0\cup Y_0)(X_1\cup Y_1)\mathrm{\dots }$ where $X_i\subseteq 𝒳$ and $Y_i\subseteq 𝒴$ for every $i$. Infinite traces of this form are also called plays.

An agent strategy is a function $\sigma :{(2^{𝒳})}^{\ast }\to 2^{𝒴}$ mapping sequences of environment moves to an agent move. The domain of $\sigma$ includes the empty sequence $\lambda$ as we assumed that the agent moves first. A trace $\pi$ is $\sigma$-consistent if $Y_0=\sigma (\lambda )$ and $Y_{j+1}=\sigma (X_0\mathrm{\cdots }{X}_j)$ for every $j\ge 0$. Let $\phi$ be an ltl_f formula over $𝒳\cup 𝒴$. An agent strategy $\sigma$ is winning for (aka enforces) $\phi$ if, for every play $\pi$ that is $\sigma$-consistent, some finite prefix of $\pi$ satisfies $\phi$. ltl_f reactive synthesis is the problem of finding an agent strategy $\sigma$ that enforces $\phi$, if one exists, and is 2exptime-complete in the size of $\phi$ [27].

In many AI applications the agent has some knowledge about how the environment works, which it can exploit to enforce the goal [2]. This knowledge can be expressed by an ltl_f formula $ℰ$ over $𝒳\cup 𝒴$, which we call environment specification. In the synthesis of winning strategies, we can intuitively see $ℰ$ as restricting traces of interest to those satisfying $ℰ$. In this setting, synthesis amounts to computing a strategy that enforces the implication $ℰ\supset \phi$, if one exists.

A dfa game is a dfa $𝒢=(\mathrm{\Sigma },Q,q_0,\delta ,F)$ with input alphabet $\mathrm{\Sigma }=2^{𝒳\cup 𝒴}$. The notions of agent strategy and play defined above also apply to dfa games. A play is winning if it contains a finite prefix that is accepted by the dfa. An agent strategy is winning if, for every play $\pi$ that is $\sigma$-consistent, $\pi$ is winning. That is, the agent wins the game if it can force the play to visit the set of final states at least once. The winning region is the set of states $q\in Q$ for which the agent has a winning strategy in the game ${𝒢}^{\prime }$, where ${𝒢}^{\prime }=(2^{𝒳\cup 𝒴},Q,q,\delta ,F)$, i.e., the same game as $𝒢$, but with initial state $q$. Solving a dfa game is the problem of computing the agent winning region and a winning strategy, if one exists. dfa games can be solved in polynomial time by a backward-induction algorithm that performs a fixpoint computation over the state space of the game [7]. Synthesis of an ltl_f formula $\phi$ can be reduced in doubly-exponential time to solve the dfa game ${𝒢}_{\phi }$ corresponding to $\phi$ [27].

Solving ltl_f synthesis reduces to solving a reachability game over the dfa corresponding to the ltl_f specification. The procedure for solving ltl_f synthesis is detailed in Algorithm 1.

We consider the dfa representation described above as an explicit-state representation. Instead, we are able to represent a dfa more compactly in a symbolic way by using a logarithmic number of propositions to encode the state space [40]. Formally, the symbolic representation of a dfa $𝒜=(2^{𝒳\cup 𝒴},Q,q_0,\delta ,F)$ is a tuple ${𝒜}^s=(𝒳,𝒴,𝒵,Z_0,\eta ,f)$, where: $𝒵$ is a set of state variables such that $|𝒵|=\lceil \log |Q|\rceil$, and every state $q\in Q$ corresponds to an interpretation $Z\in 2^{𝒵}$; $Z_0\in 2^{𝒵}$ is the interpretation corresponding to the initial state $q_0$; $\eta :2^{𝒵}\times 2^{𝒳}\times 2^{𝒴}\to 2^{𝒵}$ is a Boolean function such that $\eta (Z,X,Y)=Z^{\prime }$ if and only if $Z$ is the interpretation of a state $q$ and $Z^{\prime }$ is the interpretation of the state $\delta (q,X\cup Y)$; and $f$ is a Boolean function over $𝒵$ such that $f(Z)=1$ if and only if $Z$ is the interpretation corresponding to a state $q\in F$. Note that the transition function $\eta$ can be represented by an indexed family consisting of a Boolean formula ${\eta }_z$ for each state variable $z\in 𝒵$, which when evaluated over an assignment to $𝒵\cup 𝒳\cup 𝒴$ returns the next assignment to $z$.

A symbolic dfa game can be solved by performing a least fixpoint computation over two Boolean formulas $w$ over $𝒵$ and $t$ over $𝒵\cup 𝒴$ which represent the winning region and winning states with agent moves such that, regardless of how the environment behaves, the agent reaches the final states, respectively [40]. Specifically, $w$ and $t$ are initialized as $w_0(𝒵)=f(𝒵)$ and $t_0(𝒵,𝒴)=f(𝒵)$, since every final state is a winning state. Note that $t_0$ is independent of the propositions from $𝒴$, since once the play reaches the final states, the agent can do whatever it wants. Then, $t_{i+1}$ and $w_{i+1}$ are constructed as follows:

The computation reaches a fixpoint when $w_{i+1}\equiv w_i$. When the fixpoint is reached, no more states will be added, and all winning states have been collected. By evaluating $Z_0$ on $w_{i+1}$ we can determine if there exists a winning strategy. If that is the case, $t_{i+1}$ can be used to compute a uniform positional winning strategy through the mechanism of Boolean synthesis [28].

Following [23], we define a fond domain as a tuple $𝒟=(2^{ℱ},s_0,Act,React,\alpha ,\beta ,\delta )$, where: $ℱ$ is a finite set of fluents, $|ℱ|$ is the size of $𝒟$, and $2^{ℱ}$ is the state space; $Act$ and $React$ are finite sets of agent actions and environment reactions, respectively; $\alpha :2^{ℱ}\to 2^{Act}$ is a function denoting agent action preconditions; $\beta :2^{ℱ}\times Act\to 2^{React}$ is a function denoting environment reaction preconditions; and $\delta :2^{ℱ}\times Act\times React\to 2^{ℱ}$ is the transition function such that $\delta (s,a,r)$ is defined if and only if $a\in \alpha (s)$ and $r\in \beta (s,a)$. We assume that planning domains satisfy the properties of:

• $\mathrm{■}$

  Existence of agent action: $\forall s\in 2^{ℱ}.\exists a\in \alpha (s)$;

• $\mathrm{■}$

  Existence of environment reaction: $\forall s\in 2^{ℱ}.\forall a\in \alpha (s).\exists r\in \beta (s,a)$;

• $\mathrm{■}$

  Uniqueness of environment reaction:
     $\forall s\in 2^{ℱ}.\forall a\in \alpha (s).\forall r_1,r_2\in \beta (s,a).\delta (s,a,r_1)=\delta (s,a,r_2)\supset r_1=r_2.$

With these properties, inspired by [22], we can capture classical fond domains [18, 29] by explicitly introducing environment reactions corresponding to nondeterministic effects of agent actions.

A state trace of $𝒟$ is a finite sequence $\tau =s_0\mathrm{\cdots }{s}_n$ of states such that $s_0$ is the initial state of $𝒟$ and, for every , there exists an agent action $a_i\in \alpha (s_i)$ and an environment reaction $r_i\in \beta (s_i,a_i)$ such that $s_{i+1}=\delta (s_i,a_i,r_i)$. A plan is a partial function $\kappa :2^{ℱ}\to Act$ such that, if $\kappa (s)$ is defined, then $\kappa (s)\in \alpha (s)$. A plan terminates its execution in states where, being a partial function, it specifies no action. A state trace $\tau =s_0\mathrm{\cdots }{s}_n$ is $\kappa$-consistent if: (i) $s_0$ is the initial state of $𝒟$; (ii) for every , $s_{i+1}=\delta (s_i,a_i,r_i)$ for $a_i=\kappa (s_i)$ and some $r_i\in \beta (s_i,a_i)$; and (iii) $\kappa (s_n)$ is undefined.

fond (strong) planning concerns finding a plan to satisfy a goal regardless of the nondeterminism in the domain, called strong plan. A goal $G$ is a conjunction of fluents and negations of fluents. Given a goal $G$ and a domain $𝒟$, a plan $\kappa$ is strong for $G$ in $𝒟$ if, for every state trace $\tau =s_0,\mathrm{\cdots },s_n$ that is $\kappa$-consistent, $s_n\vDash G$. Formally, fond planning is the problem of finding a strong plan for $G$ in $𝒟$, if one exists. fond planning is exptime-complete in the size of $𝒟$ [17].

In this paper, we always assume that we have fond domains expressed in pddl [31], i.e., the fluents defining the states of the domain are predicates over objects. We write predicate/k to specify that $k$ objects participate in the predicate relation. Predicates, actions, and action preconditions are specified in first-order syntax in a domain.pddl file, whereas the initial state, goal, and objects, are usually specified in a separate problem.pddl file.

We performed experiments on a suite of $170$ classical fond planning benchmarks divided in five classes: blocks world ($50$ instance), extended blocks world ($50$ instances), triangle-tire world ($40$ instances), rectangle-tire world ($15$ instances), and elevators ($15$ instances). In blocks world instances, the agent manipulates blocks with actions that can nondeterministically succeed or fail. In extended blocks world instances, the agent can also move towers of two blocks, with similar nondeterministic success or failure in actions. In triangle-tire and rectangle-tire instances, the agent navigates a grid environment, dealing with nondeterministic success or failure when moving. Elevator instances involve managing elevators to collect coins across multiple floors. For each class, the instances grow by increasing the problem size, which depends on their parameters.

We performed experiments to evaluate the efficiency of our technique for translating pddl into symbolic dfa and the practical feasibility of reducing fond planning to synthesis.

We evaluated the performance of pddl2dfa in transforming pddl to ltl_f and ltl_f to symbolic dfa. When employing this transformation, pddl2dfa was unable to construct the symbolic dfa of the pddl domain in the considered benchmarks, except in very few cases. The bottleneck was transforming ltl_f into dfa, which requires doubly-exponential time in the size of the ltl_f formula [26].

We evaluated the performance of pddl2dfa in transforming pddl to symbolic dfa with Algorithms 2 and 3. Table 1 shows that pddl2dfa constructed the dfa for a considerable number of benchmarks. Notably, pddl2dfa was able to construct the dfa of triangle-tire domains with side $61$. The bottleneck of the dfa construction was computing the agent error bdd. Indeed, Table 1 shows that the size of the agent error bdd in the hardest solved instances is orders of magnitude larger than that of the other bdds, including that of the largest fluent bdd. The reason is that constructing the bdd of the agent error requires iterating over all actions of the domain. Instead, constructing the bdds of the fluents requires only considering actions containing that fluent in their add- and delete-lists. Constructing the environment error bdd requires iterating over all environment reactions, but these are often several orders of magnitude less than fluents and agent actions (see Remark 3). As a result, the number of actions is the parameter that affects most the performance of the dfa construction. The size of the pddl domain, i.e., its fluents, has less impact than the number of agent actions on the dfa construction performance. Overall, this is a good result and shows the effectiveness of our construction.

We evaluated the performance of syft4fond in reducing fond planning to synthesis. Table 2 shows that syft4fond is able to solve a reasonable number of instances. Indeed, syft4fond was able to solve triangle-tire planning instances with side $19$, though based on plain backward search. The bottleneck of the synthesis was constructing the bdds of the agent winning moves and region during the fixpoint computation, which are mostly affected by the size of the agent error bdd. In general, we consider this result adequate to show the practical feasibility of reducing fond planning to synthesis.