A Correctness Result for Synthesizing Plans With Loops in Stochastic Domains

TL;DR

This paper presents new theoretical results ensuring correctness when synthesizing finite-state controllers with loops in stochastic domains, addressing termination and goal-reaching guarantees.

Contribution

It introduces a generic technique for synthesizing FSCs in stochastic environments with formal guarantees on termination and goal satisfaction.

Findings

Provides a formal correctness framework for FSCs with loops in stochastic settings

Enables highly granular specifications for termination and goal conditions

Advances understanding of synthesis algorithms in probabilistic environments

Abstract

Finite-state controllers (FSCs), such as plans with loops, are powerful and compact representations of action selection widely used in robotics, video games and logistics. There has been steady progress on synthesizing FSCs in deterministic environments, but the algorithmic machinery needed for lifting such techniques to stochastic environments is not yet fully understood. While the derivation of FSCs has received some attention in the context of discounted expected reward measures, they are often solved approximately and/or without correctness guarantees. In essence, that makes it difficult to analyze fundamental concerns such as: do all paths terminate, and do the majority of paths reach a goal state? In this paper, we present new theoretical results on a generic technique for synthesizing FSCs in stochastic environments, allowing for highly granular specifications on termination and goal satisfaction.

Equations

$$\ell (h^{(:0)}):=1,\ell (h^{(:t+1)}):=\ell (h^{(:t)})\cdot \Delta (s^{(t+1)}|s^{(t)},a^{(t)}).$$

$$\mathbf{LTER}:=\sum _{\{h|h\text{ is a terminating history}\}}\ell (h)$$

$$\mathbf{LGT}:=\sum _{\{h|h\text{ is a goal history}\}}\ell (h)$$

$$h^{\star }=h_{\mathrm{curr}}^{(k-1:k)}\cdot h_{\mathrm{loop},1}\cdot \dots \cdot h_{\mathrm{loop},m}\cdot h_{\mathrm{goal}}.$$

$${\tilde{\alpha }}_{\mathrm{goal}}^{(k)}$$

$${\tilde{\lambda }}_{\mathrm{loop}}^{(k)}$$

$${\tilde{\lambda }}_{\mathrm{goal}}^{(n)}$$

$${\tilde{\lambda }}_{\mathrm{goal}}^{(k)}$$

$$p^{(k)}=Δ\big{(}s_{\mathrm{curr}}^{(k)}\ \big{|}\ s_{\mathrm{curr}}^{(k-1)},δ(q_{\mathrm{curr}}^{(k-1)},Ω(h_{\mathrm{curr}}^{(k-1)}))\big{)}.$$

$${\lambda }_{\mathrm{loop}}^{(k)}$$

$$\displaystyle\quad+p^{(k+1)}\ \big{(}1-λ_{\mathrm{loop}}^{(k+1)}\big{)}^{-1}\ α_{\mathrm{loop}}^{(k,k+1)}+\ldots+$$

$$\displaystyle\quad+p^{(k+1)}p^{(k+2)}\cdots p^{(n)}\ \big{(}1-λ_{\mathrm{loop}}^{(n)}\big{)}^{-1}\ α_{\mathrm{loop}}^{(k,n)}.$$

$${\lambda }_{\mathrm{goal}}^{(0)}\le {\tilde{\lambda }}_{\mathrm{goal}}^{(0)}=\mathbf{LGT},$$

$$\mathbf{LGT}$$

$$\le 1-{\tilde{\lambda }}_{\mathrm{fail}}^{(0)}(C_{\mathrm{good}})-{\tilde{\lambda }}_{\mathrm{noter}}^{(0)}(C_{\mathrm{good}})$$

$$\le 1-{\tilde{\lambda }}_{\mathrm{fail}}^{(0)}(C^{\prime })-{\tilde{\lambda }}_{\mathrm{noter}}^{(0)}(C^{\prime })$$

$$\le 1-{\lambda }_{\mathrm{fail}}^{(0)}(C^{\prime })-{\lambda }_{\mathrm{noter}}^{(0)}(C^{\prime })$$

$$<{LGT}^{\star }$$

$${\lambda }_{\mathrm{goal}}^{(0)}$$

$${\lambda }_{\mathrm{goal}}^{(0)}+{\lambda }_{\mathrm{fail}}^{(0)}$$

$$\mathbf{LTER}(C_{\mathrm{good}})$$

$$\le 1-{\tilde{\lambda }}_{\mathrm{noter}}^{(0)}(C^{\prime })$$

$$\le 1-{\lambda }_{\mathrm{noter}}^{(0)}(C^{\prime })$$

$$<{LTER}^{\star }$$

Full text

In this paper, we present new theoretical results on a generic technique for synthesizing FSCs in stochastic environments, allowing for highly granular specifications on termination and goal satisfaction.

††journal: Journal

\newunicodechar

αα \newunicodecharγγ \newunicodecharδδ \newunicodecharεε \newunicodecharλλ \newunicodecharωω \newunicodecharΔΔ \newunicodecharΠΠ \newunicodecharΩΩ \newunicodechar→→ \newunicodechar⇒⇒ \newunicodechar⟨⟨ \newunicodechar⟩⟩ \newunicodechar≤≤ \newunicodechar≥≥ \newunicodechar∈∈

1 Introduction

Finite-state controllers (FSCs), such as plans with loops, are powerful and compact representations of action selection widely used in robotics, video games and logistics. In AI, FSCs are much sought after for automated planning paradigms such as generalized planning, as in Figure 1, where one attempts to synthesize a controller that works in multiple initial states. Such controllers are usually hand-written by domain experts, which is problematic when expert knowledge is either unavailable or unreliable. To that end, the automated synthesis of FSCs has received considerable attention in recent years, e.g., [16, 7, 26, 24, 11, 27]. Of course, FSCs synthesis is closely related to program synthesis [16], and FSCs are frequently seen as program-like plans [17], and recent synthesis literature involves an exciting exchange of technical insights between the two fields [26]; representative examples include the use of program synthesis to infer high-level action types [25], and the use of partial order planning for imperative program synthesis [13].

Naturally, from an algorithmic perspective, the two most immediate questions are: in which sense are controllers correct, and how do we synthesize controllers that are provably correct? In classical deterministic settings, plan paths can only be extended uniquely, so it suffices to show that there is a terminating path that reaches the goal state. Ideally, then, what we seek is a procedure that is both sound (i.e., all synthesized controllers are correct) and complete (i.e., if there is a plan, then the procedure finds it).

