11institutetext:  Brno University of Technology, Brno, Czech Republic
11email<EMAIL_ADDRESS>22institutetext: RWTH Aachen University, Aachen,
Germany 33institutetext: Radboud University, Nijmegen, The Netherlands

0

# Search and Explore:
Symbiotic Policy Synthesis in POMDPs††thanks: This work has been supported by
the Czech Science Foundation grant GA23-06963S (VESCAA), the ERC AdG Grant
787914 (FRAPPANT) and the DFG RTG 2236/2 (UnRAVeL).

Roman Andriushchenko 11 Alexander Bork  22 Milan Češka (✉)  11
Sebastian Junges 33 Joost-Pieter Katoen 22 Filip Macák 11

###### Abstract

This paper marries two state-of-the-art controller synthesis methods for
partially observable Markov decision processes (POMDPs), a prominent model in
sequential decision making under uncertainty. A central issue is to find a
POMDP controller—that solely decides based on the observations seen so far—to
achieve a total expected reward objective. As finding optimal controllers is
undecidable, we concentrate on synthesising good finite-state controllers
(FSCs). We do so by tightly integrating two modern, orthogonal methods for
POMDP controller synthesis: a belief-based and an inductive approach. The
former method obtains an FSC from a finite fragment of the so-called belief
MDP, an MDP that keeps track of the probabilities of equally observable POMDP
states. The latter is an inductive search technique over a set of FSCs, e.g.,
controllers with a fixed memory size. The key result of this paper is a
symbiotic anytime algorithm that tightly integrates both approaches such that
each profits from the controllers constructed by the other. Experimental
results indicate a substantial improvement in the value of the controllers
while significantly reducing the synthesis time and memory footprint.

##  1 Introduction

A formidable synthesis challenge is to find a decision-making policy that
satisfies temporal constraints even in the presence of stochastic noise.
_Markov decision processes (MDPs)_ [26] are a prominent model to reason about
such policies under stochastic uncertainty. The underlying decision problems
are efficiently solvable and probabilistic model checkers such as PRISM [22]
and Storm [13] are well-equipped to synthesise policies that provably (and
optimally) satisfy a given specification. However, a major shortcoming of MDPs
is the assumption that the policy can depend on the precise state of a system.
This assumption is unrealistic whenever the state of the system is only
observable via sensors. _Partially observable MDPs (POMDPs)_ overcome this
shortcoming, but policy synthesis for POMDPs and specifications such as _the
probability to reach the exit is larger than 50 $\%$_ requires solving
undecidable problems [23]. Nevertheless, in recent years, a variety of
approaches have been successfully applied to a variety of challenging
benchmarks, but the approaches also fail somewhat spectacularly on seemingly
tiny problem instances. From a user perspective, it is hard to pick the right
approach without detailed knowledge of the underlying methods. This paper sets
out to develop a framework in which conceptually orthogonal approaches
symbiotically alleviate each other’s weaknesses and find policies that
maximise, e.g., the expected reward before a target is reached. We show
empirically that the combined approach can find compact policies achieving a
significantly higher reward than the policies that either individual approach
constructs.

PayntStorm${\mathcal{F}^{\mathcal{M}}_{k}}=\\{F_{1},\dots,F_{m}\\}$MDP
$\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})$MDPmodel checkingcandidate
FSCobservation-based?refinement of familypruning of familyFSC
$F_{\mathcal{I}}$unfold fragmentof belief MDPcut offunexploredbeliefsMDPmodel
checkingobs.-basedpolicy onbelief MDPheuristic boundsFSC
$F_{\mathcal{B}}$abstrspec holdsspec violatedYESNOprovide boundsshrink

Figure 1: Schematic depiction of the symbiotic approach

##### Belief exploration.

Several approaches for solving POMDPs use the notion of _beliefs_ [27]. The
key idea is that each sequence of observations and actions induces a belief—a
distribution over POMDP states that reflects the probability to be in a state
conditioned on the observations. POMDP policies can decide optimally solely
based on the belief. The evolution of beliefs can be captured by a fully
observable, yet possibly infinite _belief MDP_. A practical approach (see the
lower part of Fig. 1) is to unfold a finite fragment of this belief MDP and
make its frontier absorbing. This finite fragment can be analysed with off-
the-shelf MDP model checkers. Its accuracy can be improved by using an
arbitrary but fixed cut-off policy from the frontier onwards. Crucially, the
probability to reach the target under such a policy can be efficiently pre-
computed for all beliefs. This paper considers the belief exploration method
from [8] realised in Storm [13].

##### Policy search.

An orthogonal approach searches a (finite) space of policies [14, 24] and
evaluates these policies by verifying the induced Markov chain. To ensure
scalability, sets of policies must be efficiently analysed. However, policy
spaces explode whenever they require memory. The open challenge is to
adequately define the space of policies to search in. In this paper, we
consider the policy-search method from [5] as implemented in Paynt [6] that
explores spaces of finite-state controllers (FSCs), represented as
deterministic Mealy machines [2], using a combination of abstraction-
refinement, counterexamples (to prune sets of policies), and increasing a
controller’s memory, see the upper part of Fig. 1.

##### Our symbiotic approach.

In essence, our idea relies on the fact that a policy found via one approach
can boost the other approach. The key observation is that such a policy is
beneficial even when it is sub-optimal in terms of the objective at hand. Fig.
1 sketches the symbiotic approach. The FSCs $F_{\mathcal{I}}$ obtained by
policy search are used to guide the partial belief MDP to the target. Vice
versa, the FSCs $F_{\mathcal{B}}$ obtained from belief exploration are used to
shrinken the set of policies and to steer the abstraction. Our experimental
evaluation, using a large set of POMDP benchmarks, reveals that (a) belief
exploration can yield better FSCs (sometimes also faster) using FSCs
$F_{\mathcal{I}}$ from Paynt—even if the latter FSCs are far from optimal, (b)
policy search can find much better FSCs when using FSCs from belief
exploration, and (c) the FSCs from the symbiotic approach are superior in
value to the ones obtained by the standalone approaches.

##### Beyond exploration and policy search.

In this work, we focus on two powerful orthogonal methods from the set of
belief-based and search-based methods. Alternatives exist. Exploration can
also be done using a fixed set of beliefs [25]. Prominently, HSVI [18] and
SARSOP [20] are belief-based policy synthesis approaches typically used for
discounted properties. They also support undiscounted properties, but
represent policies with $\alpha$-vectors. Bounded policy synthesis [29] uses a
combination of belief-exploration and inductive synthesis over paths and
addresses finite horizon reachability. $\alpha$-vector policies lead to more
complex analysis downstream: the resulting policies must track the belief and
do floating-point computations to select actions. For policy search, prominent
alternatives are to search for randomised controllers via gradient descent
[17] or via convex optimization [1, 19, 12]. Alternatively, FSCs can be
extracted via deep reinforcement learning [9]. However, randomised policies
limit predictability, which hampers testing and explainability. The area of
programmatic reinforcement learning [28] combines inductive synthesis ideas
with RL. While our empirical evaluation is method-specific, the lessons carry
over to integrating other methods.

##### Contributions.

The key contribution of this paper is the symbiosis of belief exploration [8]
and policy search [5]. Though this seems natural, various technical obstacles
had to be addressed, e.g., obtaining $F_{\mathcal{B}}$ from the finite
fragment of the belief MDP and the policies for its frontier and developing an
interplay between the exploration and search phases that minimises the
overhead. The benefits of the symbiotic algorithm are manifold, as we show by
a thorough empirical evaluation. It can solve POMDPs that cannot be tackled
with either of the two approaches alone. It outputs FSCs that are superior in
value (with relative improvements of up to 40%) as well as FSCs that are more
succinct (with reduction of a factor of up to two orders of magnitude) with
only a small penalty in their values. Additionally, the integration reduces
the memory footprint compared to belief exploration by a factor of 4. In
conclusion, the proposed symbiosis offers a powerful push-button, anytime
synthesis algorithm producing, in the given time, superior and/or more
succinct FSCs compared to the state-of-the-art methods.

##  2 Motivating Examples

We give a sample POMDP that is hard for the belief exploration, a POMDP that
challenges the policy search approach, and indicate why a symbiotic approach
overcomes this. A third sample POMDP is shown to be unsolvable by either
approach alone but can be treated by the symbiotic one.

(a)

(b)

(c)

Figure 2: (a) and (b) contain two POMDPs. Colours encode observations.
Unlabelled transitions have probability 1. Omitted actions (e.g.
$\gamma,\delta$ in state $B_{2}$) execute a self-loop. (c) Markov chain
induced by the minimising policy ${\sigma_{\mathcal{B}}}$ in the finite
abstraction $\overline{\mathcal{M}^{\mathcal{B}}_{a}}$ of the POMDP from Fig.
2(a). In the rightmost state, policy $\overline{F}$ is applied (cut-off),
allowing to reach the target in $\rho$ steps.

####  2.0.1 A challenging POMDP for belief-based exploration.

Consider POMDP $\mathcal{M}_{a}$ in Fig. 2(a). The objective is to minimise
the expected number of steps to the target $T_{a}$. An optimal policy is to
always take action $\alpha$ yielding 4 expected steps. An FSC realising this
policy can be found by a policy search under 1s.

##### Belief MDPs.

States in the _belief MDP_ $\mathcal{M}^{\mathcal{B}}_{a}$ are _beliefs_ ,
probability distributions over POMDP states with equal observations. The
initial belief is $\\{S\mapsto 1\\}$. By taking action $\alpha$, ‘yellow’ is
observed and the belief becomes
$\\{L\mapsto\frac{1}{2},\,R\mapsto\frac{1}{2}\\}$. Closer inspection shows
that the set of reachable beliefs is infinite rendering
$\mathcal{M}^{\mathcal{B}}_{a}$ to be infinite. Belief exploration constructs
a finite fragment $\overline{\mathcal{M}^{\mathcal{B}}_{a}}$ by exploring
$\mathcal{M}^{\mathcal{B}}_{a}$ up to some depth while _cutting off_ the
frontier states. From cut-off states, a shortcut is taken directly to the
target. These shortcuts are heuristic over-approximations of the true number
of expected steps from the cut-off state to the target. The finite MDP
$\overline{\mathcal{M}^{\mathcal{B}}_{a}}$ can be analysed using off-the-shelf
tools yielding the minimising policy ${\sigma_{\mathcal{B}}}$ assigning to
each belief state the optimal action.

##### Admissible heuristics.

A simple way to over-approximate the minimal number of the expected number of
steps to the target is to use an arbitrary controller $\overline{F}$ and use
the expected number of steps under $\overline{F}$. The latter is cheap if
$\overline{F}$ is compact, as detailed in Sec. 4.2. Fig. 2(c) shows a Markov
chain induced by ${\sigma_{\mathcal{B}}}$ in
$\overline{\mathcal{M}^{\mathcal{B}}_{a}}$, where the belief
$\\{L\mapsto\frac{7}{8},R\mapsto\frac{1}{8}\\}$ is cut off using
$\overline{F}$. The belief exploration in Storm [8] unfolds 1000 states of
$\mathcal{M}^{\mathcal{B}}_{a}$ and finds controller $\overline{F}$ that
uniformly randomises over all actions in the rightmost state. The resulting
sub-optimal controller $F_{\mathcal{B}}$ reaches the target in ${\approx}4.1$
steps. Exploring only a few states suffices when replacing $\overline{F}$ by a
(not necessarily optimal) FSC provided by a policy search.

####  2.0.2 A challenging POMDP for policy search.

Consider POMDP $\mathcal{M}_{b}$ in Fig. 2(b). The objective is to minimise
the expected number of steps to $T_{b}$. Its 9-state belief MDP
$\mathcal{M}^{\mathcal{B}}_{b}$ is trivial for the belief-based method. Its
optimal controller ${\sigma_{\mathcal{B}}}$ first picks action $\gamma$; on
observing ‘yellow’ it plays $\beta$ twice, otherwise it always picks $\alpha$.
This is realised by an FSC with 3 memory states. The inductive policy search
in Paynt [5] explores families of FSCs of increasing complexity, i.e., of
increasing memory size. It finds the optimal FSC after consulting about 20
billion candidate policies. This requires 545 model-checking queries; the
optimal one is found after 105 queries while the remaining queries prove that
no better 3-state FSC exists.