The compact nature of FSCs makes them particularly attractive for mobile robots [20], among other domains where there is inherent stochasticity and actions are noisy. To a first approximation, in the presence of non-probabilistic nondeterminism, it is common practice to make meta-level assumptions, such as disallowing repeated configurations of (state, action) pairs. However, in stochastic environments, that is almost always an unreasonable assumption. Consider a robot attempting to grip an object: the first and second attempt may fail, but perhaps the third succeeds. Structurally, the first two failures are identical: while a domain expert might find a way to distinguish the two states for the planner, from a robustness viewpoint, of course, it is more desirable when algorithms operate without such meta-level assumptions. In this regard, the algorithmic machinery needed for lifting FSC synthesis techniques to stochastic environments is not yet fully understood.

More generally, we identify the following desiderata:

• D1.

The planner should cope with plan paths that do not terminate in a goal state;

• D2.

The planner should correctly account for how a looping history affects goal probabilities, distinguishing loops that never terminate and loops that can be extended into goal histories; and

• D3.

The planner should recognize when a combination of loops never terminates, even if the loops by themselves appear to be possibly terminating.

Implicit in these desiderata is the idea that the planner should leverage the likelihood of action outcomes, because (a) these likelihoods are informative about which action outcomes are more likely than others, and (b) in the presence of repeating configurations, probabilities allow for a natural tapering of the likelihood of paths.

In this paper, we present new theoretical results on a generic technique for synthesizing FSCs in stochastic environments, by means of a probabilistic extension of AND-OR search. We provide a careful analysis of how to maintain upper and lower bounds of the likelihoods of paths, so that one can naturally deal with tapering probabilities, arising from repeating configurations. In particular, it allows us to plan for highly granular specifications, such as: generate a FSC under the requirement that >80% of the paths terminate, and >60% of the paths reach the goal state. Most significantly, we prove that our algorithm is both sound and complete.

2 Problem formalisation

Our contributions do not depend on the details of the formal language (e.g., [12]), and so we consider an abstract framework [4].

Definition 1**.**

An environment $\mathcal{E}$ is defined as a tuple $\textlangle\mathcal{S},\mathcal{A},\mathcal{O},\Delta,\Omega\textrangle$, whose elements are the following: $\mathcal{S}$, $\mathcal{A}$, $\mathcal{O}$ are finite sets of states, actions, and observations; $Δ:\mathcal{S}\times\mathcal{A}\rightarrow Π(\mathcal{S})$ is a stochastic state transition function, where $Π(\mathcal{S})$ denotes the set of probability distributions over $\mathcal{S}$; $Ω:\mathcal{S}\textrightarrow\mathcal{O}$ is an observation function.

A planning problem is defined as an environment, an initial state, and a set of goal states:

Definition 2**.**

A planning problem $\mathcal{P}$ is a triple $\textlangle\mathcal{E},s_{0},\mathcal{G}\textrangle$, where $\mathcal{E}$ is an environment with state space $\mathcal{S}$, $s_{0}\in\mathcal{S}$ is the initial state, and $\mathcal{G}\subset\mathcal{S}$ is the set of goal states.

We represent loopy plans as follows [21]:

Definition 3**.**

A finite state controller (FSC) $C$ is defined by a tuple $\textlangle Q,q_{0},\mathcal{O},\mathcal{A},\gamma,\delta\textrangle$, where: $Q=\{q_{0},q_{1},\ldots,q_{N-1}\}$ is a finite set of controller states; $q_{0}\in Q$ is the initial state of the controller; $\mathcal{O}$ & $\mathcal{A}$ are the sets of possible observations & actions; $\gamma:Q\times\mathcal{O}\rightarrow(\mathcal{A}\cup\{\text{{stop}}\})$ is a partial function called the labeling function; $\delta:Q\times\mathcal{O}\rightarrow Q$ is a partial function called the transition function.

An FSC forms part of a system $\textlangle\mathcal{E},C\textrangle$, usually for a planning problem $\textlangle\mathcal{E},s_{0},\mathcal{G}\textrangle$. Initially, the environment is in state $s^{(0)}=s_{0}$, and the FSC $C$ is in controller state $q^{(0)}=q_{0}$. The controller makes an observation $o^{(0)}=Ω(s_{0})$, executes action $a^{(0)}=\gamma(q^{(0)},o^{(0)})$, and transitions to controller state $q^{(1)}=δ(q^{(0)},o^{(0)})$. The environment transitions to state $s^{(1)}\sim Δ(s^{(1)}|s^{(0)},a^{(0)})$. This process is repeated until the special action stop is executed, when the state$\rightarrow$observation$\rightarrow$action$\rightarrow$next-state cycle stops.

We call a pair of controller and environment state $\textlangle q,s\textrangle$ a combined state of the system.

Notation**.**

We denote the value of any $x\in\{s,q,o,a,p\}$ at step $t$ during the execution of a system by $x^{(t)}$. A sequence is written as $\langle x^{(t)}\rangle_{t=i}^{j}:=\langle x^{(i)},x^{(i+1)},\ldots,x^{(j)}\rangle$. The subsequence of $h=\textlangle h^{(t)}\textrangle_{t}$ between indices $i$ and $j$ is denoted by $h^{(i:j)}:=\textlangle h^{(i)},h^{(i+1)},\ldots,h^{(j)}\textrangle$, and $h^{(:j)}:=h^{(0:j)}$. $\mathit{end}(h)$ refers to the last element of $h$. The concatenation of two compatible sequences is denoted by $\cdot$, e.g., $h^{(i:j)}\cdot h^{(j:k)}:=h^{(i:k)}$. (Sequences $h_{1}$ and $h_{2}$ are compatible if $\mathit{end}(h_{1})=h_{2}^{(0)}$.)

A history of a system from a given combined state is one possible sequence of states that it follows, not necessarily until termination.

Definition 4**.**

Let $C=\textlangle Q,q_{0},\mathcal{O},\mathcal{A},γ,δ\textrangle$ be a finite state controller, and $\mathcal{E}$ an environment. A history $h=\textlangle\,\textlangle q^{(t)},s^{(t)}\textrangle\,\textrangle_{t=0}^{T}\in(Q\times\mathcal{S})^{<ω}$ of a system $\textlangle\mathcal{E},C\textrangle$ from the combined state $\textlangle q^{(0)},s^{(0)}\textrangle$ is a finite sequence of combined states such that $p^{(t+1)}=\Delta(s^{(t+1)}\ |\ s^{(t)},a^{(t)})>0$, where a^{(t)}:=γ\big{(}q^{(t)},Ω(s^{(t)})\big{)}, and q^{(t+1)}=δ\big{(}q^{(t)},Ω(s^{(t)})\big{)}, for each $0\leq t<T$. A history $h^{(0:T)}$ for a planning problem $\textlangle\mathcal{E},s_{0},\mathcal{G}\textrangle$ is terminating if $a^{(T)}=\text{{stop}}$. A terminating history for a planning problem $\textlangle\mathcal{E},s_{0},\mathcal{G}\textrangle$ is a goal history if $C$ terminates in a goal state: $a^{(T)}=\text{{stop}}$ and $s^{(T)}\in\mathcal{G}$. Unless otherwise noted, the first element of a history is $\textlangle q_{0},s_{0}\textrangle$.

Although the action $a^{(t)}$ is not included explicitly in the history, it can be obtained from $\textlangle q^{(t)},s^{(t)}\textrangle$.

The likelihood of a history $h$ is the probability that at each step $t$, the environment responds to the controller’s action $a^{(t)}$ with the next state $s^{(t+1)}$, and can be defined inductively based on the length of the history:

[TABLE]

The most immediate question here is this: in which sense would we say that a controller is adequate for a planning problem? In the absence of noise/nondeterminism, it is easy to show that the transition of combined states is deterministic; put differently, histories can be extended uniquely [9, 11]. So it suffices to argue that there is a terminating history and that it is a goal history. Of course, in the presence of nondeterminism, the extension of histories is no longer unique (because of nondeterministic action outcomes), and in the presence of probabilities, it is also useful to consider the likelihood of these extensions. We follow [2], where the notion of correctness from [12, 11] is extended for noise, and define:

Definition 5**.**

The total likelihood of termination of the system $\textlangle\mathcal{E},C\textrangle$ on a planning problem $\mathcal{P}$ is denoted by $\mathbf{LTER}$:

[TABLE]

Analogously, for goals, we define:

Definition 6**.**

The total likelihood of goal termination of the system $\textlangle\mathcal{E},C\textrangle$ on a planning problem $\mathcal{P}$ is denoted by $\mathbf{LGT}$:

[TABLE]

Finally, we state the search problems we want to solve.

Problem 1**.**

Given a planning problem $\mathcal{P}$, an integer $N$, ${\mathit{LGT}}^{\star}\in(0,1)$, find a finite-state controller with at most $N$ states such that $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ for $\mathcal{P}$.

A more fine-grained version is where a minimum bound on $\mathbf{LTER}$ is also possible, defined below:

Problem 2**.**

Given a planning problem $\mathcal{P}$, an integer $N$, ${\mathit{LTER}}^{\star}\in(0,1)$, ${\mathit{LGT}}^{\star}\in(0,1)$, find a finite-state controller with at most $N$ states that is $\mathbf{LTER}≥{\mathit{LTER}}^{\star}$ and $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ for $\mathcal{P}$.

We restrict our attention to solutions for Problem 1 for the most part, and turn to Problem 2 in a penultimate technical section.

3 Synthesizing classical controllers

Existing strategies for synthesizing FSCs include the compilation of generalized planning problems to classical ones [7], and the generalization of a sequential plan by abstraction [26].

From the perspective of an algorithmic schema, the generic technique of [11] is perhaps the simplest to analyze, based on AND-OR search. Here, an environment virtually identical to ours is assumed, and the transition relation is also nondeterministic (but non-probabilistic) via a state transition relation $\Delta\subseteq\mathcal{S}\times\mathcal{A}\times\mathcal{S}$. The pseudocode for the planner is in Algorithm 1. Initially, the algorithm starts with the empty controller $C_{ε}$, at the initial controller state $q^{(0)}$, with next states in $S_{0}$, the initial states of a generalized planning problem. The AND-step function enumerates the outcomes of an action from a given combined state and history, and calls OR-step to synthesize a controller that is correct for every outcome. The OR-step function enumerates the extensions of a controller for the current controller state and observation, and thus selects a next action for the current observation, and then calls AND-step to test for correctness recursively on the outcomes of the chosen action.111We provide the pseudocode of the algorithm to easily contrast it with our algorithm, but some details from [11] are omitted for the sake of exposition. The algorithm is essentially a blind search in controller space, reverting to the last non-deterministic choice point when a branch fails. The search space is trimmed in two ways. First, when a controller $C$ is found to be not correct, every extension of $C^{\prime}$ is dropped as well. Second, if $C\prec C^{\prime}$ (meaning that every controller transition defined by $C$ is the same in $C^{\prime}$), then the histories of $C$ that were already explored are not tested again for $C^{\prime}$. Most significantly, this exhaustive search results in the algorithm being sound and complete [11].

4 Problems with loops in a noisy environment

We identified three desiderata in the introduction, which we justify below. For D1, it is clear that there exist planning problems where even the optimal controller might not terminate on every run or end up in a goal state on every terminating run. (Consider a problem with an unavoidable dead end state, for example one where one outcome of a coin_flip action ends up in the goal, another outcome results in a dead end state. See Fig. 2.1.)

D2 is the result of assigning probabilities to the different outcomes of an action. If a history repeats a combined state at steps $n$ and $m$, and $\ell(h^{(0:n)})=\ell(h^{(0:m)})$, then the system will repeat the loop $h^{(n:m)}$ indefinitely, and never terminate. On the other hand, if $\ell(h^{(0:n)})>\ell(h^{(0:m)})$, and there exists a history $h^{\prime}$ from $h^{(n)}$ such that $h^{(0:n)}\cdot h^{\prime}$ terminates in $\mathcal{G}$, then $h^{(0:m)}\cdot h^{\prime}$ will also terminate in $\mathcal{G}$. (See Fig. 2.2.) This means that in a stochastic environment, tracking the likelihood of histories is essential.