##### Reference policies.

The policy search is guided by a reference policy, in this case the fully
observable MDP policy that picks (senseless) action $\delta$ in $B_{1}$ first.
Using policy ${\sigma_{\mathcal{B}}}$—obtained by the belief method—instead,
$\delta$ is never taken. As ${\sigma_{\mathcal{B}}}$ picks in each ‘blue’
state a different action, mimicking this requires at least three memory
states. Using ${\sigma_{\mathcal{B}}}$ reduces the total number of required
model-checking queries by a factor of ten; the optimal 3-state FSC is found
after 23 queries.

####  2.0.3 The potential of symbiosis.

To further exemplify the limitation of the two approaches and the potential of
their symbiosis, we consider a synthetic POMDP, called Lanes+, combining a
Lane model with larger variants of the POMDPs in Fig. 2; see Tab. 2 on page 2
for the model statistics and Appendix C of [3] for the model description. We
consider minimisation of the expected number of steps and a 15-minute timeout.
The belief-based approach by Storm yields the value 18870. The policy search
method by Paynt finds an FSC with 2 memory states achieving the value 8223.
This sub-optimal FSC significantly improves the belief MDP approximation and
enables Storm to find an FSC with value 6471. The symbiotic synthesis loop
finds the optimal FSC with value 4805.

##  3 Preliminaries and Problem Statement

A (discrete) _distribution_ over a countable set $A$ is a function $\mu\colon
A\rightarrow[0,1]$ s.t. $\sum_{a}\mu(a)=1$. The set
$\mathrm{supp}(\mu)\coloneqq\left\\{a\in A\mid\mu(a)>0\right\\}$ is the
_support_ of $\mu$. The set $Distr(A)$ contains all distributions over $A$. We
use Iverson bracket notation, where $\left[x\right]=1$ if the Boolean
expression $x$ evaluates to true and $\left[x\right]=0$ otherwise.

######  Definition 1 (MDP)

A _Markov decision process (MDP)_ is a tuple $M=(S,s_{0},Act,\mathcal{P})$
with a countable set $S$ of states, an initial state $s_{0}\in S$, a finite
set $Act$ of actions, and a partial transition function $\mathcal{P}\colon
S\times Act\nrightarrow Distr(S)$. $Act(s)\coloneqq\left\\{\alpha\in
Act\mid\mathcal{P}(s,\alpha)\neq\bot\right\\}$ denotes the set of actions
available in state $s\in S$. An MDP with $|Act(s)|=1$ for each $s\in S$ is a
_Markov chain (MC)_.

Unless stated otherwise, we assume $Act(s)=Act$ for each $s\in S$ for
conciseness. We denote
$\mathcal{P}(s,\alpha,s^{\prime})\coloneqq\mathcal{P}(s,\alpha)(s^{\prime})$.
A (finite) _path_ of an MDP $M$ is a sequence
$\pi=s_{0}\alpha_{0}s_{1}\alpha_{1}\dots s_{n}$ where
${\mathcal{P}(s_{i},\alpha_{i},s_{i+1})>0}$ for $0\leq i<n$. We use
$last(\pi)$ to denote the last state of path $\pi$. Let $Paths^{M}$ denote the
set of all finite paths of $M$. State $s$ is absorbing if
$\mathrm{supp}(\mathcal{P}(s,\alpha))=\\{s\\}$ for all $\alpha\in Act$.

######  Definition 2 (POMDP)

A _partially observable MDP (POMDP)_ is a tuple $\mathcal{M}=(M,Z,O)$, where
$M$ is the underlying MDP, $Z$ is a finite set of observations and $O\colon
S\rightarrow Z$ is a (deterministic) observation function.

For POMDP $\mathcal{M}$ with underlying MDP $M$, an _observation trace_ of
path $\pi=s_{0}\alpha_{0}s_{1}\alpha_{1}\dots s_{n}$ is a sequence
$O(\pi)\coloneqq O(s_{0})\alpha_{0}O(s_{1})\alpha_{1}\dots O(s_{n})$. Every
MDP can be interpreted as a POMDP with $Z=S$ and $O(s)=s$ for all $s\in S$.

A (deterministic) _policy_ is a function $\sigma\colon Paths^{M}\rightarrow
Act$. Policy $\sigma$ is _memoryless_ if
$last(\pi)=last(\pi^{\prime})\Longrightarrow\sigma(\pi)=\sigma(\pi^{\prime})$
for all $\pi,\pi^{\prime}\in Paths^{M}$. A memoryless policy $\sigma$ maps a
state $s\in S$ to action $\sigma(s)$. Policy $\sigma$ is _observation-based_
if $O(\pi)=O(\pi^{\prime})\Longrightarrow\sigma(\pi)=\sigma(\pi^{\prime})$ for
all $\pi,\pi^{\prime}\in Paths^{M}$. For POMDPs, we always consider
observation-based policies. We denote by $\Sigma_{\mathit{obs}}$ the set of
all observation-based policies. A policy $\sigma\in\Sigma_{\mathit{obs}}$
induces the MC $\mathcal{M}^{\sigma}$.

We consider indefinite-horizon reachability or expected total reward
properties. Formally, let $M=(S,s_{0},Act,\mathcal{P})$ be an MC, and let
$T\subseteq S$ be a set of _target states_.
$\mathbb{P}^{M}\left[s\models\Diamond T\right]$ denotes the probability of
reaching $T$ from state $s\in S$. We use $\mathbb{P}^{M}\left[\Diamond
T\right]$ to denote $\mathbb{P}^{M}\left[s_{0}\models\Diamond T\right]$ and
omit the superscript if the MC is clear from context. Now assume POMDP
$\mathcal{M}$ with underlying MDP $M=(S,s_{0},Act,\mathcal{P})$, and a set
$T\subseteq S$ of absorbing target states. Without loss of generality, we
assume that the target states are associated with the unique observation
$z^{T}\in Z$, i.e. $s\in T$ iff $O(s)=z^{T}$. For a POMDP $\mathcal{M}$ and
$T\subseteq S$, the _maximal reachability probability_ of $T$ for state $s\in
S$ in $\mathcal{M}$ is $\mathbb{P}^{\mathcal{M}}_{\max}\left[s\models\Diamond
T\right]\coloneqq\sup_{\sigma\in\Sigma_{\mathit{obs}}}\mathbb{P}^{\mathcal{M}^{\sigma}}\\!\left[s\models\Diamond{T}\right]$.
The minimal reachability probability
$\mathbb{P}^{\mathcal{M}}_{\min}\left[s\models\Diamond T\right]$ is defined
analogously.

Finite-state controllers are automata that compactly encode policies.

######  Definition 3 (FSC)

A _finite-state controller (FSC)_ is a tuple $F=(N,n_{0},\gamma,\delta)$, with
a finite set $N$ of _nodes_ , the _initial node_ $n_{0}\in N$, the _action
function_ $\gamma\colon N\times Z\rightarrow Act$ and the _update function_
$\delta\colon N\times Z\times Z\rightarrow N$.

A _$k$ -FSC_ is an FSC with $|N|=k$. If $k{=}1$, the FSC encodes a memoryless
policy. We use $\mathcal{F}^{\mathcal{M}}$ (${\mathcal{F}^{\mathcal{M}}_{k}}$)
to denote the family of all ($k$-)FSCs for POMDP $\mathcal{M}$. For a POMDP in
state $s$, an agent receives observation $z=O(s)$. An agent following an FSC
$F$ executes action $\alpha=\gamma(n,z)$ associated with the current node $n$
and the current (prior) observation $z$. The POMDP state is updated
accordingly to some $s^{\prime}$ with $\mathcal{P}(s,\alpha,s^{\prime})>0$.
Based on the next (posterior) observation $z^{\prime}=O(s^{\prime})$, the FSC
evolves to node $n^{\prime}=\delta(n,z,z^{\prime})$. The _induced MC_ for FSC
$F$ is $\mathcal{M}^{F}=(S\times
N,(s_{0},n_{0}),\\{\alpha\\},\mathcal{P}^{F})$, where for all
$(s,n),(s^{\prime},n^{\prime})\in S\times N$ we have

$\mathcal{P}^{F}\left((s,n),\alpha,(s^{\prime},n^{\prime})\right)=\left[n^{\prime}=\delta\left(n,O(s),O(s^{\prime})\right)\right]\cdot\mathcal{P}(s,\gamma(n,O(s)),s^{\prime}).$

We emphasise that for MDPs with infinite state space and POMDPs, an FSC
realising the maximal reachability probability generally does not exist. For
FSC $F\in\mathcal{F}^{\mathcal{M}}$ with the set $N$ of memory nodes, let
$\mathbb{P}^{\mathcal{M}^{F}}\\!\left[(s,n)\models\Diamond{T}\right]\coloneqq\mathbb{P}^{\mathcal{M}^{F}}\left[{(s,n)\models\Diamond(T\times
N)}\right]$ denote the probability of reaching target states $T$ from state
$(s,n)\in S\times N$. Analogously,
$\mathbb{P}^{\mathcal{M}^{F}}\\!\left[\Diamond{T}\right]\coloneqq\mathbb{P}^{\mathcal{M}^{F}}\left[\Diamond(T\times
N)\right]$ denotes the probability of reaching target states $T$ in the MC
$\mathcal{M}^{F}$ induced on $\mathcal{M}$ by $F$.

Problem statement. The classical synthesis problem [23] for POMDPs asks: given
POMDP $\mathcal{M}$, a set $T$ of targets, and a threshold $\lambda$, find an
FSC $F$ such that
$\mathbb{P}^{\mathcal{M}^{F}}\\!\left[\Diamond{T}\right]\geq\lambda$, if one
exists. We take a more practical stance and aim instead to optimise the value
$\mathbb{P}^{\mathcal{M}^{F}}\\!\left[\Diamond{T}\right]$ in an anytime
fashion: the faster we can find FSCs with a high value, the better.

###### Remark 1

Variants of the maximising synthesis problem for the expected total reward and
minimisation are defined analogously. For conciseness, in this paper, we
always assume that we want to maximise the value.

In addition to the value of the FSC $F$, another key characteristic of the
controller is its _size_ , which we treat as a secondary objective and discuss
in detail in Sec. 6.

##  4 FSCs for and from Belief Exploration

We consider _belief exploration_ as described in [8]. A schematic overview is
given in the lower part of Fig. 1. We recap the key concepts of belief
exploration. This section explains two contributions: we discuss how arbitrary
FSCs are included and present an approach to export the associated POMDP
policies as FSCs.

###  4.1 Belief Exploration With Explicit FSC Construction

Finite-state controllers for a POMDP can be obtained by analysing the (fully
observable) _belief MDP_ [27]. The state space of this MDP consists of
_beliefs_ : probability distributions over states of the POMDP $\mathcal{M}$
having the same observation. Let $S_{z}\coloneqq\\{s\in S\mid O(s)=z\\}$
denote the set of all states of $\mathcal{M}$ with observation $z\in Z$. Let
the set of all beliefs $\mathcal{B}_{\mathcal{M}}\coloneqq\bigcup_{z\in
Z}Distr(S_{z})$ and denote for $b\in\mathcal{B}_{\mathcal{M}}$ by $O(b)\in Z$
the unique observation $O(s)$ of any $s\in\mathrm{supp}(b)$.

In a belief $b$, taking action $\alpha$ yields an updated belief as follows:
let $\mathcal{P}(b,\alpha,z^{\prime})\coloneqq\sum_{s\in
S_{O(b)}}b(s)\cdot\sum_{s^{\prime}\in
S_{z^{\prime}}}\mathcal{P}(s,\alpha,s^{\prime})$ denote the probability of
observing $z^{\prime}\in Z$ upon taking action $\alpha\in Act$ in belief
$b\in\mathcal{B}_{\mathcal{M}}$. If $\mathcal{P}(b,\alpha,z^{\prime})>0$, the
corresponding successor belief $b^{\prime}=\llbracket
b{\mid}\alpha,z^{\prime}\rrbracket$ with $O(b^{\prime})=z^{\prime}$ is defined
component-wise as

$\llbracket
b{\mid}\alpha,z^{\prime}\rrbracket(s^{\prime})\coloneqq\frac{\sum_{s\in
S_{O(b)}}b(s)\cdot\mathcal{P}(s,\alpha,s^{\prime})}{\mathcal{P}(b,\alpha,z^{\prime})}$

for all $s^{\prime}\in S_{z^{\prime}}$. Otherwise, $\llbracket
b{\mid}\alpha,z^{\prime}\rrbracket$ is undefined.

######  Definition 4 (Belief MDP)

The _belief MDP_ of POMDP $\mathcal{M}$ is the MDP
$\mathcal{M}^{\mathcal{B}}=(\mathcal{B}_{\mathcal{M}},b_{0},Act,\mathcal{P}^{\mathcal{B}})$,
with initial belief $b_{0}\coloneqq\\{s_{0}\mapsto 1\\}$ and transition
function
$\mathcal{P}^{\mathcal{B}}(b,\alpha,b^{\prime})\coloneqq\left[b^{\prime}=\llbracket
b{\mid}\alpha,z^{\prime}\rrbracket\right]\cdot\mathcal{P}(b,\alpha,z^{\prime})$
where $z^{\prime}=O(b^{\prime})$.

The belief MDP captures the behaviour of its POMDP. It can be unfolded by
starting in the initial belief and computing all successor beliefs.

##### Deriving FSCs from finite belief MDPs.

Let $T^{\mathcal{B}}\coloneqq\left\\{b\in\mathcal{B}_{\mathcal{M}}\mid
O(b)=z^{T}\right\\}$ denote the set of _target beliefs_. If the reachable
state space of the belief MDP $\mathcal{M}^{\mathcal{B}}$ is finite, e.g.
because the POMDP is acyclic, standard model checking techniques can be
applied to compute the memoryless policy
${\sigma_{\mathcal{B}}}\colon\mathcal{B}_{\mathcal{M}}\rightarrow Act$ that
selects in each belief state ${b\in\mathcal{B}_{\mathcal{M}}}$ the action that
maximises $\mathbb{P}\left[b\models\Diamond
T^{\mathcal{B}}\right]$111Memoryless policies suffice to maximise the value in
a fully observable MDP [26].. We can translate the deterministic, memoryless
policy ${\sigma_{\mathcal{B}}}$ into the corresponding FSC
$F_{\mathcal{B}}=\left(\mathcal{B}_{\mathcal{M}},b_{0},\gamma,\delta\right)$
with action function $\gamma(b,z)={\sigma_{\mathcal{B}}}(b)$ and update
function $\delta(b,z,z^{\prime})=\llbracket
b{\mid}{\sigma_{\mathcal{B}}}(b),z^{\prime}\rrbracket$ for all
$z,z^{\prime}\in Z$.222The assignments of missing combinations where $z\neq
O(b)$ are irrelevant.

##### Handling large and infinite belief MDPs.

In case the reachable state space of the belief MDP
$\mathcal{M}^{\mathcal{B}}$ is infinite or too large for a complete unfolding,
a finite approximation $\overline{\mathcal{M}^{\mathcal{B}}}$ is used instead
[8]. Assuming $\mathcal{M}^{\mathcal{B}}$ is unfolded up to some depth, let
$\mathcal{E}\subset\mathcal{B}_{\mathcal{M}}$ denote the set of explored
beliefs and let
$\mathcal{U}\subset\mathcal{B}_{\mathcal{M}}{\setminus}\mathcal{E}$ denote the
_frontier_ : the set of unexplored beliefs reachable from $\mathcal{E}$ in one
step. To complete the finite abstraction, we require handling of the frontier
beliefs. The idea is to use for each $b\in\mathcal{U}$ a _cut-off value_
$\underline{V}(b)$: an under-approximation of the maximal reachability
probability
$\mathbb{P}^{\mathcal{M}^{\mathcal{B}}}_{\max}\left[b\models\Diamond
T^{\mathcal{B}}\right]$ for $b$ in the belief MDP. We explain how to compute
cut-off values systematically given an FSC in Sec. 4.2.

Ultimately, we define a finite MDP
$\overline{\mathcal{M}^{\mathcal{B}}}=(\mathcal{E}\cup\mathcal{U}\cup\\{b_{\top},b_{\bot}\\},b_{0},Act,\overline{\mathcal{P}^{\mathcal{B}}})$
with the transition function:
$\overline{\mathcal{P}^{\mathcal{B}}}(b,\alpha)\coloneqq\mathcal{P}^{\mathcal{B}}(b,\alpha)$
for explored beliefs $b\in\mathcal{E}$ and all $\alpha\in Act$, and
$\overline{\mathcal{P}^{\mathcal{B}}}(b,\alpha)\coloneqq\\{b_{\top}\mapsto\underline{V}(b),b_{\bot}\mapsto
1-\underline{V}(b)\\}$ for frontier beliefs $b\in\mathcal{U}$ and all
$\alpha\in Act$, where $b_{\top}$ and $b_{\bot}$ are fresh sink states, i.e.
$\overline{\mathcal{P}^{\mathcal{B}}}(b_{\top},\alpha)\coloneqq\\{b_{\top}\mapsto
1\\}$ and
$\overline{\mathcal{P}^{\mathcal{B}}}(b_{\bot},\alpha)\coloneqq\\{b_{\bot}\mapsto
1\\}$ for all $\alpha\in Act$. The reachable state space of
$\overline{\mathcal{M}^{\mathcal{B}}}$ is finite, enabling its automated
analysis; since our method to compute cut-off values emulates an FSC, a policy
maximising
$\mathbb{P}^{\overline{\mathcal{M}^{\mathcal{B}}}}_{\max}\left[\Diamond(T^{\mathcal{B}}\cup\\{b_{\top}\\})\right]$
induces an FSC for the original POMDP $\mathcal{M}$. We discuss how to obtain
this FSC in Sec. 4.3.

###  4.2 Using FSCs for Cut-off Values

A crucial aspect when applying the belief exploration with cut-offs is the
choice of suitable cut-off values. The closer the cut-off value is to the
actual optimum in a belief, the better the approximation we obtain. In
particular, if the cut-off values coincide with the optimal value, cutting off
the initial state is optimal. However, finding optimal values is as hard as
solving the original POMDP. We consider _under-approximative value functions_
induced by applying _any_ 333We remark that [8] considers memoryless FSCs
only. FSC to the POMDP and lifting the results to the belief MDP. The better
the FSC, the better the cut-off value. We generalise belief exploration with
cut-offs such that the approach supports arbitrary sets of FSCs with
additional flexibility.

Let $F_{\mathcal{I}}\in\mathcal{F}^{\mathcal{M}}$ be an arbitrary, but fixed
FSC for POMDP $\mathcal{M}$. Let
$p_{s,n}\coloneqq\mathbb{P}^{\mathcal{M}^{F_{\mathcal{I}}}}\left[(s,n)\models\Diamond
T\right]$ for state $(s,n)\in S\times N$ in the corresponding induced MC. For
fixed $n\in N$, $V(b,n)\coloneqq\sum_{s\in S_{O(b)}}b(s)\cdot p_{s,n}$ denotes
the cut-off value for belief $b$ and memory node $n$. It corresponds to the
probability of reaching a target state in $\mathcal{M}^{F_{\mathcal{I}}}$ when
starting in memory node $n\in N$ and state $s\in S$ according to the
probability distribution $b$. We define the overall cut-off value for $b$
induced by $F$ as $\underline{V}(b)\coloneqq\max_{n\in N}V(b,n)$. It follows
straightforwardly that
$\underline{V}(b)\leq\mathbb{P}^{\mathcal{M}^{\mathcal{B}}}_{\max}\left[b\models\Diamond
T^{\mathcal{B}}\right]$. As values $p_{s,n}$ only need to be computed once,
computing $\underline{V}(b)$ for a given belief $b$ is relatively simple.
However, the complexity of the FSC-based cut-off approach depends on the size
of the induced MC. Therefore, it is essential that the FSCs used to compute
cut-off values are concise.

###  4.3 Extracting FSC from Belief Exploration

Model checking the finite approximation MDP
$\overline{\mathcal{M}^{\mathcal{B}}}$ with cut-off values induced by an FSC
$F_{\mathcal{I}}$ yields a maximising memoryless policy
${\sigma_{\mathcal{B}}}$. Our goal is to represent this policy as an FSC
$F_{\mathcal{B}}$. We construct $F_{\mathcal{B}}$ by considering both
$F_{\mathcal{I}}$ and the necessary memory nodes for each explored belief
$b\in\mathcal{E}$. Concretely, for each explored belief, we introduce a
corresponding memory node. In each such node, the action
${\sigma_{\mathcal{B}}}(b)$ is selected. For the memory update, we distinguish
between two cases based on the next belief after executing
${\sigma_{\mathcal{B}}}(b)$ in $\overline{\mathcal{M}^{\mathcal{B}}}$. If for
observation $z^{\prime}\in Z$, the successor belief $b^{\prime}=\llbracket
b{\mid}{\sigma_{\mathcal{B}}}(b),z^{\prime}\rrbracket\in\mathcal{E}$, the
memory is updated to the corresponding node. Otherwise,
$b^{\prime}\in\mathcal{U}$ holds, i.e., the successor is part of the frontier.
The memory is then updated to the memory node $n$ of FSC $F_{\mathcal{I}}$
that maximises the cut-off value $V(b^{\prime},n)$. This corresponds to the
notion that if the frontier is encountered, we switch from acting according to
policy ${\sigma_{\mathcal{B}}}$ to following $F_{\mathcal{I}}$ (initialised in
the correct memory node). This is formalised as:

######  Definition 5 (Belief-based FSC with cut-offs)

Let $F_{\mathcal{I}}=(N,n_{0},\gamma_{\mathcal{I}},\delta_{\mathcal{I}})$ and
$\overline{\mathcal{M}^{\mathcal{B}}}$ as before. The _belief-based FSC with
cut-offs_ is $F_{\mathcal{B}}=(\mathcal{E}\cup N,b_{0},\gamma,\delta)$ with
action function $\gamma(b,z)={\sigma_{\mathcal{B}}}(b)$ for $b\in\mathcal{E}$
and $\gamma(n,z)=\gamma_{\mathcal{I}}(n,z)$ for $n\in N$ and arbitrary $z\in
Z$. The update function $\delta$ is defined for all $z,z^{\prime}\in Z$ by
$\delta(n,z,z^{\prime})=\delta_{\mathcal{I}}(n,z,z^{\prime})$ if $n\in N$, and
for $b\in\mathcal{E}$ with $b^{\prime}=\llbracket
b{\mid}{\sigma_{\mathcal{B}}}(b),z^{\prime}\rrbracket$ by:

$\delta(b,z,z^{\prime})=b^{\prime}\mbox{ if }b^{\prime}\in\mathcal{E},\mbox{
and }\delta(b,z,z^{\prime})=\mathrm{argmax}_{n\in N}V(b^{\prime},n)\mbox{
otherwise.}$

##  5 Accelerated Inductive Synthesis

In this section, we consider inductive synthesis [5], an approach for finding
controllers for POMDPs in a set of FSCs. We briefly recap the main idea, then
first explain how to use a reference policy. Finally, we introduce and discuss
a novel search space for the controllers that we consider in this paper in
detail.

###  5.1 Inductive Synthesis with $k$-FSCs