For D3, in some environments no looping history has the property that $\ell(h^{(0:n)})=\ell(h^{(0:m)})$, and yet the system has no terminating runs. Fig. 2.3 illustrates a simple example, where executing action a in $s_{2}$ brings the environment either to $s_{0}$ or $s_{1}$, and from $s_{0}$ the only possible action leads deterministically to $s_{1}$ and from there back to $s_{2}$.

It is not possible to analyze every controller synthesis framework in the literature to verify its adherence to these desiderata, but, in the very least, the case of [11] (HD henceforth) is illustrative. Their procedure is correct for the dynamic environment in which they operate, but as can be inferred from the above examples, it easily follows that the procedure fails to meet the first two of the desiderata in stochastic environments.

Theorem 1**.**

The algorithm by HD returns with failure if every controller for the planning problem has at least one history that cannot be extended into a goal history.

Theorem 2**.**

The algorithm by HD returns with failure if every controller for the problem has at least one looping history.

More significantly, it is not possible to specify likelihood-based correctness criteria, which becomes essential for handling domains where actions fail, for example, and meta-level assumptions are unrealistic.

5 Algorithm for loopy planning

We propose a search algorithm that provably meets all three of the desiderata. It also instantiates an AND-OR search in that it simulates the runs of a system, enumerates the possible controller extensions whenever it reaches an undefined action, and when an action has multiple outcomes, it does a depth-first search on the next states recursively. However, it fixes the shortcomings stated in the previous section: instead of only allowing controllers that are correct on every run, it synthesizes controllers whose correctness likelihood exceeds some likelihood given as input to the algorithm; and it is capable of handling looping histories. As it is a probabilistic variant of the AND-OR search, we name it Pandor.

5.1 Allowing less than perfect controllers

The basic idea behind our planner is that it maintains an upper and lower bound for the $\mathbf{LGT}$ of the current controller, based on the histories simulated thus far. Whenever a failing run is encountered, the upper bound is decreased by the likelihood of this run; similarly, a goal run increases the lower bound on $\mathbf{LGT}$. When the lower bound exceeds the desired correctness likelihood (hereafter denoted by ${\mathit{LGT}}^{\star}$), the current controller is guaranteed to be “good enough”, and the algorithm returns with success. When the upper bound is lower than ${\mathit{LGT}}^{\star}$, none of the extensions of the controller is sufficiently good, and we revert the program state to the point of the last non-deterministic choice point. In the simplest variant of Pandor, any run with repeated combined states is counted as a failed run, thus it meets D1 but not D2. This property leads to an underestimation of the lower and upper bounds on $\mathbf{LGT}$, making the search sound but incomplete.

While the planner of [11] declared a controller and all of its extensions insufficiently good when it had a single failing run, we relax this condition. Now a controller is insufficiently good when the total likelihood of all of its failing runs exceeds $1-{\mathit{LGT}}^{\star}$; this results in the same behavior as that of its predecessor when ${\mathit{LGT}}^{\star}=1$.

5.2 Correctly counting looping histories

In order to account for looping histories, we draw on the following insight. Suppose that for a history $h^{(0:k)}$, there is a history $h_{{\mathrm{loop}}}$ from $h^{(k)}$ with $\mathit{end}(h_{{\mathrm{loop}}})=h^{(k)}$, and another history $h_{{\mathrm{goal}}}$ from $h^{(k)}$ that terminates in a goal state. A system with an FSC has the Markov property such that both the next action of the controller and the next state of the environment are defined by the current combined state. As a result, $h\cdot h_{\mathrm{goal}}$, $h\cdot h_{\mathrm{loop}}\cdot h_{\mathrm{goal}}$, $h\cdot h_{\mathrm{loop}}\cdot h_{\mathrm{loop}}\cdot h_{\mathrm{goal}}$ and so on are all valid goal histories, where the one with $m$ repetitions of $h_{\mathrm{loop}}$ has likelihood \ell(h)\big{(}\ell(h_{\mathrm{loop}})\big{)}^{m}\ell(h_{\mathrm{goal}}). These likelihoods form a geometric progression, whose sum for all $m\geq 0$ is \ell(h)\ell(h_{\mathrm{goal}})/\big{(}1-\ell(h_{\mathrm{loop}})\big{)}. (The existence of two distinct histories from $h^{(k)}$, namely $h_{\mathrm{goal}}$ and $h_{\mathrm{loop}}$, guarantees that $\ell(h_{\mathrm{loop}})<1$.) In the following, we describe how to utilize this argument.

We said that Pandor enumerates the histories of FSCs; let $h_{{\mathrm{curr}}}^{(0:n)}$ be the currently simulated history at some point during execution. Now we construct the set of all goal histories from pairwise disjoint sets of histories, one set for each $0\leq k\leq n$.

Denote by $H_{{\mathrm{loop}}}^{k}$ the set of histories $h_{{\mathrm{loop}}}$ from $h_{{\mathrm{curr}}}^{(k)}$ with the following properties:

• L1.

$\smash{h_{{\mathrm{loop}}}^{(0)}=h_{\vphantom{l}{\mathrm{curr}}}^{(k)}}$

• L2.

$\mathit{end}(h_{{\mathrm{loop}}})=\smash{h_{{\mathrm{curr}}}^{(k)}}$

• L3.

apart from its first and last element, $h_{\mathrm{loop}}$ doesn’t

L3.** contain ${h_{{\mathrm{curr}}}^{(k)}}$, and**

• L4.

no element of $h_{\mathrm{loop}}$ is equal to $\smash{h_{{\mathrm{curr}}}^{(i)}}$ for any $i<k$.

Furthermore, let $H_{{\mathrm{goal}}}^{k+1}$ denote the set of histories $h_{{\mathrm{goal}}}$ from $h_{{\mathrm{curr}}}^{(k)}$ with the following properties:

• W1.

${h_{{\mathrm{goal}}}^{(0)}=h_{\vphantom{l}{\mathrm{curr}}}^{(k)}}$

• W2.

$\mathit{end}(s_{{\mathrm{goal}}})\in\mathcal{G}$, and \smash{γ\big{(}Ω(\mathit{end}(h_{{\mathrm{goal}}}))\big{)}=\text{{stop}}}

• W3.

apart from its first element, $h_{\mathrm{goal}}$ doesn’t contain

W3. $h_{{\mathrm{curr}}}^{(k)}$,

• W4.

no element of $h_{\mathrm{goal}}$ is equal to $\smash{h_{{\mathrm{curr}}}^{(i)}}$ for any $i<k$,

• W5.

$\smash{h_{{\mathrm{goal}}}^{(1)}\neq h_{\vphantom{l}{\mathrm{curr}}}^{(k+1)}}$.

Condition W2 states that $h_{\mathrm{goal}}$ is a goal history. The other conditions collectively ensure that if $h^{\star}$ is a goal history from $h^{(k-1)}$ such that $h^{\star\,(1:)}$ doesn’t repeat any element of $h^{(:k-1)}$, then it is either W1–W5 for $k-1$, or it can be uniquely pieced together by elements of $H_{\mathrm{loop}}^{k}$ and $H_{\mathrm{goal}}^{k+1}$.

Lemma 1**.**

Let $h^{\star}$ meet W1–W4 for some $k$. Then either of these hold, but not both:

$h^{\star}\in H_{\mathrm{goal}}^{k}$, or

• 2.

there is a unique $m≥0$ such that for some $h_{{\mathrm{loop}},i}\in H_{\mathrm{loop}}^{k}$ for all $0\leq i\leq m$ and some $h_{{\mathrm{goal}}}\in H_{\mathrm{goal}}^{k+1}$, we have:

[TABLE]

Let $\tilde{\alpha}_{{\mathrm{goal}}}^{(k)}$ and $\tilde{\lambda}_{{\mathrm{loop}}}^{(k)}$ denote the sum of the likelihood of the elements of $H_{\mathrm{goal}}^{(k)}$ and $H_{\mathrm{loop}}^{(k)}$.

[TABLE]

The likelihood of the system terminating in a goal state (s.t.i.g.) if started in the initial state $h_{{\mathrm{curr}}}^{(0)}$ can be calculated inductively, as follows.

Lemma 2**.**

Let $\tilde{\lambda}_{{\mathrm{goal}}}^{(k)}$ denote the probability of s.t.i.g. after the history $h_{\mathrm{curr}}^{(:k-1)}$ without repeating any combined state of $h_{\mathrm{curr}}^{(:k-1)}$. Then the following hold for any $0\leq k<n$:

[TABLE]

where $p^{(k)}$ is the probability of transitioning from $h_{{\mathrm{curr}}}^{(k-1)}$ to $h_{\mathrm{curr}}^{(k)}$, i.e.

[TABLE]

This is because $\tilde{\lambda}_{{\mathrm{goal}}}^{(k)}$ is equal to the probability of s.t.i.g. from $h_{\mathrm{curr}}^{(:k)}$ without repeating $h_{\mathrm{curr}}^{(:k-1)}$  plus the probability of s.t.i.g. from $h_{\mathrm{curr}}^{(:k-1)}$ without repeating $h_{\mathrm{curr}}^{(:k-1)}$ if the $k$th combined state is not equal to $h_{\mathrm{curr}}^{(k)}$. The latter is simply $\tilde{\alpha}_{{\mathrm{goal}}}^{(k)}$, and the former is the sum of an infinite geometric series whose ratio is $\tilde{\lambda}^{(k)}_{\mathrm{loop}}$.

It is easy to see that with the natural definition of $h^{(:-1)}:=\textlangle\textrangle$, the probability of s.t.i.g. from $h_{\mathrm{curr}}^{(0)}$ is $\mathbf{LGT}$.

Lemma 3**.**

$\mathbf{LGT}=\tilde{\lambda}_{{\mathrm{goal}}}^{(0)}$**

5.3 Measuring the looping goal likelihood

While Pandor simulates the histories of a controller, it maintains variables $α_{{\mathrm{goal}}}^{(k)}$ for each $k$, which is the sum of likelihoods of the elements $h\in H_{\mathrm{goal}}^{(k)}$ such that $h_{{\mathrm{curr}}}^{(k-1)}\cdot h$ has already been visited. (This is done by increasing the relevant $α_{\mathrm{goal}}^{(k)}$ in the OR-step when the controller terminates in a goal state.) The following inequality trivially holds:

Lemma 4**.**

$α_{{\mathrm{goal}}}^{(k)}\leq\tilde{\alpha}_{{\mathrm{goal}}}^{(k)}$, with equality when every non-looping goal history from $h_{\mathrm{curr}}^{(k-1)}$ has been visited.

When a looping history is found in an OR-step, i.e., $\textlangle q,s\textrangle=h_{\mathrm{curr}}^{(k)}$ for some $k\leq\mathit{len}(h_{\mathrm{curr}})$, such that the likelihood of the loop is $\ell(h_{\mathrm{curr}}^{(k:n)})\cdot p=p_{\mathrm{loop}}<1$, then $α_{{\mathrm{loop}}}^{(k,m)}$ is increased by $p_{\mathrm{loop}}$. (Note that in the OR-step function, $h_{\mathrm{curr}}$ doesn’t yet include the current combined state.) The intuitive meaning of $α_{{\mathrm{loop}}}^{(k,m)}$ is the probability estimate of looping to $h^{(k)}$ after a history of $h^{(:m)}$ with not $h^{(m+1)}$ as the $(m+1)$-st step, without repeating any of $h^{(:m-1)}$ and repeating $h^{(m)}$ exactly once (Fig. 3). Now we can calculate $λ_{\mathrm{loop}}^{(k)}$: we can loop to step $k$ with not $h^{(k+1)}$ as the $(k+1)$-st step, or with $h^{(k+1:m)}$ as the next steps, repeating $h^{(m)}$ any number of times but then looping back to $h^{(k)}$ from $h^{(m)}$ without $h^{(m+1)}$ as the next step – for any $k<m\leq n$.

[TABLE]

This calculation is done in lines 48–51 of Alg. 3. The following result is proved easily by induction on $k$.

Lemma 5**.**

$λ_{\mathrm{loop}}^{(k)}\leq\tilde{\lambda}_{\mathrm{loop}}^{(k)}$, with equality when every once-looping history from $h_{\mathrm{curr}}^{(k)}$ has been visited.

Using Lemmas 4 and 5, the following can be seen:

Lemma 6**.**

$λ_{\mathrm{goal}}^{(k)}\leq\tilde{\lambda}_{\mathrm{goal}}^{(k)}$, with equality when every non-looping goal history from $h_{\mathrm{curr}}^{(k-1)}$ has been visited.