In the scope of this paper, inductive synthesis [4] considers a finite family
of FSCs ${\mathcal{F}^{\mathcal{M}}_{k}}$ of $k$-FSCs with memory nodes
$N=\\{n_{0},\dots,n_{k-1}\\}$, and the family
$\mathcal{M}^{{\mathcal{F}^{\mathcal{M}}_{k}}}\coloneqq\\{\mathcal{M}^{F}\mid
F\in{\mathcal{F}^{\mathcal{M}}_{k}}\\}$ of associated induced MCs. The states
for each MC are tuples $(s,n)\in S\times N$. For conciseness, we only discuss
the abstraction-refinement framework [10] within the inductive synthesis loop.
The overall image is as in Fig. 1. Informally, the _MDP abstraction_ of the
family $\mathcal{M}^{{\mathcal{F}^{\mathcal{M}}_{k}}}$ of MCs is an MDP
$\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})$ with the set $S\times N$ of
states such that, if some MC
$M\in\mathcal{M}^{{\mathcal{F}^{\mathcal{M}}_{k}}}$ executes action $\alpha$
in state $(s,n)\in S\times N$, then this action (with the same effect) is also
enabled in state $(s,n)$ of $\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})$.
Essentially, $\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})$ over-
approximates the behaviour of all the MCs in the family
$\mathcal{M}^{{\mathcal{F}^{\mathcal{M}}_{k}}}$: it simulates an arbitrary
family member in every step, but it may switch between steps.444The MDP is an
game-based abstraction [21] of the all-in-one MC [11].

###### Definition 6

_MDP abstraction_ for POMDP $\mathcal{M}$ and family
${\mathcal{F}^{\mathcal{M}}_{k}}=\\{F_{1},\ldots,F_{m}\\}$ of $k$-FSCs is the
MDP $\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})\coloneqq\big{(}S\times
N,(s_{0},n_{0}),\\{1,\ldots,m\\},\mathcal{P}^{\mathcal{F}^{\mathcal{M}}_{k}}\big{)}$
with

$\mathcal{P}^{\mathcal{F}^{\mathcal{M}}_{k}}((s,n),i)=\mathcal{P}^{F_{i}}.$

While this MDP has $m$ actions, practically, many actions coincide. Below, we
see how to utilise the structure of the FSCs. Here, we finish by observing
that the MDP is a proper abstraction:

###### Lemma 1

[10] For all $F\in{\mathcal{F}^{\mathcal{M}}_{k}}$,
$\mathbb{P}^{\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})}_{\min}\left[\Diamond
T\right]\leq\mathbb{P}^{\mathcal{M}^{F}}\left[\Diamond
T\right]\leq\mathbb{P}^{\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})}_{\max}\left[\Diamond
T\right]$.

With that result, we can naturally start with the set of all $k$-FSCs and
search through this family by selecting suitable subsets [10]. Since the
number $k$ of memory nodes necessary is not known in advance, one can
iteratively explore the sequence
$\mathcal{F}^{\mathcal{M}}_{1},\mathcal{F}^{\mathcal{M}}_{2},\dots$ of
families of FSCs of increasing complexity.

###  5.2 Using Reference Policies to Accelerate Inductive Synthesis

Consider the synthesis process of the optimal $k$-FSC
$F\in{\mathcal{F}^{\mathcal{M}}_{k}}$ for POMDP $\mathcal{M}$. To accelerate
the search for $F$ within this family, we consider a reference policy, e.g., a
policy ${\sigma_{\mathcal{B}}}$ extracted from an (approximation of the)
belief MDP, and shrink the FSC family. For each observation $z\in Z$, we
collect the set
$Act[{\sigma_{\mathcal{B}}}](z)\coloneqq\left\\{{\sigma_{\mathcal{B}}}(b)\mid
b\in\mathcal{B}_{\mathcal{M}},O(b)=z\right\\}$ of actions that were selected
by ${\sigma_{\mathcal{B}}}$ in beliefs with observation $z$. The set
$Act[{\sigma_{\mathcal{B}}}](z)$ contains the actions used by the reference
policy when in observation $z$. We focus the search on these actions by
constructing a subset of FSCs $\\{\
(N,n_{0},\gamma,\delta)\in{\mathcal{F}^{\mathcal{M}}_{k}}\mid\forall n\in
N,z\in Z.\gamma(n,z)\in Act[{\sigma_{\mathcal{B}}}](z)\\}$.

Restricting the action selection may exclude the optimal $k$-FSC. It also does
not guarantee that the optimal FSC in the restricted family achieves the same
value as the reference policy ${\sigma_{\mathcal{B}}}$ as
${\sigma_{\mathcal{B}}}$ may have more memory nodes. We first search the
restricted space of FSCs before searching the complete space. This also
accelerates the search: The earlier a good policy is found, the easier it is
to discard other candidates (because they are provably not optimal).
Furthermore, in case the algorithm terminates earlier (notice the anytime
aspect of our problem statement), we are more likely to have found a
reasonable policy.

Additionally, we could use sets $Act[{\sigma_{\mathcal{B}}}]$ to determine
with which $k$ to search. If in some observation $z\in Z$ the belief policy
${\sigma_{\mathcal{B}}}$ uses $|Act[{\sigma_{\mathcal{B}}}](z)|$ distinct
actions, then in order to enable the use of all of these actions, we require
at least $k=\max_{z\in Z}|Act[{\sigma_{\mathcal{B}}}](z)|$ memory states.
However, this may lead to families that are too large and thus we use a more
refined view discussed below.

###  5.3 Inductive Synthesis with Adequate FSCs

In this section, we discuss the set of candidate FSCs in more detail. In
particular, we take a more refined look at the families that we consider.

##### More granular FSCs.

We consider memory models [5] that describe per-observation how much memory
may be used:

######  Definition 7 ($\mu$-FSC)

A _memory model_ for POMDP $\mathcal{M}$ is a function $\mu\colon
Z\rightarrow\mathbb{N}$. Let $k=\max_{z\in Z}\mu(z)$. The $k$-FSC
$F\in{\mathcal{F}^{\mathcal{M}}_{k}}$ with nodes $N=\\{n_{0},\dots,n_{k-1}\\}$
is a _$\mu$ -FSC_ iff for all $z\in Z$ and for all $i>\mu(z)$ it holds:
$\gamma(n_{i},z)=\gamma(n_{0},z)$ and
$\delta(n_{i},z,z^{\prime})=\delta(n_{0},z,z^{\prime})$ for any $z^{\prime}\in
Z$.

${\mathcal{F}^{\mathcal{M}}_{\mu}}$ denotes the family of all $\mu$-FSCs.
Essentially, memory model $\mu$ dictates that for prior observation $z$ only
$\mu(z)$ memory nodes are utilised, while the rest behave exactly as the
default memory node $n_{0}$. Using memory model $\mu$ with $\mu(z)<k$ for some
observations $z\in Z$ greatly reduces the number of candidate controllers. For
example, if $|S_{z}|=1$ for some $z\in Z$, then upon reaching this state, the
history becomes irrelevant. It is thus sufficient to set $\mu(z)=1$ (for the
specifications in this paper). It also significantly reduces the size of the
abstraction, see Appendix A of [3].

(a)

(b)

Figure 3: (a) A POMDP where colours and capital letters encode observations;
unlabelled transitions have probability $1/2$; omitted actions (e.g. action
$\beta$ in the initial state) are self-loops; the objective is to minimise the
expected number of steps to reach state $G$. (b) The optimal posterior-aware
2-FSC.

##### Posterior-aware or posterior-unaware.

The technique outlined in [5] considers _posterior-unaware FSCs_ [2]. An FSC
with update function $\delta$ is posterior-unaware if the posterior
observation is not taken into account when updating the memory node of the
FSC, i.e. $\delta(n,z,z^{\prime})=\delta(n,z,z^{\prime\prime})$ for all $n\in
N,z,z^{\prime},z^{\prime\prime}\in Z$. This restriction reduces the policy
space and thus the MDP abstraction
$\textsf{MDP}({{\mathcal{F}^{\mathcal{M}}_{k}}})$. On the other hand, general
(posterior-aware) FSCs can utilise information about the next observation to
make an informed decision about the next memory node. As a result, fewer
memory nodes are needed to encode complex policies. Consider Fig. 3(a) which
depicts a simple POMDP. First, notice that in yellow states $Y_{i}$ we want to
be able to execute two different actions, implying that we need at least two
memory nodes to distinguish between the two states, and the same is true for
the blue states $B_{i}$. Second, notice that in each state the visible action
always leads to states having different observations, implying that the
posterior observation $z^{\prime}$ is crucial for the optimal decision making.
If $z^{\prime}$ is ignored, it is impossible to optimally update the memory
node. Figure 3(b) depicts the optimal posterior-aware 2-FSC allowing to reach
the target within 12 steps on expectation. The optimal posterior-unaware FSC
has at least 4 memory nodes and the optimal posterior-unaware 2-FSC uses 14
steps.

##### MDP abstraction.

To efficiently and precisely create and analyse MDP abstractions, Def. 6 is
overly simplified. In Appendix A of [3], we present the construction for
general, posterior-aware FSCs including memory models.

##  6 Integrating Belief Exploration with Inductive Synthesis

We clarify the symbiotic approach from Fig. 1 and review FSC sizes.

####  6.0.1 Symbiosis by closing the loop

Section 4 shows the potential to improve belief exploration using FSCs, e.g.,
obtained from an inductive synthesis loop, whereas Sec. 5 shows the potential
to improve inductive synthesis using policies from, e.g., belief exploration.
A natural next step is to use improved inductive synthesis for belief
exploration and improved belief exploration for inductive synthesis, i.e., to
alternate between both techniques. This section briefly clarifies the
symbiotic approach from Fig. 1 using Alg. 1.

Input : POMDP $\mathcal{M}$, set $T$ of target states, timeout values
$t,t_{\mathcal{I}},t_{\mathcal{B}}$

Output : Best FSCs $F_{\mathcal{I}}$ and $F_{\mathcal{B}}$ found so far

1

2$F_{\mathcal{I}}\leftarrow\bot$,
$\mathcal{F}\leftarrow\mathcal{F}_{1}^{\mathcal{M}}$, $k\leftarrow 0$,
$\mu\leftarrow\\{z\mapsto 1\mid z\in Z\\}$, $F_{\mathcal{B}}\leftarrow\bot$,
${\sigma_{\mathcal{B}}}\leftarrow\bot$

3 while  _not timeout $t$_ do

4 while  _not timeout $t_{\mathcal{I}}$_ do

5 if  _$\mathcal{F}=\emptyset$_ then

6 $k\leftarrow k+1$

7 $\forall z\in Z\colon\mu(z)\leftarrow\max\\{\mu(z),k\\}$

8 $\mathcal{F}\leftarrow{\mathcal{F}^{\mathcal{M}}_{\mu}}$

9

10
$\mathcal{F},F_{\mathcal{I}}\leftarrow\texttt{{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}search}}(\mathcal{F},F_{\mathcal{I}},Act[{\sigma_{\mathcal{B}}}]\textbf{
if
}\mathbb{P}^{\mathcal{M}^{F_{\mathcal{I}}}}\\!\left[\Diamond{T}\right]>\mathbb{P}^{\mathcal{M}^{F_{\mathcal{B}}}}\\!\left[\Diamond{T}\right]\textbf{
else }\bot)$

11

12
${\sigma_{\mathcal{B}}},F_{\mathcal{B}}\leftarrow\texttt{{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}explore}}(t_{\mathcal{B}},F_{\mathcal{I}})$

13 if
_$\mathbb{P}^{\mathcal{M}^{F_{\mathcal{I}}}}\\!\left[\Diamond{T}\right]\leq\mathbb{P}^{\mathcal{M}^{F_{\mathcal{B}}}}\\!\left[\Diamond{T}\right]$
and  $\exists z\in Z\colon\mu(z)<|Act[{\sigma_{\mathcal{B}}}](z)|$_ then

14 $\forall z\in Z\colon\mu(z)\leftarrow|Act[{\sigma_{\mathcal{B}}}](z)|$

15 $\mathcal{F}\leftarrow{\mathcal{F}^{\mathcal{M}}_{\mu}}$

16

17 yield _$F_{\mathcal{I}},F_{\mathcal{B}}$_

Algorithm 1 Anytime algorithm

We iterate until a global timeout $t$: in each iteration, we make both
controllers available to the user as soon as they are computed (Alg. 1, l.
13). We start in the inductive mode (l. 3-8), where we initially consider the
$1$-FSCs represented in ${\mathcal{F}^{\mathcal{M}}_{\mu}}$. Method search (l.
8) investigates $\mathcal{F}$ and outputs the new maximising FSC
$F_{\mathcal{I}}$ (if it exists). If the timeout $t_{\mathcal{I}}$ interrupts
the synthesis process, the method additionally returns yet unexplored
parameter assignments. If $\mathcal{F}$ is fully explored within the timeout
$t_{\mathcal{I}}$ (l. 4), we increase $k$ and repeat the process. After the
timeout $t_{\mathcal{I}}$, we run belief exploration explore for
$t_{\mathcal{B}}$ seconds, where we use $F_{\mathcal{I}}$ as backup
controllers (l. 9). After the timeout $t_{\mathcal{B}}$ (exploration will
continue from a stored configuration in the next belief phase), we use
$F_{\mathcal{I}}$ to obtain cut-off values at unexplored states, compute the
optimal policy $\sigma^{\mathcal{M}^{\mathcal{B}}}$ (see Sec. 4) and extract
the FSC $F_{\mathcal{B}}$ which incorporates $F_{\mathcal{I}}$. Before we
continue the search, we check whether the belief-based FSC is better and
whether that FSC gives any reason to update the memory model (l. 10). If so,
we update $\mu$ and reset the $\mathcal{F}$ (l. 11-12).

####  6.0.2 The size of an FSC

We have considered several sub-classes of FSCs and wish to compare the sizes
of these controllers. For FSC $F=(N,n_{0},\gamma,\delta)$, we define its size
$size(F)\coloneqq size(\gamma)+size(\delta)$ as the memory required to encode
functions $\gamma$ and $\delta$. Encoding $\gamma\colon N\times Z\rightarrow
Act$ of a general $k$-FSC requires $size(\gamma)=\sum_{n\in N}\sum_{z\in
Z}1=k\cdot|Z|$ memory. Encoding $\delta\colon N\times Z\times Z\rightarrow N$
requires $k\cdot|Z|^{2}$ memory. However, it is uncommon that in each state-
memory pair $(s,n)$ all posterior observations can be observed. We therefore
encode $\delta(n,z,\cdot)$ as a sparse adjacency list, i.e., as a list of
pairs $(z^{\prime},\delta(n,z,z^{\prime}))$. To define the size of such a list
properly, consider the induced MC $\mathcal{M}^{F}=(S\times
N,(s_{0},n_{0}),\\{\alpha\\},\mathcal{P}^{F})$. Let
$post(n,z)\coloneqq\left\\{O(s^{\prime})\mid\exists s\in
S_{z}\colon(s^{\prime},\cdot)\in\mathrm{supp}(\mathcal{P}^{F}((s,n),\alpha))\right\\}$
denote the set of posterior observations reachable when taking a transition in
a state $(s,n)$ of $\mathcal{M}^{F}$ with $O(s)=z$. Table 1 summarises the
resulting sizes of FSCs of various sub-classes. The derivation is included in
Appendix B of [3]. Table 4 on p. 4 shows that we typically find much smaller
$\mu$-FSCs ($F_{\mathcal{I}}$) than belief-based FSCs ($F_{\mathcal{B}}$).

FSC class | $size(\gamma)$ | $size(\delta)$
---|---|---
$k$-FSC | $k\cdot|Z|$ | $2\cdot\sum_{n\in N}\sum_{z\in Z}|post(n,z)|$
$\mu$-FSC | $\sum_{z\in Z}\mu(z)$ | $2\cdot\sum_{z\in Z}\sum_{i=0}^{\mu(z)-1}|post(n_{i},z)|$
posterior-unaware $\mu$-FSC | $\sum_{z\in Z}\mu(z)$ | $\sum_{z\in Z}\mu(z)$
$F_{\mathcal{B}}$ using $F_{\mathcal{I}}$ for cut-offs | $size(\gamma_{\mathcal{I}})+|\mathcal{E}|$ | $size(\delta_{\mathcal{I}})+2\cdot\sum_{b\in\mathcal{E}}|post(b,O(b))|$
Table 1: Sizes of different types of FSCs.

##  7 Experiments

Our evaluation focuses on the following three questions:

  * Q1:

_Do the FSCs from inductive synthesis raise the accuracy of the belief MDP?_

  * Q2:

_Does exploiting the belief MDP boost the inductive synthesis of FSCs?_

  * Q3:

_Is the symbiotic approach improving run time, controller’s value and size?_

####  7.0.1 Selected benchmarks and setup

Our baseline are the recent belief exploration technique [8] implemented in
Storm [13] and the inductive (policy) synthesis method [5] implemented in
Paynt [6]. Paynt uses Storm for parsing and model checking of MDPs, but not
for solving POMDPs. Our symbiotic framework (Alg. 1) has been implemented on
top of Paynt and Storm. In the following, we use Storm and Paynt to refer to
the implementation of belief exploration and inductive synthesis respectively,
and Saynt to refer to the symbiotic framework. The implementation of Saynt and
all benchmarks are publicly available555 https://github.com/randriu/synthesis.
Additionally, the implementation and the benchmarks in the form of an artifact
are also available at https://doi.org/10.5281/zenodo.7874513.

##### Setup.

The experiments are run on a single core of a machine equipped with an Intel
i5-12600KF @4.9GHz CPU and 64GB of RAM. Paynt searches for posterior-unaware
FSCs using abstraction-refinement, as suggested by [5]. By default, Storm
applies the cut-offs as presented in Sect. 4.1. Saynt uses the default
settings for Paynt and Storm while $t_{\mathcal{I}}=60s$ and
$t_{\mathcal{B}}=10s$ were taken for Alg. 1. Under Q3, we discuss the effect
of changing these values.

##### Benchmarks.

We evaluate the methods on a selection of models from [7, 8, 5] supplemented
by larger variants of these models (Drone-8-2 and Refuel-20), by one model
from [16] (Milos-97) and by the synthetic model (Lanes+) described in Appendix
C of [3]. We excluded benchmarks for which Paynt or Storm finds the (expected)
optimal solution in a matter of seconds. The benchmarks were selected to
illustrate advantages as well as drawbacks of all three synthesis approaches:
belief exploration, inductive (policy) search, and the symbiotic technique.
Table 2 lists for each POMDP the number $|S|$ of states, the total number
$\sum Act\coloneqq\sum_{s}|Act(s)|$ of actions, the number $|Z|$ of
observations, the specification (either maximising or minimising a
reachability probability $P$ or expected reward $R$), and a known over-
approximation on the optimal value computed using the technique from [7].
These over-approximations are solely used as rough estimates of the optimal
values. Tab. 5 on p. 5 reports the quality of the resulting FSCs on a broader
range of benchmarks and demonstrates the impact of the non-default settings.

Model | $|S|$ | ${\sum}Act$ | $|Z|$ | Spec. | Over- | Model | $|S|$ | ${\sum}Act$ | $|Z|$ | Spec. | Over-
---|---|---|---|---|---|---|---|---|---|---|---
approx. | approx.
4x3-95 | 22 | 82 | 9 | $R_{\max}$ | $\leq 2.24$ | Drone-4-2 | 1226 | 2954 | 761 | $P_{\max}$ | $\leq 0.98$
4x5x2-95 | 79 | 310 | 7 | $R_{\max}$ | $\leq 3.26$ | Drone-8-2 | 13k | 32k | 3195 | $P_{\max}$ | $\leq 0.99$
Hallway | 61 | 301 | 23 | $R_{\min}$ | $\geq 11.5$ | Lanes+ | 2741 | 5285 | 11 | $R_{\min}$ | $\geq 4805$
Milos-97 | 165 | 980 | 11 | $R_{\max}$ | $\leq 80$ | Netw-3-8-20 | 17k | 30k | 2205 | $R_{\min}$ | $\geq 4.31$
Network | 19 | 70 | 5 | $R_{\max}$ | $\leq 359$ | Refuel-06 | 208 | 565 | 50 | $P_{\max}$ | $\leq 0.78$
Query-s3 | 108 | 320 | 6 | $R_{\max}$ | $\leq 600$ | Refuel-20 | 6834 | 25k | 174 | $P_{\max}$ | $\leq 0.99$
Tiger-95 | 14 | 50 | 7 | $R_{\max}$ | $\leq 159$ | Rocks-12 | 6553 | 32k | 1645 | $R_{\min}$ | $\geq 17.8$

Table 2: Information about the benchmark POMDPs.

### Q1: FSCs provide better approximations of the belief MDP

In these experiments, Paynt is used to obtain a sub-optimal $F_{\mathcal{I}}$
within 10s which is then used by Storm. Tab. 3 (left) lists the results. Our
main finding is that _belief exploration can yield better FSCs (and sometimes
faster) using FSCs from Paynt_—even if the latter FSCs are far from optimal.
For instance, Storm with provided $F_{\mathcal{I}}$ finds an FSC with value
0.97 for the Drone-4-2 benchmark within a total of 10s (1s+9s for obtaining
$F_{\mathcal{I}}$), compared to obtaining an FSC of value 0.95 in 56s on its
own. A value improvement is also obtained if Storm runs longer. For the
Network model, the value improves with 37% (short-term) and 47% (long-term)
respectively, at the expense of investing 3s to find $F_{\mathcal{I}}$. For
the other models, the relative improvement ranges from 3% to 25%. A further
value improvement can be achieved when using better FSCs $F_{\mathcal{I}}$
from Paynt; see Q3. Sometimes, belief exploration does not profit from
$F_{\mathcal{I}}$. For Hallway, the unexplored part of the belief MDP becomes
insignificant rather quickly, and so does the impact of $F_{\mathcal{I}}$.
Clipping [8], a computationally expensive extension of cut-offs, is beneficial
only for Rocks-12, rendering $F_{\mathcal{I}}$ useless. Though even in this
case, using $F_{\mathcal{I}}$ significantly improves Short Storm that did not
have enough time to apply clipping.

| Paynt | Short Storm | Long Storm
---|---|---|---
Model | $F_{\mathcal{I}}$ |  | \+ $F_{\mathcal{I}}$ |  | +$F_{\mathcal{I}}$
Drone-4-2 | $0.94$ | $0.92$ | ${0.97}$ | $0.95$ | $0.97$
$P_{\mathrm{max}}$ | $9s$ | $1s$ | $1s$ | $56s$ | $57s$
Network | $266.1$ | $186.7$ | $274.5$ | $202.1$ | ${277.1}$
$R_{\mathrm{max}}$ | $3s$ | ${<}1s$ | ${<}1s$ | $26s$ | $33s$
Drone-8-2 | $0.9$ | $0.6$ | ${0.96}$ | $0.68$ | $0.97$
$P_{\mathrm{max}}$ | $28s$ | $3s$ | $3s$ | $101s$ | $103s$
4x3-95 | $1.66$ | $1.62$ | $1.82$ | $1.84$ | ${1.88}$
$R_{\mathrm{max}}$ | $7s$ | ${<}1s$ | ${<}1s$ | $60s$ | $72s$
Query-s3 | $425.2$ | $417.4$ | $430.0$ | $419.6$ | ${432.0}$
$R_{\mathrm{max}}$ | $7s$ | $2s$ | $2s$ | $91s$ | $94s$
Milos-97 | $31.56$ | $37.15$ | $39.15$ | $38.35$ | ${40.64}$
$R_{\mathrm{max}}$ | $3s$ | ${<}1s$ | ${<}1s$ | $42s$ | $42s$
Hallway | $16.05$ | $13.07$ | $12.63$ | $12.55$ | $12.55$
$R_{\mathrm{min}}$ | $9s$ | $1s$ | $1s$ | $160s$ | $167s$
Rocks-12 | $42$ | $38$ | $31.89$ |  $20$* |  $20$*
$R_{\mathrm{min}}$ | ${<}1s$ | ${<}1s$ | ${<}1s$ | $10s$ | $10s$