In Alg. 3, the CalcLambda function calculates $λ_{\mathrm{goal}}^{(0)}$ based on $\bm{\alpha}_{\mathrm{goal}}$, $\bm{\alpha}_{\mathrm{loop}}$, and $h_{\mathrm{curr}}$, and this $λ_{\mathrm{goal}}^{(0)}$ serves as the basis for termination in the AND-step.

5.4 Failing and non-terminating histories

We can treat failing histories (histories that terminate in a non-goal state) and histories that contain a non-decaying loop similarly to goal histories. We account for them via $α_{\mathrm{fail}}^{(k)}$ and $α_{\mathrm{noter}}^{(k)}$ values in a manner analogous to $α_{\mathrm{goal}}^{(k)}$.

We have similar results for the relevant $λ$ values as before:

Lemma 7**.**

$λ_{\mathrm{fail}}^{(k)}\leq\tilde{\lambda}_{\mathrm{fail}}^{(k)}$, with equality when every non-looping failing history from $h_{\mathrm{curr}}^{(k-1)}$ has been visited.

Calculating $λ_{\mathrm{noter}}^{(k)}$ is peculiar in that multiple decaying loops can add up to a a history that cannot be extended into a terminating history (Fig. 2.3). When no history from $h_{\mathrm{curr}}^{(k)}$ terminates, $\tilde{λ}_{\mathrm{loop}}^{(k+1)}+\tilde{λ}_{\mathrm{noter}}^{(k)}=1$ – for example, $h_{\mathrm{curr}}^{(k)}$ has an extension with likelihood $0.1$ with a non-decaying loop at the end, and another extension with likelihood $0.9$ loops back to $h_{\mathrm{curr}}^{(k)}$. When this happens, the values of $α_{\mathrm{loop}}^{(k:,k:)}$ are zeroed out, and $λ_{\mathrm{noter}}^{(k)}$ is assigned $p^{(k)}$. (Lines 74–77.) With this caveat, the inequality result for $λ_{\mathrm{noter}}$ is the following:

Lemma 8**.**

$\smash{λ_{\mathrm{noter}}^{(k)}\leq\tilde{\lambda}_{\mathrm{noter}}^{(k)}}$, with equality when every once-looping history from $h_{\mathrm{curr}}^{(k-1)}$ has been visited.

We now have classified histories as those that could be extended into terminating ones (either in a goal state or not) and those that have a non-decaying loop.

Lemma 9**.**

$\smash{\tilde{λ}_{\mathrm{goal}}^{(0)}+\tilde{λ}_{\mathrm{fail}}^{(0)}=\mathbf{LTER}=1-\tilde{λ}_{\mathrm{noter}}^{(0)}}$**

5.5 Rolling up the $\alpha$ values

Next, we see what should happen to the \smash{\alpha_{\mathord{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\bullet}}^{(\mathord{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\bullet})}} values when the current history changes. Clearly, when $h_{\mathrm{curr}}$ is extended, $α_{\mathrm{goal}}$ should be extended with an additional zero item, and $α_{\mathrm{loop}}$ with an additional row&column of zeros (lines 9–10).

When $h_{\mathrm{curr}}$ is shortened when the AND-step function returns, the last element (or last row&column) of these variables needs to be integrated to the previous ones before deleting them (CumulateAlpha function at lines 20, 44). The approach is similar to how the first iteration of $λ_{\mathrm{goal}}$ and $λ_{\mathrm{loop}}$ was calculated: in fact, the new $α$ values are chosen so that CalcLambda returns the same values before and after CumulateAlpha is called. It is important to note that this change in the $α$ values doesn’t affect our earlier results:

Lemma 10**.**

After \smash{α_{\mathord{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\bullet}}^{(\mathord{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\bullet})}} is assigned the values returned by CumulateAlpha, Lemmas 5, 6, 7, 8 still hold.

5.6 Correctness of the search

Our final theorem states that Pandor meets desiderata D1–D3, and solves Problem 1 correctly.

Theorem 3**.**

Given a planning problem $\mathcal{P}$, integer $N$, and ${\mathit{LGT}}^{\star}\in(0,1)$, the search algorithm Pandor is sound and complete: every FSC $C$ returned by Pandor-synth is $N\!$-bounded and $\mathbf{LGT}\geq{\mathit{LGT}}^{\star}$ for $\mathcal{P}$, and if there exists an $N\!$-bounded controller that is $\mathbf{LGT}\geq{\mathit{LGT}}^{\star}$ for $\mathcal{P}$, then one such FSC will be found.

Proof sketch.

Soundness. A controller $C$ is returned by Pandor-synth only if ${\mathit{LGT}}^{\star}\leq λ_{\mathrm{goal}}^{(0)}$

(line 2.14). By Lemmas 3 and 6:

[TABLE]

making the controller ${\mathit{LGT}}^{\star}≤\mathbf{LGT}$ for $\mathcal{P}$.

Completeness. Suppose there exists an $N\!$-bounded controller $C_{{\mathrm{good}}}$ which is $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ for $\mathcal{P}$.

Suppose a smaller controller $C^{\prime}\prec C_{\mathrm{good}}$ is rejected (property $\dagger$). A failing or non-terminating history of $C^{\prime}$ has the same property for $C_{\mathrm{good}}$ as well, and is a valid history for the system $\textlangle\mathcal{E},C_{\mathrm{good}}\textrangle$ (property $\ddagger$). A failing or non-terminating history does not terminate in a goal state (property $\star$).

[TABLE]

This is against the premise that $C_{\mathrm{good}}$ is $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$, contradiction: no smaller controller is rejected.

Suppose that when the current controller is $C^{\prime}\prec C_{\mathrm{good}}$, at a non-deterministic choice the next controller $C^{\prime\prime}$ is such that $C^{\prime}\prec C^{\prime\prime}\not\preceq C_{\mathrm{good}}$. If this execution branch of $C^{\prime\prime}$ does not fail, then a controller was returned, which was $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ by the soundness of the search.