| Storm | Paynt
---|---|---
Model | $F_{\mathcal{B}}$ |  | \+ $F_{\mathcal{B}}$
4x5x2-95 | $2.08$ | $0.94$ | ${2.03}$
$R_{\mathrm{max}}$ | ${<}1s$ | $258s$ | $38s$
Refuel-20 | $0.09$ | ${<}0.01$ | $0.19$
$P_{\mathrm{max}}$ | $1s$ | $10s$ | $11s$
Tiger-95 | $50.38$ | $2.99$ | ${28.73}$
$R_{\mathrm{max}}$ | ${<}1s$ | $14s$ | $23s$
4x3-95 | $1.62$ | $1.75$ | ${1.84}$
$R_{\mathrm{max}}$ | ${<}1s$ | $14s$ | $238s$
Refuel-06 | $0.67$ | $0.35$ | ${0.67}$
$P_{\mathrm{max}}$ | ${<}1s$ | ${<}1s$ | $42s$
Milos-97 | $37.15$ | $31.56$ | ${39.29}$
$R_{\mathrm{max}}$ | ${<}1s$ | $3s$ | $215s$
Netw-3-8-20 | $11.93$ | $11.07$ | ${10.95}$
$R_{\mathrm{min}}$ | $1s$ | $185s$ | $271s$
Rocks-12 | $38$ | $42$ | ${38}$
$R_{\mathrm{min}}$ | ${<}1s$ | ${<}1s$ | ${<}1s$

Table 3:  Left (Q1): Experimental results on how a (quite sub-optimal) FSC
$F_{\mathcal{I}}$ computed by Paynt within 10s impacts Storm. (For Drone-8-2,
the largest model in our benchmark, we use 30s). The “Paynt” column indicates
the value of $F_{\mathcal{I}}$ and its run time. The “Short Storm” column runs
storm for 1s and compares the value of FSC $F_{\mathcal{B}}$ found by Storm
alone to Storm using $F_{\mathcal{I}}$. The “Long Storm” column is analogous,
but with a 300s timeout for Storm. In the last row, * indicates that clipping
was used. Right (Q2): Experimental results on how an FSC $F_{\mathcal{B}}$
obtained by a shallow exploration of the belief MDP impacts the inductive
synthesis by Paynt. The “Storm” column reports the value of $F_{\mathcal{B}}$
computed within 1s. The “Paynt” column compares the values of the FSCs
$F_{\mathcal{I}}$ obtained by Paynt itself to Paynt using the FSCs
$F_{\mathcal{B}}$ within a 300s timeout.

### Q2: Belief-based FSCs improve inductive synthesis

In this experiment, we run Storm for at most 1s, and use the result in Paynt.
Tab. 3 (right) lists the results. Our main finding is that _inductive
synthesis can find much better FSCs—and sometimes much faster—when using FSCs
from belief exploration._ For instance, for the 4x5x2 benchmark, an FSC is
obtained about six times faster while improving the value by 116%. On some
larger models, Paynt alone struggles to find any good $F_{\mathcal{I}}$ and
using $F_{\mathcal{B}}$ boosts this; e.g., the value for the Refuel-20 model
is raised by a factor 20 at almost no run time penalty. For the Tiger
benchmark, a value improvement of 860% is achieved (albeit not as good as
$F_{\mathcal{B}}$ itself) at the expense of doubling the run time. Thus: _even
a shallow exploration of the belief MDP pays off in the inductive synthesis_.
The inductive search typically profits even more when exploring the belief MDP
further. This is demonstrated, e.g., in the Rocks-12 model: using the FSC
$F_{\mathcal{B}}$ computed using clipping (see Table 3 (left)) enables Paynt
to find FSC $F_{\mathcal{I}}$ with the same (optimal) value 20 as
$F_{\mathcal{B}}$ within 1s. Similarly, for the Milos-97 model, running Storm
for 45s (producing a more precise $F_{\mathcal{B}}$) enables Paynt to find an
FSC $F_{\mathcal{I}}$ achieving a better value than controllers found by Storm
or Paynt alone within the timeout. (These results are not reported in the
tables.) However, as opposed to Q1, where a better FSC $F_{\mathcal{I}}$
naturally improves the belief MDP, longer exploring the belief MDP does not
always yield a better $F_{\mathcal{I}}$: a larger
$\overline{\mathcal{M}^{\mathcal{B}}}$ with a better $F_{\mathcal{B}}$ may
yield a larger memory model $\mu$, thus inducing a significantly larger family
where Paynt struggles to identify good FSCs.

### Q3: The practical benefits of the symbiotic approach

The goals of these experiments are to investigate whether the symbiotic
approach improves the run time (can FSCs of a certain value be obtained
faster?), the memory footprint (how is the total memory consumption
affected?), the controller’s value (can better FSCs be obtained with the same
computational resources?) and the controller’s size (are more compact FSCs
obtained?).

##### Value of the synthesised FSCs.

Figure 4 plots the value of the FSCs produced by Storm, Paynt, and Saynt
versus the computation time. Note that for maximal objectives, the aim is to
obtain a high value (the first 4 plots) whereas for minimal objectives a lower
value prevails. From the plots, it follows that _the FSCs from the symbiotic
approach are superior in value to the ones obtained by the standalone
approaches._ The relative improvement of the value of the resulting FSCs
differs across individual models, similar to the trends in Q1 and Q2. When
comparing the best FSC found by Storm or Paynt alone with the best FSC found
by Saynt, the improvement ranges from negligible (4x3-95) to around 3%-7%
(Netw-3-8-20, Milos-97, Query-s3) and sometimes goes over 40% (Refuel-20,
Lines+). We note that the distance to the (unknown) optimal values remains
unclear. The FSC value never decreases but sometimes does also not increase,
as indicated by Hallway and Rocks-12 (see also Q2). Our experiments (see Tab.
5) also indicate that the improvement over the baseline algorithms is
typically more significant in the larger variants of the models. Furthermore,
the plots in Fig. 4 also include the FSC value by the one-shot combination of
Storm and Paynt. We see that _Saynt can improve the FSC value over the one-
shot combination._ This is illustrated in, e.g., the 4x3-95 and Lanes+
benchmarks, see the 1st and 3rd plots in Fig. 4 (left).

$1.7$$1.74$$1.78$$1.82$$1.86$$1.9$Value [Rmax]4x3-95
$\bullet$Saynt$F_{\mathcal{B}}$Saynt$F_{\mathcal{I}}$StormPayntQ1 StormQ2
Paynt$31$$33$$35$$37$$39$$41$$43$Value [Rmax]Milos-97
$\diamond$$0$$0.05$$0.1$$0.15$$0.2$$0.25$Value
[Pmax]Refuel-20$415$$435$$455$$475$$495$$515$Value [Rmax]Query-s3
$\diamond$$0.4$$0.8$$1.2$$1.6$$2$$\cdot 10^{4}$Value
[Rmin]Lanes+$12$$13$$14$$15$$16$$17$Value
[Rmin]Hallway$0$$2$$4$$6$$8$$10$$12$$14$$10$$10.4$$10.8$$11.2$$11.6$$12$Time
[min]Value [Rmin]Network-3-8-20$0$$2$$4$$6$$8$$10$$12$$14$$8$$16$$32$$64$Time
[min]Memory usage [GB]Avg. memory usage comparisonSayntStorm Figure 4: Value
of the generated FSCs over time. The last graph shows the average memory usage
of Storm and Saynt. The lines ending before the timeout indicate that the 64GB
memory limit was hit. $\bullet$ indicates that Paynt and Saynt synthesised
posterior-aware FSCs. $\diamond$ indicates that Saynt ran with
$t_{\mathcal{I}}=$90s.

##### Total synthesis time.

Saynt initially needs some time for the first iteration (one inductive and one
belief phase) in Alg. 1 and thus during the beginning of the synthesis
process, the standalone tools may provide FSCs of a certain value faster.
_After the first iteration, however, Saynt typically provides better FSCs in a
shorter time._ For instance, for the Refuel-20 benchmark Saynt swiftly
overtakes Storm after the first iteration. The only exception is Rocks-12
(discussed before), where Saynt with the default settings needs significantly
more time than Storm to obtain an FSC of the same value.

##### Memory footprint.

Belief exploration typically has a large memory footprint: Storm quickly hits
the 64GB memory limit on exploring the belief MDP. _Saynt reduces the memory
footprint of Storm alone by a factor 3 to 4_, see the bottom right plot of
Fig. 4. The average memory footprint of running Paynt standalone quickly
stabilises around 700MB. The memory footprint of Saynt is thus dominated by
the restricted exploration of the belief MDP.

Models: | Lanes+ | Hallway | Netw-3-8-20 | Query-s3$\diamond$ | Refuel-06 | Drone-8-2 | Refuel-20
---|---|---|---|---|---|---|---
$F_{\mathcal{B}}$ | 4805/8.1k | 12.55/2k | 10/40k | 511.32/7.7k | 0.67/84 | 0.96/237k | 0.24/1.5k
$F_{\mathcal{I}}$ | 6591/34 | 15.46/86 | 11.04/4.8k | 509.49/26 | 0.67/156 | 0.90/6.4k | 0.2/362
Table 4: Trade-offs between the value and size in the resulting FSCs
$F_{\mathcal{I}}$ and $F_{\mathcal{B}}$ found by Saynt. Each cell reports
value/size. The first three models have a minimising objective. $\diamond$
indicates that Saynt ran with $t_{\mathcal{I}}=$90s.

##### The size of the synthesised FSCs.

For selected models, Tab. 4 shows the trade-offs between the value and size of
the resulting FSCs $F_{\mathcal{I}}$ and $F_{\mathcal{B}}$ found by Saynt. The
experiments show that _the FSCs $F_{\mathcal{I}}$ provided by inductive
synthesis are typically about one to two orders of magnitude smaller than the
belief-based FSCs $F_{\mathcal{B}}$ with only a small penalty in their
values_. There are models (e.g. Refuel-06) where a very small
$F_{\mathcal{B}}$, having even slightly smaller size than $F_{\mathcal{I}}$,
does exist. The integration mostly reduces the size of $F_{\mathcal{B}}$ due
to the better approximation of the belief MDP by up to a factor of two. This
reduction has a negligible effect on the size of $F_{\mathcal{I}}$. This
observation further strengthens the usefulness of Saynt that jointly improves
the value of $F_{\mathcal{I}}$ and $F_{\mathcal{B}}$. Hence, Saynt gives users
a unique opportunity to run a single, time-efficient synthesis and select the
FSC according to the trade-off between its value and size.

##### Customising the Saynt setup.

In contrast to the standalone approaches as well as to the one-way
integrations presented in Q1 and Q2, _Saynt provides a single synthesis method
that is efficient for a general class of models without tuning its
parameters_. Naturally, adjusting the parameters to individual benchmarks can
further improve the quality of the computed controllers: captions of Fig. 4
and Tab. 4 describe which non-default settings were used for selected models.

### Additional results

In Tab. 5, we compare values and sizes of FSCs synthesised by the particular
methods on a broader range of benchmarks. We can see that FSCs
$F_{\mathcal{I}}$ obtained by Saynt achieve better values than the controllers
computed by Paynt; size-wise, these better FSCs of Saynt are similar or only
slightly bigger. Meanwhile, for FSCs $F_{\mathcal{B}}$ obtained by Saynt, we
sometimes observe a significant size reduction while still improving the value
compared to the FSCs produced by Storm. Two models are notable: On Drone-8-2,
Saynt obtains 50% smaller $F_{\mathcal{B}}$ while having a 41% better value.
On Network-3-8-20, the size of $F_{\mathcal{B}}$ is reduced by 40% while again
providing better value.

In the following, we further discuss the impact of non-default settings for
selected benchmarks, as presented in Tab. 5. For instance, using posterior-
aware FSCs generally significantly slows down the synthesis process, however,
for Network and 4x3-95, it helps improve the value of the default posterior-
unaware FSCs by 2% and 4%, respectively. For the former model, a better
$F_{\mathcal{I}}$ also improves $F_{\mathcal{B}}$ by about a similar value. In
some cases, e.g. for Query-s3, it is beneficial to increase the parameter
$t_{\mathcal{I}}$, giving Paynt enough time to search for a good FSC
$F_{\mathcal{I}}$ (the relative improvement is 6%), which also improves the
value of the resulting FSC $F_{\mathcal{B}}$ by about a similar value. Tuning
$t_{\mathcal{I}}$ and $t_{\mathcal{B}}$ can also have an impact on the value-
size trade-off, as seen in the Milos-97 model, where setting longer timeout
$t_{\mathcal{I}}$ results in finding a 2% better $F_{\mathcal{B}}$ with 130%
size increase. A detailed analysis of the experimental results suggests that
usually, it is more beneficial to invest time into searching for good
$F_{\mathcal{I}}$ that is used to compute better cut-off values, rather than
into deeper exploration of belief MDP. However, the timeouts still need to
allow for multiple subsequent iterations of the algorithm in order to utilise
the full potential of the symbiosis.

##  8 Conclusion and Future Work

We proposed Saynt, a symbiotic integration of the two main approaches for
controller synthesis in POMDPs. Using a wide class of models, we demonstrated
that Saynt substantially improves the value of the resulting controllers and
provides an any-time, push-button synthesis algorithm allowing users to select
the controller based on the trade-off between its value and size, and the
synthesis time.

In future work, we plan to explore if the inductive policy synthesis can also
be successfully combined with point-based approximation methods, such as
SARSOP, and on discounted reward properties. A preliminary comparison on
discounting properties provides two interesting observations: 1) For models
with large reachable belief space and discount factors (very) close to one,
SARSOP typically fails to update its initial _alpha-vectors_ and thus produces
low-quality controllers. In these cases, SAYNT outperforms SARSOP. 2) For
common discount factors, SARSOP beats SAYNT on the majority of benchmarks.
This is not surprising, as the MDP engine underlying SAYNT does not natively
support discounting and instead computes a much harder fixed point. See [15],
for a recent discussion on the differences between discounting and not
discounting.

Benchmark Model Size Paynt Storm Saynt Model Spec. $S$/$\Sigma Act$ $Z$
$F_{\mathcal{I}}$ Size $F_{\mathcal{B}}$ Size $F_{\mathcal{B}}$ Size
$F_{\mathcal{I}}$ Size $R_{\mathrm{max}}$ $9$ 36 999 $\mathbf{1.89}\bullet$
968 $1.87\bullet$ 126 4x3 $22$ $1.81$ $1.87$ $283s$ $120s$ 95 $82$ $764s$
$414s$ $\mathbf{1.89}$ 869 $1.79$ 36 $303s$ $678s$ 4x5x2 $R_{\mathrm{max}}$
$79$ $7$ $0.94$ 26 $2.08$ 102 $2.08$ 102 $2.03$ 38 95 $310$ $305s$ $3s$ $71s$
$378s$ $P_{\mathrm{max}}$ $384$ 768 170k $\mathbf{0.89}\bullet$ 169k
$0.87\bullet$ 2.5k Drone $1226$ $0.87$ $0.84$ $390s$ $453s$ 4-1 $3026$ $665s$
$110s$ $\mathbf{0.89}$ 176k $0.79$ 922 $180s$ $45s$ Drone $P_{\mathrm{max}}$
$1226$ $761$ $0.95$ 1.5k $0.95$ 135k $\mathbf{0.97}$ 140k $0.94$ 1.5k 4-2
$3026$ $900s$ $110s$ $194s$ $1s$ Drone $P_{\mathrm{max}}$ $13$k $3195$ $0.9$
6.4k $0.68$ 280k $\mathbf{0.96}$ 140k $0.9$ 6.4k 8-2 $32$k $260s$ $98s$ $247s$
$30s$ Hallway $R_{\mathrm{min}}$ $61$ $23$ $15.54$ 66 $12.55$ 1.9k $12.55$
1.8k $15.46$ 86 $301$ $26s$ $916s$ $263s$ $293s$ Lanes+ $R_{\mathrm{min}}$
$2741$ $11$ $8223$ 42 $18870$ 8.1k $\mathbf{4805}$ 8.1k $6591$ 34 $5289$
$118s$ $376s$ $173s$ $114s$ Milos-97 $R_{\mathrm{max}}$ $11$ 40 823
$\mathbf{41.99}\diamond$ 692 $35.82\diamond$ 40 $165$ $31.56$ $39.03$ $370s$
$185s$ $980$ $4s$ $88s$ $\mathbf{41.55}$ 290 $35.41$ 40 $270s$ $114s$ Network
$R_{\mathrm{max}}$ $5$ 22 2.4k $\mathbf{289.18}\bullet$ 2k $287.23\bullet$ 54
$19$ $280.33$ $209.71$ $395s$ $106s$ $70$ $38s$ $110s$ $\mathbf{284.51}$ 1.8k
$280.33$ 22 $85s$ $41s$ Netw $R_{\mathrm{min}}$ $4589$ $1173$ $4.24$ 2.3k
$3.21$ 34k $\mathbf{3.2}$ 23k $4.19$ 2.5k 2-8-20 $6973$ $914s$ $11s$ $71s$
$211s$ Netw $R_{\mathrm{min}}$ $17$k $2205$ $11.04$ 4.4k $10.27$ 64k
$\mathbf{10}$ 38k $11.04$ 4.8k 3-8-20 $30$k $638s$ $238s$ $742s$ $379s$
$R_{\mathrm{max}}$ $6$ 28 12.9k $\mathbf{511.32}\diamond$ 7.7k
$509.49\diamond$ 26 Query $108$ $502.3$ $420.11$ $566s$ $362s$ s3 $320$ $931s$
$184s$ $482.21$ 7.7k $478.59$ 28 $700s$ $610s$ Refuel $P_{\mathrm{max}}$ $208$
$50$ $0.35$ 100 $0.67$ 343 $0.67$ 84 $0.67$ 156 06 $565$ ${<}1s$ $182s$ $178s$
$84s$ Refuel $P_{\mathrm{max}}$ $470$ $66$ $0.32$ 132 $0.44$ 534
$\mathbf{0.45}$ 140 $0.3$ 142 08 $1431$ $253s$ $96s$ $186s$ $84s$ Refuel
$P_{\mathrm{max}}$ $6834$ $174$ $0.02$ 348 $0.15$ 1.2k $\mathbf{0.24}$ 1.5k
$0.2$ 360 20 $24$k $922s$ $468s$ $386s$ $173s$ Rocks $R_{\mathrm{min}}$ $6553$
$1645$ $42$ 3.3k $\mathbf{20}*$ 115 $20*$ 115 $20*$ 3.3k 12 $32$k ${<}1s$
$15s$ $235s$ $236s$ Tiger $R_{\mathrm{max}}$ $14$ $7$ $7.93$ 34 $50.38$ 58
$50.38$ 58 $31.61$ 48 95 $50$ $547s$ ${<}1s$ $71s$ $513s$

Table 5: The quality and size of resulting FSCs provided by Paynt, Storm, and
Saynt within the 15-minute timeout. The run times indicate the time needed to
find the best FSC. Non-default settings: $*$ marks experiments where clipping
was enabled, $\bullet$ marks experiments where PAYNT synthesised posterior-
aware FSCs, $\diamond$ marks experiments where integration parameter
$t_{\mathcal{I}}$ was set to 90 seconds.

## References

  * [1] Amato, C., Bernstein, D.S., Zilberstein, S.: Optimizing fixed-size stochastic controllers for POMDPs and decentralized POMDPs. Autonomous Agents and Multi-Agent Systems 21(3), 293–320 (2010)
  * [2] Amato, C., Bonet, B., Zilberstein, S.: Finite-state controllers based on Mealy machines for centralized and decentralized POMDPs. In: AAAI. pp. 1052–1058. AAAI Press (2010)
  * [3] Andriushchenko, R., Bork, A., Češka, M., Junges, S., Katoen, J.P., Macák, F.: Search and Explore: Symbiotic policy synthesis in POMDPs. arXiv preprint arXiv:2305.14149 (2023)
  * [4] Andriushchenko, R., Češka, M., Junges, S., Katoen, J.P.: Inductive synthesis for probabilistic programs reaches new horizons. In: TACAS. LNCS, vol. 12651, pp. 191–209. Springer (2021)
  * [5] Andriushchenko, R., Češka, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for POMDPs. In: UAI. vol. 180, pp. 85–95. PMRL (2022)
  * [6] Andriushchenko, R., Češka, M., Junges, S., Katoen, J.P., Stupinský, Š.: PAYNT: a tool for inductive synthesis of probabilistic programs. In: CAV. LNCS, vol. 12759, pp. 856–869. Springer (2021)
  * [7] Bork, A., Junges, S., Katoen, J.P., Quatmann, T.: Verification of indefinite-horizon POMDPs. In: ATVA. LNCS, vol. 12302, pp. 288–304. Springer (2020)
  * [8] Bork, A., Katoen, J.P., Quatmann, T.: Under-approximating expected total rewards in POMDPs. In: TACAS (2). LNCS, vol. 13244, pp. 22–40. Springer (2022)
  * [9] Carr, S., Jansen, N., Topcu, U.: Task-aware verifiable rnn-based policies for partially observable markov decision processes. J. Artif. Intell. Res. 72, 819–847 (2021)
  * [10] Češka, M., Jansen, N., Junges, S., Katoen, J.P.: Shepherding hordes of Markov chains. In: TACAS. LNCS, vol. 11428, pp. 172–190. Springer (2019)
  * [11] Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: Profeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30(1), 45–75 (2018)
  * [12] Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suilen, M., Topcu, U.: Robust finite-state controllers for uncertain POMDPs. In: AAAI. pp. 11792–11800. AAAI Press (2021)
  * [13] Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: A modern probabilistic model checker. In: CAV. LNCS, vol. 10427, pp. 592–600. Springer (2017)
  * [14] Hansen, E.A.: Solving pomdps by searching in policy space. In: UAI. pp. 211–219. Morgan Kaufmann (1998)
  * [15] Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: TACAS. LNCS, vol. 13993, pp. 469–488. Springer (2023)
  * [16] Hauskrecht, M.: Incremental methods for computing bounds in partially observable Markov decision processes. In: AAAI/IAAI. pp. 734–739 (1997)
  * [17] Heck, L., Spel, J., Junges, S., Moerman, J., Katoen, J.: Gradient-descent for randomized controllers under partial observability. In: VMCAI. LNCS, vol. 13182, pp. 127–150. Springer (2022)
  * [18] Horak, K., Bosansky, B., Chatterjee, K.: Goal-hsvi: Heuristic search value iteration for Goal POMDPs. In: IJCAI. pp. 4764–4770. AAAI Press (2018)
  * [19] Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Finite-state controllers of POMDPs via parameter synthesis. In: UAI. pp. 519–529 (2018)
  * [20] Kurniawati, H., Hsu, D., Lee, W.S.: SARSOP: Efficient point-based POMDP planning by approximating optimally reachable belief spaces. In: Robotics: Science and Systems. MIT Press (2008)
  * [21] Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based abstraction for markov decision processes. In: QEST. pp. 157–166. IEEE Computer Society (2006)
  * [22] Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. LNCS, vol. 6806, pp. 585–591. Springer (2011)
  * [23] Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artificial Intelligence 147(1), 5–34 (2003)
  * [24] Meuleau, N., Kim, K., Kaelbling, L.P., Cassandra, A.R.: Solving pomdps by searching the space of finite policies. In: UAI. pp. 417–426. Morgan Kaufmann (1999)
  * [25] Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Systems 53(3), 354–402 (2017)
  * [26] Puterman, M.L.: Markov decision processes: discrete stochastic dynamic programming. John Wiley & Sons (1994)
  * [27] Smallwood, R.D., Sondik, E.J.: The optimal control of partially observable Markov processes over a finite horizon. Oper. Res. 21(5), 1071–1088 (1973)
  * [28] Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: ICML. vol. 80, pp. 5052–5061. PMLR (2018)
  * [29] Wang, Y., Chaudhuri, S., Kavraki, L.E.: Bounded policy synthesis for pomdps with safe-reachability objectives. In: AAMAS. pp. 238–246. International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM (2018)