In a finite environment, a system with an FSC has finitely many combined states. This implies that the number and length of the at-most-once-looping histories is bounded above, and so is the number of OR-steps required to explore these histories. At the end of the execution, every such history of $C$ has been simulated, resulting in $λ_{\mathrm{goal}}^{(0)}+λ_{\mathrm{fail}}^{(0)}+\penalty-100λ_{\mathrm{noter}}^{(0)}=1$ by Lemmas 6, 7, 8, and 9. At this time one of the termination conditions is fulfilled.

If at every non-deterministic choice, $C^{\prime\prime}$ is chosen such that $C^{\prime}\prec C^{\prime\prime}\preceq C_{\mathrm{good}}$, then as $C^{\prime\prime}$ can’t be rejected (by the argument above), either $C^{\prime\prime}$ or an extension of it will be returned. ∎

5.7 Planning for minimum likelihood of termination

The above results outline how our algorithm can plan for a minimum $\mathbf{LGT}$, but only minor modifications are required for setting a lower bound on $\mathbf{LTER}$ as well. Formally,

Problem 3**.**

Given a planning problem $\mathcal{P}$, an integer $N$, ${\mathit{LTER}}^{\star}\in(0,1)$, ${\mathit{LGT}}^{\star}\in(0,1)$, find a finite-state controller with at most $N$ states that is $\mathbf{LTER}≥{\mathit{LTER}}^{\star}$ and $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ for $\mathcal{P}$.

To solve this, the only change required in the pseudocode is in lines 14–18, where we simply extend the criteria for early termination and failure. These changes are shown in Alg. 4.

This new search process is sound and complete with respect to Problem 3.

Theorem 4**.**

Given a planning problem $\mathcal{P}$, integer $N$, ${\mathit{LTER}}^{\star}\in(0,1)$, and ${\mathit{LGT}}^{\star}\in(0,1)$, the search algorithm Pandor is sound and complete: every FSC $C$ returned by Pandor-synth is $N\!$-bounded and $\mathbf{LTER}\geq{\mathit{LTER}}^{\star}$ and $\mathbf{LGT}\geq{\mathit{LGT}}^{\star}$ for $\mathcal{P}$, and if there exists an $N\!$-bounded controller that is $\mathbf{LTER}\geq{\mathit{LTER}}^{\star}$ and $\mathbf{LGT}\geq{\mathit{LGT}}^{\star}$ for $\mathcal{P}$, then one such FSC will be found.

Proof sketch.

Soundness. A controller $C$ is returned by Pandor-synth only if ${\mathit{LGT}}^{\star}\leq λ_{\mathrm{goal}}^{(0)}$ and ${\mathit{LTER}}^{\star}\leq λ_{\mathrm{goal}}^{(0)}+λ_{\mathrm{fail}}^{(0)}$ (line 4.14). By Lemmas 3, 6, and 7, 9:

[TABLE]

making the controller ${\mathit{LGT}}^{\star}≤\mathbf{LGT}$ and ${\mathit{LTER}}^{\star}≤\mathbf{LTER}$ for $\mathcal{P}$.

Completeness. Suppose there exists an $N\!$-bounded controller $C_{{\mathrm{good}}}$ which is $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ and $\mathbf{LTER}≥{\mathit{LTER}}^{\star}$ for $\mathcal{P}$.

Suppose a smaller controller $C^{\prime}\prec C_{\mathrm{good}}$ is rejected – this can happen either for not meeting the bound on ${\mathit{LGT}}^{\star}$ (property $\dagger$) or on ${\mathit{LTER}}^{\star}$ ($\dagger\dagger$). A failing or non-terminating history of $C^{\prime}$ has the same property for $C_{\mathrm{good}}$ as well, and is a valid history for the system $\textlangle\mathcal{E},C_{\mathrm{good}}\textrangle$ (property $\ddagger$). A failing or non-terminating history does not terminate in a goal state (property $\star$). If the controller is rejected for $\dagger$, then inequality 11 holds, otherwise:

[TABLE]

Either Eq. 11 or Eq. 14 is against the premise that $C_{\mathrm{good}}$ is $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ and $\mathbf{LTER}≥{\mathit{LTER}}^{\star}$, contradiction: no smaller controller is rejected.

The algorithm terminates for the reasons described in the proof of Theorem 3.

Suppose that when the current controller is $C^{\prime}\prec C_{\mathrm{good}}$, at a non-deterministic choice the next controller $C^{\prime\prime}$ is such that $C^{\prime}\prec C^{\prime\prime}\not\preceq C_{\mathrm{good}}$. If this execution branch of $C^{\prime\prime}$ does not fail, then a controller was returned, which was $\mathbf{LGT}≥{\mathit{LGT}}^{\star}$ and $\mathbf{LTER}≥{\mathit{LTER}}^{\star}$ by the soundness of the search.

If at every non-deterministic choice, $C^{\prime\prime}$ is chosen such that $C^{\prime}\prec C^{\prime\prime}\preceq C_{\mathrm{good}}$, then as $C^{\prime\prime}$ can’t be rejected, either $C^{\prime\prime}$ or an extension of it will be returned. ∎

5.8 Time and space complexity

In order to explore the whole environment with a given controller, we need to take $O(b^{h_{\text{max}}})$ steps, where $b$ is the branching factor at the AND-step (the maximum number of outcomes of an action), and $h_{\text{max}}$ is the length of the longest possible history without a repeated state (i.e. $h_{\text{max}}\leq|\mathcal{S}|$). At every AND-step, Pandor needs to calculate the $\lambda$ vectors, which takes $O(h_{\text{max}}^{2})$ steps due to the size of $\alpha_{\text{loop}}$. This exploration needs to be done, usually to different depths, for every possible non-isomorphic $N$-bounded FSC, which we denote by $\#_{C}$. A controller is defined by its transitions, hence $\#_{C}<(N\cdot|\mathcal{O}|)^{N\cdot|\mathcal{A}|}$. It follows that the time complexity of the algorithm is $O(b^{h_{\text{max}}}\cdot\#_{C}\cdot h_{\text{max}}^{2})=O(b^{h_{\text{max}}}\cdot\#_{C}$).

These numbers are realized in an adversarial environment with extremely low probability (depending on the action/outcome selection); in most realistic situations (i.e., non-adversarial environments), failure/success would be orders of magnitude quicker. First, whenever a controller is found to not meet the desired ${\mathit{LGT}}^{\star}$, all of its extensions are discarded immediately, leaving us with $\#_{C}\ll(N\cdot|\mathcal{O}|)^{N\cdot|\mathcal{A}|}$. Secondly, most controllers are unable to explore the whole environment, and require orders of magnitude fewer than $b^{h_{\text{max}}}$ steps. We believe the search process could be further improved using heuristics.