##  Appendix 0.A MDP abstraction for general FSCs

##### Design space.

It is convenient to have a concise representation of a family of FSCs. Assume
POMDP $\mathcal{M}$, memory model $\mu$ and a family
${\mathcal{F}^{\mathcal{M}}_{\mu}}$ of $\mu$-FSCs with the set
$N=\\{n_{0},\dots,n_{k-1}\\}$ of memory nodes, where $k=\max_{z\in Z}\mu(z)$.
Let $N_{z}\coloneqq\\{n_{0},\dots,n_{\mu(z)-1}\\}$ denote the set of memory
nodes available to observation $z$. Family ${\mathcal{F}^{\mathcal{M}}_{\mu}}$
is parameterised by the choice of the action function $\gamma\colon N\times
Z\rightarrow Act$ and the update function $\delta\colon N\times Z\times
Z\rightarrow N$. Thus, to represent ${\mathcal{F}^{\mathcal{M}}_{\mu}}$, for
every $z,z^{\prime}\in Z$ and for each $n\in N_{z}$, we introduce parameters
$\gamma_{n}^{z}\in Act$, $\delta_{n}^{z,z^{\prime}}\in N_{z^{\prime}}$. The
sets

$\Gamma_{\mu}\coloneqq\\!\\!\prod_{z\in Z}\prod_{n\in
N_{z}}\\!\\!\left\\{\gamma_{n}^{z}=\alpha\mid\alpha\in Act\right\\}\quad\text{
and }$

$\Delta_{\mu}\coloneqq\\!\\!\prod_{z\in Z}\prod_{n\in
N_{z}}\prod_{z^{\prime}\in
Z}\\!\\!\left\\{\delta_{n}^{z,z^{\prime}}=n^{\prime}\mid n^{\prime}\in
N_{z^{\prime}}\right\\}$

collect possible assignments of parameters related to the functions $\gamma$
and $\delta$, respectively. Thus, the set of policies is represented by the
_design space_ $\mathcal{D}_{\mu}\coloneqq\Gamma_{\mu}\times\Delta_{\mu}$. The
goal of the inductive synthesis is now to select the assignment of all
parameters $\gamma_{n}^{z}$ and $\delta_{n}^{z,z^{\prime}}$ so that the
corresponding FSC $(N,n_{0},\gamma,\delta)$ induces the optimal Markov chain.

##### Refined MDP abstraction.

Let $post(s,\alpha)\coloneqq\\{O(s^{\prime})\mid
s^{\prime}\in\mathrm{supp}(\mathcal{P}(s,\alpha))\\}$ denote the set of
posterior observations available when executing $\alpha\in Act$ in $s\in S$.
Then, if $\alpha$ is executed in state $s$ and $n\in N_{O(s)}$ is the current
memory node, then the following parameter assignments

$\Delta_{\mu}[s,n,\alpha]\coloneqq\prod_{z^{\prime}\in
post(s,\alpha)}\left\\{\delta_{n}^{O(s),z^{\prime}}=n^{\prime}\mid
n^{\prime}\in N_{z^{\prime}}\right\\}$

are relevant to determine the new memory node. The following definition
refines the earlier naive version in Def. 6.

###### Definition 8

_MDP abstraction_ for POMDP $\mathcal{M}$ and a family
${\mathcal{F}^{\mathcal{M}}_{\mu}}$ of $\mu$-FSCs is an MDP
$\textsf{MDP}\left({\mathcal{F}^{\mathcal{M}}_{\mu}}\right)\coloneqq\left(S\times
N,(s_{0},n_{0}),Act\times\Delta_{\mu},\mathcal{P}^{\mathcal{F}^{\mathcal{M}}_{\mu}}\right)$
with the transition function

$\mathcal{P}^{\mathcal{F}^{\mathcal{M}}_{\mu}}((s,n),(\alpha,\delta))\coloneqq\left\\{(s^{\prime},n^{\prime})\mapsto\left[\delta_{n}^{O(s),O(s^{\prime})}=n^{\prime}\right]\cdot\mathcal{P}(s,\alpha,s^{\prime})\right\\}$

Notice that in this MDP abstraction state $(s,n)$ has only $\sum_{\alpha\in
Act}\left|\Delta_{\mu}[s,n,\alpha]\right|$ unique actions.

##  Appendix 0.B Sizes of FSC of various sub-classes

Assume a POMDP $\mathcal{M}$, a $k$-FSC $F=(N,n_{0},\gamma,\delta)$ with the
set $N=\\{n_{0},\dots,n_{k-1}\\}$ of memory nodes and an induced MC
$\mathcal{M}^{F}=(S\times N,(s_{0},n_{0}),\\{\alpha\\},\mathcal{P}^{F})$.
Recall that in order to avoid an explicit encoding of $\delta$ requiring
${k\cdot|Z|^{2}}$ space, we use sets
$post(n,z)\coloneqq\left\\{O(s^{\prime})\mid\exists s\in
S_{z}\colon(s^{\prime},\cdot)\in\mathrm{supp}(\mathcal{P}^{F}((s,n),\alpha))\right\\}$
of posterior observations available when making a transition in states $(s,n)$
of $\mathcal{M}^{F}$ with prior observation $z$. Then, $\delta(n,z,\cdot)$ can
be encoded as a list $\left\\{(z^{\prime},\delta(n,z,z^{\prime})\mid
z^{\prime}\in post(n,z)\right\\}$ of posterior-node pairs. Thus,

$size(\delta)=\sum_{n\in N}\sum_{z\in Z}2\cdot|post(n,z)|=2\cdot\sum_{n\in
N}\sum_{z\in Z}|post(n,z)|.$

Using memory model $\mu$ refines the generic $k$-factor: for observation $z\in
Z$ there are now not $k$ but only $\mu(z)$ distinct memory nodes. Therefore,

$\displaystyle size(\gamma)$ $\displaystyle=\sum_{z\in
Z}\sum_{i=0}^{\mu(z)-1}1=\sum_{z\in Z}\mu(z)$ $\displaystyle size(\delta)$
$\displaystyle=2\cdot\sum_{z\in Z}\sum_{i=0}^{\mu(z)-1}|post(n_{i},z)|$

If $\mu$-FSC is posterior-unaware, i.e. $\delta(n_{i},z,z^{\prime})$ is the
same for all $z^{\prime}\in Z$, then for each $z\in Z$ and
$n_{i}\in\left\\{n_{0},\dots,n_{\mu(z)-1}\right\\}$ it is sufficient to store
a single value $\delta(n_{i},z,\cdot)$. Thus,

$size(\delta)=\sum_{z\in Z}\sum_{i=0}^{\mu(z)-1}1=\sum_{z\in Z}\mu(z)$

and $size(\gamma)=\sum_{z\in Z}\mu(z)$, as before.

Finally, assume a composite FSC $F_{\mathcal{B}}=(\mathcal{E}\cup
N,b_{0},\gamma,\delta)$ obtained after applying
$F_{\mathcal{I}}=(N,n_{0},\gamma_{\mathcal{I}},\delta_{\mathcal{I}})$ at
frontier states. Recall that each non-frontier state $b\in\mathcal{E}$ is
associated with the unique prior observation $O(b)$. Therefore, for every
$b\in\mathcal{E}$ we must store exactly 1 action and a list
$\left\\{(z^{\prime},\delta(b,O(b),z^{\prime})\mid z^{\prime}\in
post(b,O(b))\right\\}$ of posterior-belief pairs. Finally, we must also
account for the size of FSC $F_{\mathcal{I}}$ used for cut-offs. Overall, we
obtain:

$\displaystyle size(\gamma)$
$\displaystyle=size(\gamma_{\mathcal{I}})+\sum_{b\in\mathcal{E}}1=size(\gamma_{\mathcal{I}})+|\mathcal{E}|$
$\displaystyle size(\delta)$
$\displaystyle=size(\delta_{\mathcal{I}})+\sum_{b\in\mathcal{E}}2\cdot\left|post(b,O(b))\right|=size(\delta_{\mathcal{I}})+2\cdot\sum_{b\in\mathcal{E}}\left|post(b,O(b))\right|$

##  Appendix 0.C New POMDP Lanes+

This section describes the new model, Lanes+, used in our experimental
evaluation. Fig. 5(a) illustrates the structure of the Lanes+ model: it is a
sequential composition of a Lanes POMDP (described below) repeated 100 times,
followed by the POMDP from Fig. 2(a) extended to 100 states, followed by the
POMDP from Fig. 2(b). The core component – Lanes model – was designed with two
main goals in mind: i) the optimal FSC $F_{\mathcal{I}}$ requires several
memory nodes and ii) the model can be easily scaled up such that an exhaustive
policy search is not feasible. When combining Lanes with POMDPs from Fig 2, we
obtain a model the analysis of which is unfeasible for standalone methods and
requires their two-way integration.

Fig. 5(b) depicts the structure of the Lanes model. Similarly to POMDPs
presented in Fig. 2, assume an agent that attempts to reach the target state
$T$ as fast as possible. In order to reach $T$, the agent must cross three
_lanes_ : slow, moderate and fast. The agent initially starts in a random lane
chosen uniformly (i.e. with probability 1/3). Each lane consists of 8 states
and in each state, the agent has two actions available: $\alpha$ and $\beta$.
One of these actions is an upgrading action which moves the agent with
probability $p_{u}$ to the next lane (or to the target state when performed in
the fast lane); with probability $1{-}p_{u}$ the agent moves to the next state
of the same lane. The other action is a stalling action: it moves the agent to
the next state of the same lane with probability 1. Which of the actions
$\alpha,\beta$ is the upgrading one differs depending on the lane and the
current position in the lane. Additionally, the lanes are circular: when
residing in the last state of the lane, failing to upgrade the lane or
performing the stalling action moves the agent back to the beginning of the
current lane. The only available observation for the agent is its current
lane.

There are two differences between individual lanes. First, their speed:
performing any action in the slow lane takes 5 time units, 3 for the moderate
lane and 1 for the fast lane. Second, the distribution of upgrading/stalling
actions is also different in each lane. For instance, in the slow lane, every
other state has action $\alpha$ as the upgrading one; in the moderate one,
states $1,2$ and $5,6$ have $\alpha$ as the upgrading action, etc. Due to this
irregularity of upgrading actions as well as due to the fact that only lanes
are observable, but not individual states, the best policy must keep track of
the current position in the lane, implying that 8 memory nodes are needed to
encode the optimal FSC. The corresponding family
${\mathcal{F}^{\mathcal{M}}_{\mu}}$ contains $\approx\\!10^{43}$ controllers,
which is unattainable for inductive search. Meanwhile, the belief-based
analysis is straightforward since the belief MDP $\mathcal{M}^{\mathcal{B}}$
is finite.

(a)

(b)

Figure 5: (a) Overall structure of the Lanes+ POMDP. (b) The Lanes POMDP. When
performing the upgrading action (e.g. action $\alpha$ in the first state of
the slow lane), the lane is upgraded with probability $p_{u}$; with
probability $1{-}p_{u}$ the agent moves to the next state of the lane.