Analogously, we need to store the alpha vectors and the $\alpha_{\text{loop}}$ matrix at each controller extension, which each require $O(h_{\text{max}}^{2})$ space. If the maximum number of controller transitions is $\#_{T}$ (where $\#_{T}\leq N\cdot|\mathcal{O}|$), then this results in a space complexity of $O(h_{\text{max}}^{2}\cdot\#_{T})$.

6 Related Work

Our results are related to a number of recent approaches on bounded search and FSC synthesis, but as we discuss below, the nature of our results and the thrust of our proof strategy is significantly different from these approaches. At the outset, our contributions should be seen as a full generalization of [11] to stochastic domains, in that it provides a generic technique for FSC synthesis in a whole range of planning frameworks (cf. [11]) that can now be considered with probabilistic nondeterminism.

The work of [11] is positioned in the area of generalized planning. We will briefly touch on approaches to generating loopy plans, and then discuss related correctness concerns.

Early approaches to loopy plans can be seen as deductive methodologies, often influenced by program synthesis and correctness [10]. Manna and Waldinger [19] obtained recursive plans by matching induction rules, and [28] refine generic plan specifications, but required input from humans. See [18] for a recent approach using induction.

Most recent proposals differ considerably from this early work using deduction:

[16] expects two parameters with the planning problem; the approach plans for the first parameter, winds it to form loops and tests it for the second.

• 2.

[29] synthesize a plan sequence with partial orderings, and exploit repeated occurrences of subplans to obtain loops.

• 3.

[26] considers an abstract state representation that groups objects into equivalences classes, the idea being that any concrete plan can be abstracted wrt these classes and repeated occurrences of subplans can be leveraged to generate compact loopy plans.

• 4.

[7] integrate the dynamics of a memoryless plan with a planning problem, and convert that to a conformant planning problem; the solution to this latter problem is shown to generalize to multiple instances of the original problem.

• 5.

[11] propose a bounded AND/OR search procedure that is able to synthesize loopy plans, which is what we build on.

On the matter of correctness, [15] argued that generalized plans be tested for termination and correctness against all problem instances; [17] extended this account to define goal achievability. In later work, [9] defined the notions of weak, strong and strong cyclic solutions in the presence of nondeterminism.222Variant additional stipulations in the literature include things like fairness, where every outcome of a nondeterministic action must occur infinitely often [6]. These notions are widely used in the planning community [6]; see, for example, [3] for an account of strong planning with a sensor model. Recently, [27] synthesize loopy plans in domains with nondeterministic quantitative effects, for which strong cyclic solutions are studied. Our account of correctness is based on [2], which generalized Levesque’s account [15].

Synthesizing FSCs is a very active area of research within Markov Decision Processes (MDPs) and partially observable MDPs (POMDPs) [22, 23, 1]. But the majority of algorithms in this space either solve an approximation of the problem, or they come without correctness guarantees. In contrast, emphasizing correctness, [14] show how FSC synthesis for POMDPs can be reduced to parameterized Markov chains, under the requirement of almost-sure plans that do not enter bad states. Similarly, [8] propose the synthesis of almost-sure plans by means of a SAT-based oracle. Not only are the algorithms significantly different from our own, but the correctness specification too is formulated differently. Thus, our contributions are complementary to this major body of work, and orthogonal to a large extent; for the future, it would be interesting to relate these strategies more closely.

When it comes to similarity to our algorithms, there are a variety of approaches based on bounded AND-OR search, such as AO∗, LAO∗, and LRTDP (e.g., [5]). Here too, the specification criteria, the correctness bound and the nature of the analysis are largely orthogonal to ours. For example, LAO∗ allows for loops, but the solution is not necessarily a sound and complete N-bounded FSC: it yields a partial policy and does not allow for arbitrary likelihood scenarios (e.g., an anytime bound such as the goal of generating a FSC where >20% of the paths reach the goal state). Perhaps one could think of the difference between LAO∗ and LRTDP vs. Pandor as being analogous to the difference between the paradigms of dynamic programming vs. Monte Carlo methods. In fact, we think our proposal is suitable to combine the best of the two worlds, but that is a topic for future research. We are also excited about the prospect of extending our contributions to the continuous case, and potentially providing asymptotic guarantees for provably correct FSC synthesis.

7 Conclusions and Discussion

In this paper, we presented new theoretical results on a generic technique for synthesizing FSCs in stochastic environments, allowing for highly granular specifications on termination and goal satisfaction. We then proved the soundness and completeness of that synthesis algorithm.

As discussed above, the contributions of this paper are solely on the theoretical front. Nonetheless, we will release a proof-of-concept implementation of the pseudocode in Alg. 2 and 3.333The implementation can be accessed at https://github.com/treszkai/pandor In our preliminary evaluations, we observed that in deterministic domains, our planner has the same runtime as the planner of [11], and the difference is only a small linear factor for additional bookkeeping. But suppose we were to consider a noisy variant of the Hall-A domain in Fig. 1, where every action has a 50-50% probability of either succeeding or leaving the current state unchanged. Here, because moving left in cell B is not guaranteed to succeed, we can see that an extra transition is required to move the agent out of B in case the first attempt fails (\smash{q_{1}\xrightarrow{\raisebox{-2.15277pt}[4.30554pt][0.0pt]{\scriptstyle B\ :\ \leftarrow}}q_{0}}). And indeed, the FSC synthesized by Pandor contains this transition:

q_{0}$$q_{1}\pgfmathresultptA:\ \rightarrow$$-:\ \rightarrow$$B:\ \leftarrow$$-:\ \leftarrow$$A:\text{{stop}}$$B:\ \leftarrow

There are many interesting directions for the future. For example, one could investigate: (a) effective sampling strategies; (b) the tradeoff between higher LGT bounds vs scalability (i.e., demands on LGT bounds may be different across applications); and (c) the merits and demerits of the various correctness criteria from the literature for safety-critical applications. To that end, along with recent advances in the area, we hope that our results provide theoretical foundations, new proof strategies and a fresh perspective on FSC synthesis in stochastic domains.