# Inductive Synthesis of Finite-State Controllers for POMDPs

Roman Andriushchenko  Brno University of Technology, Brno, Czech Republic
Milan Češka<EMAIL_ADDRESS>Brno University of Technology, Brno, Czech
Republic
Sebastian Junges  Radboud University, Nijmegen, Netherlands
Joost-Pieter Katoen  RWTH Aachen University, Aachen, Germany

###### Abstract

We present a novel learning framework to obtain finite-state controllers
(FSCs) for partially observable Markov decision processes and illustrate its
applicability for indefinite-horizon specifications. Our framework builds on
oracle-guided inductive synthesis to explore a design space compactly
representing available FSCs. The inductive synthesis approach consists of two
stages: The outer stage determines the design space, i.e., the set of FSC
candidates, while the inner stage efficiently explores the design space. This
framework is easily generalisable and shows promising results when compared to
existing approaches. Experiments indicate that our technique is (i)
competitive to state-of-the-art belief-based approaches for indefinite-horizon
properties, (ii) yields smaller FSCs than existing methods for several models,
and (iii) naturally treats multi-objective specifications.

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F_i

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F

###### Abstract

F_n

###### Abstract

F_n

###### Abstract

F_1

##  1 Introduction

Partially observable MDPs (POMDPs) model sequential decision making processes
in which the agent only observes limited information about the current state
of the system [Smallwood and Sondik, 1973, Kaelbling et al., 1998]. The key
challenge in the analysis of POMDPs is to compute a policy satisfying some
constraints, captured as a threshold on (discounted) reward or as a task
description given in, e.g., a temporal logic. In full generality, policies
need arbitrary memory to reflect the belief state of the agent. Point-based
[Pineau et al., 2006, Spaan and Vlassis, 2005] and Monte Carlo methods [Silver
and Veness, 2010] excel in finding such policies. Solving the generally
undecidable policy learning problem profits from having complementary
approaches in the portfolio. A natural alternative is to search for (small)
finite state controllers (FSCs) [Hansen, 1998]. Such controllers provide
benefits in terms of explainability [Bonet et al., 2010, Wang and Niepert,
2019], resource-consumption [Grześ et al., 2013], and generalisability [Inala
et al., 2020]. Recently, an automata learning framework has been proposed for
synthesising permissive FSCs [Wu et al., 2021]. In this paper, we propose a
novel approach— _inductive synthesis_ —to find FSCs for POMDPs.

Inductive synthesis is a technique developed in the context of program
synthesis, originally proposed by Church in the 1950’s, the task to construct
a program that provably satisfies a given formal specification. As developing
a program (or in this context, a controller) from scratch is mostly
infeasible, variants emerged, most notably syntax-guided synthesis [Alur et
al., 2015, 2018] variations such as _sketching_ [Solar-Lezama et al., 2006].
In sketching, the user provides a sketch that outlines a controller
implementation, and a specification that constrains the controller’s
behaviour. The principal engine behind many instances of sketching is (oracle-
guided) _inductive synthesis_ [Jha and Seshia, 2017] and falls in a more
general framework of learner-teacher frameworks. In a nutshell, this
methodology suggests to heuristically _guess_ candidate solutions, to
_validate_ them, and in case the solution is not satisfactory, _learn_ in
order to refine the search heuristic. The successful application of inductive
synthesis has inspired numerous applications beyond classical programming,
including recent works on sketching of probabilistic programs [Nori et al.,
2015, Ceska et al., 2021, Andriushchenko et al., 2021b] and (variations of)
programmatic reinforcement learning [Verma et al., 2018, Inala et al., 2020].
_This paper proposes inductive synthesis to search for FSCs in POMDPs._

LearnerTeacherSearcherEval

Abstr Oracle

FSCvalue $\&$ conflictsdesign spacebest FSCdesign spacevalue bounds(sub)design
spacevalue bounds Figure 1: Nested Inductive Synthesis Framework with an
Abstraction Oracle. The framework takes a POMDP and a specification and finds
an FSC that satisfies the specification.

Our inductive synthesis framework works in two stages, see Fig. 1. Let us
first discuss the outer stage. Here, a learner constructs a _design space_
containing (finitely many) FSCs. A teacher provides the ‘best’ FSC within this
design space, and potentially additional diagnostic information. The learner
either accepts the FSC provided by the teacher as final result, or adapts the
design space. Naturally, teachers will provide much better FSCs much faster
whenever the design space for these FSCs is small. The key ingredient for the
outer stage is thus to start with a small design space and to strategically
adapt this design space based on the obtained feedback from the teacher. A
similar idea was proposed in [Kumar and Zilberstein, 2015], where the entropy
of the observations is used as criterion for adding memory to the FSC. We use
the FSC returned by the teacher together with the state-values induced by this
FSC. Additionally, we use an abstraction oracle, see below.

The inner stage describes the internals of the teacher that determines the
‘best’ FSC within the design space. The teacher may naively use enumeration,
but can also be realised using branch-and-bound [Grześ et al., 2013] or mixed-
integer linear programming (MILP) [Amato et al., 2010, Kumar and Zilberstein,
2015]. We realise the teacher by (another) inductive synthesis loop. We search
for an FSC by symbolically representing the design space as a propositional
logic formula. The policy evaluation analyses the fixed policy w.r.t. a given
specification (e.g., a reward function and a threshold). If the policy refutes
the specification, the evaluation engine indicates the distance to
satisfaction (e.g., the achieved value) as well as conflicts—critical parts of
the FSC that suffice to violate the specification—that are used to prune the
search design space [Ceska et al., 2021].

Both learning stages have access to an additional oracle that, inspired by
Andriushchenko et al. [2021a], _over-approximates_ the design space. This
larger abstract design space can efficiently be analysed as the underlying
problem solved by the oracle resembles the analysis of fully observable
policies. The oracle yields constraints to what the best FSC within the
original design space will possibly achieve. This information is an essential
ingredient to guide the search in both stages.

The separate policy evaluation—a natural component in an inductive synthesis
framework—brings some advantages. The policy evaluation (i.e., solving systems
of linear equations) via dedicated algorithms is faster than letting an (MI)LP
solver solve these equations [Dehnert et al., 2014]. This improves upon
performance of MILP-based approaches (either primal [Winterer et al., 2020] or
dual [Kumar and Zilberstein, 2015]) for FSC synthesis. Furthermore, as the
policy is fixed, our framework provides an elegant alternative to existing
approaches for constrained POMDPs [Poupart et al., 2015, Khonji et al., 2019]
and multi-objective POMDPs [Soh and Demiris, 2011, Roijers et al., 2013, Wray
and Zilberstein, 2015]. It additionally paves the way to learn robust FSCs for
POMDPs with imprecise probabilities, similar to [Cubuktepe et al., 2021].

We instantiate our framework to learn _deterministic_ FSCs, i.e., FSCs that do
not use randomisation. Finding optimal deterministic FSCs is NP-complete
whereas finding optimal randomised FSCs is ETR-complete111The class ETR lies
between NP and PSPACE. [Junges et al., 2018, 2021]. Algorithmically, finding
randomised FSCs requires solving non-convex optimisation problems with
thousands of variables. This often limits the guarantees on global
(almost-)optimality that are practically feasible [Kumar and Zilberstein,
2015]. Deterministic FSCs are additionally beneficial in terms of
reproducibility of their behaviour, which is useful for debugging. We use an
evaluation framework that supports indefinite horizon queries, e.g., queries
with a discount factor one. These support queries with a discount factor, but
also settings as used in Goal-POMDPs [Bonet and Geffner, 2009, Kolobov et al.,
2011]. These queries naturally occur when using temporal logic specifications
and are particularly adequate for safety-critical aspects.

The experimental evaluation shows the applicability of our approach on a wide
range of benchmarks with promising results. Particularly, it significantly
outperforms approaches based on MILP optimisation. We further compare it with
the state-of-the-art belief-based approaches, namely, with recent works in
formal verification on under-approximation for indefinite-horizon
specifications [Norman et al., 2017, Bork et al., 2022]. Our inductive
synthesis approach is highly competitive and for several POMDPs (having a
moderate number of observations/actions and large/infinite belief-space), it
is able to find small FSCs improving lower bounds of existing solutions.

##  2 Problem Statement

A _(discrete) distribution_ over a finite set $X$ is a function $\mu\colon
S\rightarrow[0,1]$ s.t. $\sum_{x}\mu(x)=1$. The set $Distr(X)$ contains all
distributions over $X$.

A _Markov decision process (MDP)_ is a tuple $M=(S,s_{0},Act,P)$ with a finite
set $S$ of _states_ , an initial state $s_{0}\in S$, a finite set $Act$ of
_actions_ , and a _transition probability function_
$P(s^{\prime}\leavevmode\nobreak\ |\leavevmode\nobreak\ s,a)$ that gives the
probability of evolving to $s^{\prime}$ after taking action $a$ in $s$. A
_Markov chain_ (MC) is an MDP with $|Act|=1$; its transition function is
written as $P(s^{\prime}\leavevmode\nobreak\ |\leavevmode\nobreak\ s)$. Markov
decision processes can additionally be equipped with a reward function
$r(s,a)$. We do not use discount factors, see the paragraph on specifications
below.

A _Partially Observable MDP (POMDP)_ $\mathcal{M}=(S,s_{0},Act,P,Z,O)$ extends
MDP $M$ with a finite set $Z$ of _observations_ , and a (deterministic)
_observation function_ 222Observation functions resulting in a distribution
over observations can be encoded by deterministic observation functions at the
expense of a polynomial blow-up [Chatterjee et al., 2016]. $O$ that returns
for every state $s$ an observation $Z(s)=z\in Z$. The observation $z\in Z$ is
said to be _trivial_ if there is only one state $s\in S$ with $O(s)=z.$

Finite State Controllers (FSCs) are automata that compactly represent
policies. We call its states nodes to distinguish them from POMDP states. FSCs
in the literature come in various styles, in particular either as Moore
machines, with the output—the action it selects—determined by the node, or as
Mealy machines, with the output determined by the taken transition [Amato et
al., 2010]. In the context of sketching FSCs and their inductive exploration,
it is convenient to describe controllers as Mealy machines. Furthermore, we
restrict ourselves to deterministic FSCs.

Formally, a _finite-state controller_ (FSC) for a POMDP $\mathcal{M}$ is a
tuple $F=(N,n_{0},\gamma,\delta)$, where $N$ is a finite set of _nodes_ ,
$n_{0}\in N$ is the _initial node_ , $\gamma(n,z)$ determines the action when
the agent is in node $n$ and observes $z$, while $\delta$ updates the memory
node to $\delta(n,z)$, when being in $n$ and observing $z$. For $|N|=k$, we
call an FSC a $k$-FSC.

Figure 2: A simple maze problem (left), a part of a 2-FSC (right, top) and a
part of the induced MC (right, bottom).

Imposing $k$-FSC $F$ onto POMDP $\mathcal{M}$ yields the Markov chain (MC)
$\mathcal{M}^{F}=(S^{F},(s_{0},n_{0}),P^{F})$ with ${S^{F}=S\times N}$ and
using333 Iverson-brackets: $[x]=1$ if predicate $x$ is true, $0$ otherwise.
$z=O(s)$:

$P^{F}((s^{\prime},n^{\prime})\leavevmode\nobreak\ |\leavevmode\nobreak\
(s,n))=P(s^{\prime}\leavevmode\nobreak\ |\leavevmode\nobreak\
s,\gamma(n,z))\cdot[\delta(n,z)=n^{\prime}].$

######  Example 1.

As running example, we use a simple variant of the maze problem [Hauskrecht,
1997], where an agent tries to reach the state $s_{T}$, modelled by the POMDP
$\mathcal{M}$ with $S=\\{s_{0},\ldots s_{9},s_{T}\\}$, $Act=\\{u,d,l,r\\}$,
and $Z=\\{z_{0},\ldots,z_{5}\\}$. The initial state is given by a uniform
distribution over $S$. Fig. 2(left) depicts $P$ and $O$ where state $s_{x}$ is
labelled by $x/y$ with $x$ the state index and $y$ its observation, i.e.,
$O(s_{x})=z_{y}$. The arrow direction from $x/y$ to $x^{\prime}/y^{\prime}$
represents the action; e.g., $\rightarrow$ corresponds to action $r$. The maze
is slippery. An action is successful with probability $0.9$; with $0.1$, the
agent does not move. Actions without effect are omitted from the figure. Fig.
2 (right, top) illustrates a fragment of a 2-FSC where
$\gamma(0,0)=\gamma(0,1)=r$ (for memory node 0 and observations $z_{0}$ and
$z_{1}$, action $r$ is chosen), $\gamma(0,3)=\gamma(1,1)=l$,
$\delta(0,0)=\delta(0,1)=0$ (memory node 0 is not changed for $z_{0}$ an
$z_{1}$) and $\delta(0,3)=\delta(1,1)=1$. This FSC tries to resolve the
inconsistency (formalised later) in the observation $z_{1}$, i.e., in $s_{1}$
the action $r$ is optimal but in $s_{3}$ action $l$ is optimal (w.r.t.
reaching $s_{T}$). Fig. 2 (right, bottom) illustrates a fragment of the
induced MC containing two copies of $s_{2}$.

Specifications contain two parts: a set of _constraints_ given by quantitative
properties and a single optimisation _objective_. Constraints are defined as
indefinite-horizon reachability and expected reward properties, but our
approach also supports more general probabilistic temporal logic properties
[Baier and Katoen, 2008]444These properties can describe thxe setting of goal-
POMDPs, finite horizon reachability and rewards, and discounted rewards. Let
target set $T\subseteq S$, _thresholds_ $\lambda_{1}\in[0,1]$ and
$\lambda_{2}\in\mathbb{R}^{+}$ and $\bowtie\,\in\\{\leq,\geq\\}$. The POMDP
$\mathcal{M}$ under FSC $F$ _satisfies_ the constraint
$P_{\bowtie\lambda_{1}}$ if the probability $\Pr^{F}$ of reaching $T$ in the
induced MC $\mathcal{M}^{F}$ meets $\bowtie\lambda_{1}$. Similarly, the
constraint $R_{\bowtie\lambda_{2}}$ is satisfied if the expected reward
$R^{F}$ accumulated in MC $\mathcal{M}^{F}$ until reaching $T$ meets
$\bowtie\lambda_{2}$. We call an FSC $F$ _admissible_ (for $\mathcal{M}$), if
$\mathcal{M}$ under $F$ satisfies the given (set of) constraint(s). Objectives
either minimise or maximise reachability probabilities (as in goal-POMDPs) or
(un)discounted expected reward properties, denoted as $P_{*}$ and $R_{*}$
respectively for $*\in\\{\min,\max\\}$. The probability or reward obtained by
FSC $F$ on $\mathcal{M}$ is called the _value_ of $F$. For conciseness, we
assume throughout the paper that the specification contains a maximisation
objective. Minimisation is analogously supported (but may require flipping
bounds and inequalities).

##### Problem statement.

We aim to construct an algorithm that: i) quickly finds a (small) admissible
FSC $F$ and ii) incrementally improves $F$ w.r.t. the optimisation objective.
We can view the algorithm as solving a sequence of decision problems, where
the first decision problem is to find some admissible FSC $F_{0}$, and
decision problem $i{+}1$ is to find an admissible FSC $F_{i+1}$ whose value
improves upon the value of the previous FSC $F_{i}$.

##  3 Inductive exploration of FSCs

This section presents the inner loop (see Fig. 1) in which we search among a
given set of $k$-FSCs. Before we describe the ingredients, we formalise the
representation of the set of $k$-FSCs. We then outline the two oracles that
our search can use to prune the search space. A _hybrid strategy_
[Andriushchenko et al., 2021a] combines the two oracles by switching based on
perceived performance while communication between the oracles takes place.

###  3.1 Families of FSCs

A POMDP and a single FSC induce a Markov chain. A POMDP and a set of FSCs thus
induces a set of MCs. The set of FSCs has additional structure enabling a
concise representation as a family-MC. We first consider _full_ FSCs where for
each observation the same amount of memory is used. We generalise this to a
class of _reduced_ FSCs that are more memory efficient.

######  Definition 1.

A _family_ of full $k$-FSCs is a tuple $\mathcal{F}_{k}=(N,n_{0},K)$, where
$N$ is the set of $k$ nodes, $n_{0}\in N$ is the initial node, $K=N\times Z$
is a finite set of parameters each with domain $V_{(n,z)}\subseteq Act\times
N$.

An FSC is obtained by choosing values for each parameter. Their domains
determine the set of FSCs described by the family. Families of FSCs thus
contain $\mathcal{O}(|N||Z|)$ many FSCs. To simplify the notation, we will
interpret $\mathcal{F}_{k}$ as a set of $k$-FSCs. A POMDP $\mathcal{M}$ and a
family $\mathcal{F}_{k}$ naturally induces the family of MCs
$\mathcal{M}^{\mathcal{F}}=\\{\mathcal{M}^{F}\mid F\in\mathcal{F}_{k}\\}$.

######  Example 2.

The family $\mathcal{F}_{2}$ of all 2-FSCs for our maze problem is given by
$N=\\{n_{0},n_{1}\\}$, $K=\\{(n_{i},z_{j})\mid i\in\\{0,1\\}\wedge
j\in\\{u,d,l,r\\}\\}$, $V_{(n,z)}=\\{u,d,l,r\\}\times\\{n_{0},n_{1}\\}$ for
all $(n,z)\in K$.

While FSCs have $k$ available memory nodes in conjunction with every
observation, memory is often required only in some observation (see e.g., the
running example). Therefore, we consider reduced FSCs given by a _memory
model_ $\mu:Z\rightarrow\mathbb{N}$, where $\mu(z)$ determines the number of
memory nodes used in the observation $z$. The reduced FSC requires $\max_{z\in
Z}\\{\mu(z)\\}$ nodes, but the parameter domains are significantly reduced. In
the previous example as well as in various benchmarks, memory is required only
in a few observations, dropping the number of mappings to
$\mathcal{O}(|N|{+}|Z|)$.

######  Definition 2.

A _reduced family_ $\mathcal{F}_{\mu}$ given by the memory model $\mu$ is a
sub-family of $\mathcal{F}_{k}$ for $|N|=\max_{z\in Z}\\{\mu(z)\\}$ where
$(n,z)\in K$ implies $n\leq\mu(z)$, and the domains $V_{(n,z)}$ are as in
$\mathcal{F}_{k}$555If a memory update $\delta(n,z)=n^{\prime}$ is invalid in
the resulting observation $z^{\prime}$ (i.e. $n^{\prime}>\mu(z^{\prime})$),
the update to $n_{0}$ is used..

Such reduction has several key benefits: in the case of resource-aware
applications, the memory needed to store and execute the controller is
reduced, better interpretability of the controller is achieved, and finally
the family of reduced FSCs induces a smaller design space (the number of
parameters is given by the size of the mappings).

###  3.2 MDP abstraction

As families of MCs may become large, it is beneficial to consider an
abstraction (represented as a single MDP) of it.

######  Definition 3.

MDP
$\begin{abstract}\mathcal{F}\end{abstract}=(S{\times}N,(s_{0},n_{0}),Act^{\mathcal{F}},P^{\mathcal{F}})$
is an _abstraction_ of MC family $\mathcal{M}^{\mathcal{F}}$ with
$Act^{\mathcal{F}}=Act\times N$ and
$P^{\mathcal{F}}((s^{\prime},n^{\prime})\leavevmode\nobreak\
|\leavevmode\nobreak\ (s,n),(a,n^{\prime}))=P(s^{\prime}\leavevmode\nobreak\
|\leavevmode\nobreak\ s,a)$ if $(a,n^{\prime})\in V_{(n,O(s))}$, and 0
otherwise.

For MDPs and our specifications, it suffices to consider deterministic
memoryless policies, i.e., policy $\pi$ for MDP is a function $\pi\colon
S{\times}N\rightarrow Act$. It is _consistent_ if $O(s)=O(s^{\prime})$ implies
$\pi((s,n))=\pi((s^{\prime},n))$ for all $s,s^{\prime}\in S,n\in N$. The set
of consistent polices in matches the family $\mathcal{F}$. The parameter
$(n,z)\in K$ is _inconsistent_ in $\pi$ if $\exists{s,s^{\prime}\in
S}:O(s)=O(s^{\prime})=z\wedge\pi((s,n))\neq\pi((s^{\prime},n))$. The
observation $z\in Z$ is inconsistent if the parameter $(n,z)\in K$ is
inconsistent for some $n\in N$.

######  Example 3.

Assume we want to maximise the probability to reach $s_{T}$. The stars in Fig.
2 represent the optimal policy $\pi^{*}$ in MDP where $\mathcal{F}$ is set of
all 1-FSCs for the maze problem. $\pi^{*}$ is inconsistent in the observations
$z_{1}$ and $z_{4}$.

The analysis of MDP provides useful information about the family
$\mathcal{F}$. Assume our interest is to maximise the constraint
$P_{\geq\lambda}$ for target set $T$. (Reasoning for constraints of the form
$P_{\leq\lambda}$ is dual and expected reward constraints are handled the
same). Let policy $\pi^{*}$ in achieve the probability $\Pr^{\pi^{*}}$. If
$\Pr^{\pi^{*}}<\lambda$, it is guaranteed that all $F\in\mathcal{F}$ violate
the constraint and $\mathcal{F}$ can be safely pruned. Otherwise, we check the
consistency of policy $\pi^{*}$. If it is consistent, it represents a valid
FSC satisfying the constraint. Similarly, a minimising policy can be used to
prove that the entire family $\mathcal{F}$ satisfies the constraint. If the
analysis of is inconclusive, $\mathcal{F}$ has to be _refined_. Additionally,
analysing provides state-vectors $ub$ and $lb$ such that $\forall s\in S$,
$ub(s)$ and $lb(s)$ represent the maximal and minimal probability to reach $T$
from $s$, respectively. These bounds are used in the inner and outer synthesis
loop.666Furthermore, the state-vectors $ub$ and $lb$ allow _bootstrapping_ the
analysis of MDP where $\mathcal{F}_{i}$ is a subfamily of $\mathcal{F}$: This
exploits the fact that $\mathcal{F}_{i}$ shares the structure of $\mathcal{F}$
while some actions for some states are removed.

For specifications with _multiple_ constraints, the optimisation objective is
handled by iteratively updating a new (initially trivial) constraint
representing the running value of the optimum so far. Once a policy $\pi$
satisfying all constraints is found, we update the new constraint according to
the objective value that $\pi$ achieves. Reasoning about multiple constraints
works as follows. If the entire family $\mathcal{F}$ violates some constraint,
it is pruned. Otherwise, we investigate the consistency of the policies found
for the constraints with the aim to find a FCS improving the optimum and
eventually to prune $\mathcal{F}$. If $\mathcal{F}$ cannot be pruned, it is
_refined_.

##### Refinement strategy

The refinement strategy is a key component in driving the exploration of the
family $\mathcal{F}$. It decomposes $\mathcal{F}$ into sub-families by
splitting the domain of selected parameters from $K$. In contrast to the
general refinement strategy used in program synthesis [Ceska et al., 2019], we
leverage the specific topology of the FSC families.

The key idea is to examine the inconsistencies of the policies $\pi^{*}$
obtained for particular constraints777We focus on the constraint derived from
improving the objective value as it usually is the most restrictive.. We
estimate the _significance_ of each inconsistent parameter $p\in K$ in
$\pi^{*}$ by examining the impact of changing $p$ in $\pi^{*}$ weighted by the
expected frequency of the decisions corresponding to $p$. We then select the
most significant parameter $p$. Assume (inconsistent) $p$ has domain
$V_{p}=\\{v_{1},\ldots,v_{n}\\}$ and $\pi^{*}$ selected the options $v_{i}$,
$v_{j}$. We partition $V_{p}$ into $V_{p}^{1}=\\{v_{i}\\}$,
$V_{p}^{2}=\\{v_{j}\\}$ and $V_{p}^{3}=V_{p}\setminus\\{v_{i},v_{j}\\}$ and
create the three corresponding subfamilies. This allows us to remove the
inconsistency of $p$ by considering the selected options $v_{i}$ and $v_{j}$
by different sub-families.

We can restrict the exploration to FSCs that are structurally close to
$\pi^{*}$. We use the _incomplete_ refinement strategy that i) fixes the
options selected by $\pi^{*}$ in perfectly observable states, ii) fixes the
options in the consistent parameters, and iii) removes options in the
inconsistent parameters that were not selected by $\pi^{*}$, i.e., the set
$V^{3}$.

###  3.3 Counter-example-based pruning

While MDP abstraction is an effective exploration strategy for large FSC
families, it can be helpful to prune the design space by analysing candidate
FSCs. If the individual candidate is admissible and has a good value, this
clearly accelerates the teacher. Otherwise, we learn counterexamples. To
realise this teacher, we represent the FSCs that have not been pruned as a
propositional formula. We use the SMT solver CVC5 [Barbosa et al., 2022] (over
quantified-free bounded integers) to effectively manipulate the propositional
formula and to find FSCs that have not been pruned.

We assume a constraint $P_{\geq\lambda}$ (for target set $T$), a family
$\mathcal{F}$, the state-vector $ub$ obtained from the maximising policy
$\pi^{*}$ in MDP , and FSC $F\in\mathcal{F}$.

######  Definition 4.

A  _counter-example_ (CE) for FSC $F$ and $P_{\geq\lambda}$ is a subset
$C\subseteq S^{F}$ that induces the sub-MC of $\mathcal{M}^{F}$ given as
$({C\cup\mathrm{succ}(C)\cup\\{s_{\bot}},s_{\top}\\},(s_{0},n_{0}),P^{\prime})$
where $P^{\prime}(s)=$

$\displaystyle\begin{cases}P^{F}(s)&\text{if }s\in C,\\\ [s_{\top}\mapsto
ub(s),s_{\bot}\mapsto 1{-}ub(s)]&\text{if }s\in\mathrm{succ}(C)\setminus C,\\\
[s\mapsto 1]&\text{if }s\in\\{s_{\top},s_{\bot}\\},\\\ \end{cases}$

where $\mathrm{succ}(C)$ is the set of direct successors of $C$, and the
probability to reach $T\cup\\{s_{\top}\\}$ from $C$ is $<\lambda$.

Intuitively, states $s$ outside the CE evolve to $s_{\top}$ with probability
$ub(s)$, the maximal probability to reach $T$ from $s$ in the family
$\mathcal{F}$ (i.e., the worst that can happen for CE in $\mathcal{F}$). They
evolve to $s_{\bot}$ with probability $1{-}ub(s)$, the minimal probability to
avoid $T$ in $\mathcal{F}$. For $(s,n)\in C$, the parameter $(n,O(s))\in K$ is
called _relevant_. The CE for the constraint $P_{\leq\lambda}$ is defined
similarly using $lb$ rather than $ub$.

For each $F^{\prime}\in\mathcal{F}$ that selects the same options as $F$ for
all relevant parameters of the CE $C$, it holds that $P^{F^{\prime}}<\lambda$.
Therefore, we can safely remove $F^{\prime}$ from the design space. We say
that $C$ _generalised_ to the set of all such $F^{\prime}$.

Smaller CEs lead to more effective pruning. As computing minimal CEs is NP-
complete [Funke et al., 2020], we use a greedy approach proposed in
[Andriushchenko et al., 2021a]. Handling multiple constraints is
straightforward as we can compute the CE for each constraint violated by the
FSC $F$. This can potentially improve the pruning.

Similarly as the incomplete refinement strategy in Sec. 3.2, we consider an
incomplete generalisation of the CEs. In particular, we redefine the notation
of relevant parameters. The parameter $(n,O(s))$ for $(s,n)\in C$ is relevant
only if the observation $O(s)$ is inconsistent in or the option selected by
$F$ is different from the options selected by $\pi^{*}$. This leads to more
aggressive pruning and restricts the exploration to the FSCs that are
topologically close to $\pi^{*}$.

######  Example 4.

Consider a variant of our maze problem with initial state $s_{0}$, family
$\mathcal{F}$ of all 1-FSCs, where the available set of actions in the
observation $o_{3}$ is restricted s.t.
$V_{(n_{0},z_{3})}\in\\{u,d,r\\}\times\\{0\\}$. Let FSC $F$ as in Fig 3
(left). The right part illustrates the induced MC and the middle part shows
the CE $C$ for the constraint $P_{\geq 1}$. Note $P((s_{4},n_{0}),s_{\bot})=1$
as $ub(s_{4})=0$. Thus, the relevant parameters are $(n_{0},z_{i})$ for
$i\in\\{0,1,2\\}$. The generalisation of $C$ enables pruning a significant
part of $\mathcal{F}$. Under incomplete generalisation, the parameter
$(n_{0},z_{0})$ is not relevant as it is consistent in and $F$ picks the same
option as $\pi^{*}$.

Figure 3: A CE for the given FSC in the maze problem.

##  4 Memory injection strategy

This section discusses the outer stage of our approach, cf. Fig. 1, in which
the learner decides _where_ to search. In particular, a subset of FSCs is
selected and passed onto the teacher, as outlined in Sec. 3. We assume access
to an abstraction oracle that yields bounds on the value for every state based
on an abstraction scheme outlined in Sec. 3.2. The learner processes this
information and derives a new design space. It does so by combining a couple
of ingredients:  1. _Adding memory_ : By allowing FSCs to store more
information, we (drastically) increase the design space. We allow to locally
increase memory to keep the growth manageable.  2. _Removing symmetries_ :
Similar to [Grześ et al., 2013], it is unnecessary to include symmetric FSCs
in the design space.  3. _Analysing abstractions_ : Use the results from the
abstraction to guide the search.

###  4.1 Adding Memory

The key idea of the memory injection strategy is to use the diagnostic
information obtained from the preceding inner loop exploring the design space
represented by a family $\mathcal{F}$ to construct a new family
$\mathcal{F}^{\prime}$, say. These families are based on two fixed memory
structures (either as a full or reduced FSC). On constructing
$\mathcal{F}^{\prime}$, memory can be added that corresponds to one of the
observations, see Sec. 3.1. This section outlines where to add the memory.

To decide how to extend the family of FSCs, we use the following information:
1. the maximising policy $\pi^{*}$ in MDP together with its corresponding
bounds $ub$888 Note that the state space of MDP includes copies of states
where memory has been added previously. Without symmetry reduction, an optimal
policy (mostly) takes the same action in these copies, thus making the copies
redundant. However, in combination with the symmetry reduction, the outgoing
transitions of these copies differ and the copies are then no longer
redundant., and  2. The FSC $F^{*}$ in $\mathcal{F}$ obtained from the
teacher. Such an FSC is not available if the FSC is inadmissible or if the
teacher aborts the search.

If $F^{*}$ is not available, the memory injection strategy employs a similar
idea as the refinement strategy described in Sec. 3.3. In particular, it
evaluates the significance of the inconsistent observations w.r.t. $\pi^{*}$
by aggregating the significance of their inconsistent parameters as defined
before. By adding the memory to the most significant inconsistent observation,
we try to resolve the inconsistency and drive the search towards an FSC that
is topologically close to $\pi^{*}$.

If $F^{*}$ is available, the injection strategy tries to improve it by adding
memory to the observations where $F^{*}$ selects a different action than
$\pi^{*}$. Similarly as before, we evaluate the significance of the
observations by evaluating the significance of the corresponding parameters.
(This is possible as the expected number of visits of states in the MC induced
by $F^{*}$ or $\pi^{*}$ can be used). We estimate how changing an action in
$F^{*}$ can improve its value by looking at the state values in $ub$. We use
the expected visits in $F^{*}$ to estimate the impact of these changes. Here,
we also consider consistent (but non-trivial) observations in $\pi^{*}$.

###  4.2 Symmetry reduction

Adding memory to a selected observation typically creates FSCs in the
resulting family $\mathcal{F}$ that have the same value (see Example 5), often
because of some symmetries between the FSCs. Removing these symmetries from
$\mathcal{F}$ has two crucial benefits: i) it reduces the size of
$\mathcal{F}$ and ii) it reduces the number of inconsistencies of the
$\pi^{*}$ obtained from , see below. The importance of symmetry breaking has
been recognised by Grześ et al. [2013] who proposed a generation strategy for
isomorphism-free Moore automata. We propose a different approach based on
restricting the family of candidate FSCs. We first describe where the
symmetries are introduced, and then how we avoid this.

Let $\pi^{*}$ be the optimal inconsistent controller obtained from analysing
where $\mathcal{F}$ describes 1-FSCs (no memory was added) based on $\pi^{*}$.
In line with the above algorithm, we add memory to the inconsistent
observation $z$, where $(n_{0},z)\in K$ is the inconsistent parameter with
$V_{(n_{0},z)}=\\{(a_{1},0),\ldots,(a_{n},0)\\}$. This means
$\exists{s_{1},s_{2}\in S},(a_{i},0),(a_{j},0)\in
V_{(n_{0},z)}:O(s_{1})=O(s_{2})=z$ and
$\pi^{*}((s_{1},n_{0}))=(a_{i},n_{0})\neq(a_{j},n_{0})=\pi^{*}((s_{2},n_{0}))$.
Adding memory creates a new family $\mathcal{F}_{n}$ where $K$ includes the
new parameter $(n_{1},z)$ having the same domain as $(n_{0},z)$. It introduces
several symmetric FSCs in $\mathcal{F}_{n}$. Consider, e.g.,
$F_{0}\in\mathcal{F}_{n}$ where $\gamma(n_{0},z)=a_{i}$,
$\gamma(n_{1},z)=a_{j}$ and has a memory mapping $\delta$. Then there is also
$F_{1}\in\mathcal{F}_{n}$ that is symmetric in $z$, i.e.
$\gamma(n_{0},z)=a_{j}$, $\gamma(n_{1},z)=a_{i}$, and has a symmetric $\delta$
(otherwise it is the same as $F_{0}$). Clearly, $F_{0}$ and $F_{1}$ are
equivalent (i.e., achieve the same value) and thus we want to keep only one of
them in $\mathcal{F}_{n}$. Additionally, $\pi^{*}$ obtained for has the same
inconsistency as before, but now in both parameters.

The key idea of the symmetry reduction is to restrict $V_{(n_{0},z)}$ and
$V_{(n_{1},z)}$ in $\mathcal{F}_{n}$ such that symmetric FSCs are removed and
the inconsistency in $\pi^{*}$ for is decreased while the value of $\pi^{*}$
is preserved. In this case, the reduction can be easily achieved by removing
$a_{i}$ from $V_{(n_{0},z)}$ and $a_{j}$ from $V_{(n_{1},z)}$. If in some
state $s$, $O(s)=z$, the optimal action is $a_{i}$, then $\pi^{*}$ will ensure
that the predecessors of $s$ use, if possible, the appropriate memory update
that leads to $(s,1)$, where this action is available. This decreases the
probability of reaching $(s,0)$ as well as the significance of the possible
inconsistency associated with $(n_{0},z)$.

Removing symmetry for the first memory injection is safe (the optimal solution
is preserved). When several memory injections and symmetry reductions are
performed, the optimal solution can potentially be removed as the symmetry
reduction in one observation may affect the completeness of the reduction in
another observation via memory updates. We demonstrate the impact of symmetry
reduction in our experimental evaluation.

######  Example 5.

Consider again the maze problem from Example 1 and the specification to
minimise the expected number of steps to reach $T$. Note that this includes an
implicit constraint $P_{\geq 1}$ to reach $T$. Let $\mathcal{F}_{1}$ be the
family of all 1-FSCs. The inner loops detects that there is no admissible
1-FSC satisfying the constraint: in observation $z_{1}$ we need to be able to
pick both actions $r$ and $l$, and similarly for observation $z_{4}$.
Analysing $\pi^{*}$ in reveals that the most significant inconsistency is in
observation $z_{1}$. Thus, memory is added to $z_{1}$ and the symmetry is
removed as follows: $V_{(n_{0},z_{1})}=\\{u,d,r\\}\times\\{0,1\\}$ and
$V_{(n_{1},z_{1})}=\\{u,d,l\\}\times\\{0,1\\}$, obtaining a new family
$\mathcal{F}^{\prime}_{1}$. The inner loop again detects that no admissible
solution exists, proposing to add memory to observation $z_{4}$ as well as to
break symmetry in actions $u$ and $d$:
$V_{(n_{0},z_{4})}=\\{u,r,l\\}\times\\{0,1\\}$ and
$V_{(n_{1},z_{1})}=\\{d,r,l\\}\times\\{0,1\\}$. The third iteration finally
yields an optimal FSC with value $7.1\overline{6}$. We emphasise that no
additional memory injection can improve upon this.

##  5 Experimental evaluation

Our evaluation focuses on the following questions:

_Q1: How does our approach compare to state-of-the-art approaches to
synthesise deterministic FSCs?_ To this end, we consider the state-of-the-art
dual MILP formulation from [Kumar and Zilberstein, 2015] which uses a max-
entropy strategy for adding memory nodes. We consider a recent alternative
formulation of a primal MILP in [Winterer et al., 2020] for treating multi-
objective specifications.

_Q2: How does our approach compare with state-of-the-art belief-based
approaches?_ Although these approaches share the main idea (i.e., approximate
the underlying belief MDP that is prohibitively large or infinite), they
approach the problem by constructing an approximation of the belief-MDP. We
compare with the approach of [Norman et al., 2017] (implemented in Prism
Kwiatkowska et al. [2011]) and the recent work of [Bork et al., 2022]
(implemented in Storm [Dehnert et al., 2017]). To the best of our knowledge,
these methods provide state-of-the-art techniques for finding policies in
belief MDPs for indefinite-horizon specifications, i.e., without discounting.

_Q3: What is the effect of our heuristics on the run-time and the value of the
resulting FSCs?_

##### Selected benchmarks and experimental setting

A direct comparison with MILP-based approaches is complicated as they mostly
consider other specifications (discounted rewards) and stochastic
observations. Therefore, we selected the _Hallway_ model from [Kumar and
Zilberstein, 2015] and manually translated it to an almost equivalent model
999The values of the resulting FSCs are comparable.. We also took a multi-
objective variant of a _4×4grid avoid_ model from [Winterer et al., 2020]
(denoted as _Grid-av 4.0_) that enables a direct comparison with the multi-
objective MILP optimisation. The main evaluation considers representative
benchmarks from [Bork et al., 2020, 2022] extended by a few more involved
variants 101010The results with STORM and PRISM were provided by the authors.
The experiments run on a comparable machine.. Table 1 lists the statistics of
the models. Our results run on a single core of a machine equipped with an
Intel i5-8300H CPU and 24 GB of RAM.

Model | $S$ | $Act$ | $Z$ | Spec. | Model | $S$ | $Act$ | $Z$ | Spec. | Model | $S$ | $Act$ | $Z$ | Spec.
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
Grid-av 4-0 | 17 | 59 | 4 | $P_{\max}$ | Grid-av 4-0.1 | 17 | 59 | 4 | $P_{\max}$ | Grid 30-sl | 900 | 3587 | 37 | $P_{\max}$
Maze sl | 15 | 54 | 3 | $R_{\min}$ | Crypt 4 | 1972 | 4612 | 510 | $P_{\max}$ | Nrp 8 | 125 | 161 | 41 | $P_{\max}$
Hallway | 61 | 301 | 23 | $P_{\max}$ | Drone 4-1 | 1226 | 3026 | 384 | $P_{\max}$ | Drone 4-2 | 1226 | 3026 | 761 | $P_{\max}$
Refuel 6 | 208 | 565 | 50 | $P_{\max}$ | Netw-p 2-8-20 | $3\\!\cdot\\!10^{4}$ | $3\\!\cdot\\!10^{4}$ | 4909 | $R_{\max}$ | Rocks 12 | 6553 | $3\\!\cdot\\!10^{4}$ | 1645 | $R_{\mathrm{min}}$

Table 1: The statistics of the twelve POMDP models and the optimisation
objective.

#### Q1: Comparison to MILP-based FSC synthesis

We first compare our approach with [Kumar and Zilberstein, 2015] on the
_Hallway_ model. The dual MILP optimisation for the fixed-size reactive FSC
(equivalent to our 1-FSC) achieved the value 0.32 in 900s. This corresponds to
an FSC where the expected number of steps to reach the target equals
22.2111111[Kumar and Zilberstein, 2015] use a discount factor of 0.95. Using
the memory injection strategy, they found an FSC with 14 additional memory
nodes in 3345s achieving value 0.46, i.e., 15.1 expected steps. Our complete
strategy explored all 1-FSCs in less than 1s and found a solution achieving
18.5 expected steps. The restricted exploration of full 3-FSCs found a
solution achieving 14.9 expected steps in 156s. The default strategy used in
Tab 2 (see below) added one memory node and found a solution achieving 16.1
expected steps in less than 1s. Although the value of the resulting FSCs
cannot be exactly compared, _these results clearly demonstrate that our
approach is superior to MILP-based synthesis methods._

We also compare our approach with [Winterer et al., 2020] on the _Grid-av 4_
model with a constraint on the reachability probability and the minimisation
of an reward. The best solution of the MILP optimisation with a restricted
randomisation and memory injection has value 3.43 (found in 2.8s). This
solution is obtained by our default strategy within 1s by adding one memory
node. In 389s, it added nine memory nodes and found a solution with value
3.29. This shows that _our inductive approach outperforms the MILP
optimisation also on multi-objective specifications_.

Benchmark | PRISM | STORM | Inductive synthesis
---|---|---|---
model |  | first | best | fastest | best
Grid-av | 0.21 | $0.86$ | $0.93$ |  0.93 (3) | 0.93(4)†
4-0 | 5s | < 1 s | 14s | <1s | <1s
Grid-av | 0.21 | $0.82$ | $0.85$ | 0.85 (2) | 0.92 (10)
4-0.1 | 1s | < 1 s | 1913s | < 1s | 874s
Grid | MO/TO | 121 | - | TO | 119(6)
30-sl | <1s | - | TO | $\mathbf{3s^{*}}$
Maze | SE | 7.68 | - |  7.14(3) | 7.09(3f)
sl | 1s | - | $\mathbf{<1s}$ | $\mathbf{18s^{*}}$
Crypt | 0.33 | 0.33 | - | 0.33(0) | -
4 | 20s | < 1s | - | 3s | -
Nrp | 0.13 | 0.12 | - | 0.13(0) | -
8 | 2s | < 1s | - | < 1s | -
Hallway | SE | 19.2 | 19.3 | 16.3(1) | 14.9(3f)
| < 1s | 3s | < 1s | $\mathbf{156s^{*}}$
Drone | MO/TO | $0.79$ | - | 0.79 (0) | 0.87(0)
4-1 | < 1 s | - | 12 s | 120s
Drone | MO/TO | $0.86$ | $0.92$ | 0.93 (0) | 0.97(2)
4-2 | < 1 s | 1902s | 3 s | 611s
Refuel | 0.67 | $\mathbf{0.67}$ | $0.67$ | 0.63(8) | 0.67(2f)
6 | 4625s | < 1 s | 2076s | 2.6s | $170s^{*}$
Netw-p | $\mathbf{557}$ | $537$ | - | 539(0) | -
2-8-20 | 2355s | 2s | - | 210s | -
Rocks | MO/TO | $0.38$ | $\mathbf{20}$ | 42(0) | -
12 | 1 s | 230s | 3s | -

Table 2: The comparison with belief-base methods. Bold entries denote the best
solutions, – indicates that no better solution was found within 30 minutes, *
indicates that the result was found using a non-default strategy, MO/TO
denotes out of memory or timeout, and SE indicates errors.

#### Q2: Comparison to belief-based methods

Table 2 summarises key experimental results related to Q2. The columns list
the following information (from left to right): the model and its version, the
lower bounds provided by [Norman et al., 2017] and its run-time, the lower
bounds provided by [Bork et al., 2022] and its run-time (for two settings: the
fastest synthesis and the best bound), the results provided by our approach
(including the number of added memory nodes) and its run-time (the first
interesting solution and the best solution found).

To simplify the presentation, this table shows results (except for the entries
denoted by ∗) achieved by our approach using the default setting: the inner
loop is instantiated by the pure MDP abstraction oracle with the incomplete
refinement strategy, and the outer loop uses the memory injection strategy
with symmetry reduction. The impact of our optimisation heuristics as well as
the results for multi-objective specifications are discussed under Q3.

The results clearly demonstrate that _our inductive approach is highly
competitive with the belief-state space approximation for indefinite-horizon
specifications_. For the models having moderate number of observation/actions,
we provide better trade-offs between the run-time and the values of the found
policies. Moreover, we found small FSCs that improve the lower-bounds in [Bork
et al., 2022]. For models with a large number of observations/actions, we
found small high-quality FSCs in comparable run-time. For the _Rocks_ model
and a larger _Netw_ model, we failed to find a good solution. We highlight two
interesting results: For _Grid-av 4-0_ , our strategy injected four memory
nodes (see $\dagger$) and achieved the bound provided by the symmetry-free MDP
abstraction which guarantees the global optimum. For _Drone 4-2_ , we found a
very small FSC that implements the known upper bound on the solution value
[Bork et al., 2020].

#### Q3: The effect of optimisation heuristics

_Efficacious heuristics_ We generally remark that the design spaces in this
paper are several orders of magnitude bigger than the design spaces supported
by the more general-purpose inductive synthesis framework in [Andriushchenko
et al., 2021b]. The differences can mostly be explained by the tailored
representation and novel heuristics.

_Symmetry reduction:_ This is quite beneficial as it reduces the design space
and, more importantly, considerably helps the memory injection strategy
correctly select the most promising observation. For example, in the _Maze2_
model, the memory injection without symmetry reduction repeatedly adds memory
only due to a single observation and the optimal solution is not found. On the
other hand, symmetry reduction can discard an optimal solution as demonstrated
in the _Refuel 6, Hallway_ and _Grid large_ models. For these models, the last
column of Tab. 2 lists the results of the incomplete exploration of full
2-FSCs and 3-FSC denoted as 2f and 3f, respectively.

_Incomplete search:_ the incomplete refinement strategy and CE generalisation
is essential for handling large number of observations/actions. The complete
exploration, e.g., fails to find a good solution for the _Drone_ models. In
our experiments, we did not observe that the incomplete exploration discards
import solutions except the _Grid-av 4-0.1_ model, where the full exploration
found in 580s (after 9 memory injections) a better solution achieving 0.93.

_Hybrid approach:_ For the models in Table 2, the hybrid approach (combining
the exploration using the MDP abstraction and CE pruning) does not improve the
synthesis process. However, for models where the MDP abstraction is
significantly larger than the induced MCs corresponding to the candidate FSCs,
the hybrid approach is superior, as exemplified by the _Grid 30-sl_ model, a
more complex variant of the grid-like model, where the MDP abstraction is 15x
larger. For this model, the standard settings do not find an admissible FSC
within 30 minutes. Using the hybrid approach in the inner loop, we found an
FSC improving the solution found by the belief-based method within 3s.

_Multi-objective (MO) specifications:_ Apart from the MO variant of the _Grid-
av 4-0_ model discussed in Q1, we also considered a MO variant of the _Maze
sl_ model including a more complicated specification with an additional reach-
avoid constraint. The constraint restricts the optimal FSC, but the run-time
of the synthesis remains < 1s.

##  6 Conclusion

This paper presents a first inductive-synthesis based framework for finding
finite-state controllers (FSCs) in POMDPs. Key ingredients are the novel
heuristics to incrementally construct the memory structure of the FSC as well
as two oracles for searching and evaluating families of FSCs. The experimental
results show promising results indicating that this framework is competitive
with the state-of-the-art alternatives. Future work includes the integration
of belief-based approaches as an additional oracle.

## References

  * Alur et al. [2015] Rajeev Alur, Rastislav Bodík, Eric Dallal, et al.  Syntax-guided synthesis.  In _Dependable Software Systems Engineering_ , volume 40 of _Information and Communication Security_ , pages 1–25. IOS Press, 2015\.

  * Alur et al. [2018] Rajeev Alur, Rishabh Singh, Dana Fisman, and Armando Solar-Lezama.  Search-based program synthesis.  _Commun. ACM_ , 61(12):84–93, 2018.
  * Amato et al. [2010] Christopher Amato, Blai Bonet, and Shlomo Zilberstein.  Finite-state controllers based on Mealy machines for centralized and decentralized POMDPs.  In _AAAI_ , pages 1052–1058. AAAI Press, 2010.
  * Andriushchenko et al. [2021a] Roman Andriushchenko, Milan Češka, Sebastian Junges, and Joost-Pieter Katoen.  Inductive synthesis for probabilistic programs reaches new horizons.  In _TACAS_ , volume 12651 of _LNCS_ , pages 191–209. Springer, 2021a.
  * Andriushchenko et al. [2021b] Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, and Šimon Stupinskỳ.  PAYNT: a tool for inductive synthesis of probabilistic programs.  In _CAV_ , volume 12759 of _LNCS_ , pages 856–869. Springer, 2021b.
  * Baier and Katoen [2008] Christel Baier and Joost-Pieter Katoen.  _Principles of Model Checking_.  MIT Press, 2008.
  * Barbosa et al. [2022] Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli Ying Sheng, and Yoni Zohar.  CVC5: A versatile SMT-solver.  In _TACAS _(to appear)__ , 2022.
  * Bonet and Geffner [2009] Blai Bonet and Hector Geffner.  Solving POMDPs: RTDP-Bel vs. point-based algorithms.  In _IJCAI_ , pages 1641–1646, 2009.
  * Bonet et al. [2010] Blai Bonet, Hector Palacios, and Hector Geffner.  Automatic derivation of finite-state machines for behavior control.  In _AAAI_ , 2010.
  * Bork et al. [2020] Alexander Bork, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann.  Verification of indefinite-horizon POMDPs.  In _ATVA_ , volume 12302 of _LNCS_ , pages 288–304. Springer, 2020.
  * Bork et al. [2022] Alexander Bork, Joost-Pieter Katoen, and Tim Quatmann.  Under-approximating expected total rewards in POMDPs.  In _TACAS (to appear)_ , 2022.
  * Ceska et al. [2019] Milan Ceska, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen.  Shepherding hordes of Markov chains.  In _TACAS_ , volume 11428 of _LNCS_ , pages 172–190. Springer, 2019.
  * Ceska et al. [2021] Milan Ceska, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen.  Counterexample-guided inductive synthesis for probabilistic systems.  _Formal Aspects Comput._ , 33(4-5):637–667, 2021\.
  * Chatterjee et al. [2016] Krishnendu Chatterjee, Martin Chmelík, Raghav Gupta, and Ayush Kanodia.  Optimal cost almost-sure reachability in POMDPs.  _Artif. Intell._ , 234:26–48, 2016.
  * Cubuktepe et al. [2021] Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen, and Ufuk Topcu.  Robust finite-state controllers for uncertain POMDPs.  In _AAAI_ , pages 11792–11800. AAAI Press, 2021.
  * Dehnert et al. [2014] Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, and Joost-Pieter Katoen.  Fast debugging of PRISM models.  In _ATVA_ , volume 8837 of _LNCS_ , pages 146–162. Springer, 2014.
  * Dehnert et al. [2017] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk.  A Storm is coming: A modern probabilistic model checker.  In _CAV_ , volume 10427 of _LNCS_ , pages 592–600. Springer, 2017\.
  * Funke et al. [2020] Florian Funke, Simon Jantsch, and Christel Baier.  Farkas certificates and minimal witnesses for probabilistic reachability constraints.  In _TACAS_ , volume 12078 of _LNCS_ , pages 324–345. Springer, 2020.
  * Grześ et al. [2013] Marek Grześ, Pascal Poupart, and Jesse Hoey.  Isomorph-free branch and bound search for finite state controllers.  In _IJCAI_ , pages 2282–2290, 2013.
  * Hansen [1998] Eric A Hansen.  Solving POMDPs by searching in policy space.  In _UAI_ , pages 211–219, 1998.
  * Hauskrecht [1997] Milos Hauskrecht.  Incremental methods for computing bounds in partially observable Markov decision processes.  In _AAAI/IAAI_ , pages 734–739, 1997.
  * Inala et al. [2020] Jeevana Priya Inala, Osbert Bastani, Zenna Tavares, and Armando Solar-Lezama.  Synthesizing programmatic policies that inductively generalize.  In _ICLR_. OpenReview.net, 2020.
  * Jha and Seshia [2017] Susmit Jha and Sanjit A. Seshia.  A theory of formal synthesis via inductive learning.  _Acta Inf._ , 54(7):693–726, 2017.
  * Junges et al. [2018] Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, and Bernd Becker.  Finite-state controllers of POMDPs via parameter synthesis.  In _UAI_ , pages 519–529, 2018.
  * Junges et al. [2021] Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, and Tobias Winkler.  The complexity of reachability in parametric markov decision processes.  _J. Comput. Syst. Sci._ , 119:183–210, 2021.
  * Kaelbling et al. [1998] Leslie Pack Kaelbling, Michael L Littman, and Anthony R Cassandra.  Planning and acting in partially observable stochastic domains.  _Artif. Intell._ , 101(1-2):99–134, 1998.
  * Khonji et al. [2019] Majid Khonji, Ashkan Jasour, and Brian C Williams.  Approximability of constant-horizon constrained POMDP.  In _IJCAI_ , pages 5583–5590, 2019.
  * Kolobov et al. [2011] Andrey Kolobov, Mausam, Daniel S. Weld, and Hector Geffner.  Heuristic search for generalized stochastic shortest path MDPs.  In _ICAPS_. AAAI, 2011.
  * Kumar and Zilberstein [2015] Akshat Kumar and Shlomo Zilberstein.  History-based controller design and optimization for partially observable MDPs.  In _ICAPS_ , volume 25, pages 156–164, 2015.
  * Kwiatkowska et al. [2011] Marta Z. Kwiatkowska, Gethin Norman, and David Parker.  PRISM 4.0: Verification of probabilistic real-time systems.  In _CAV_ , volume 6806 of _LNCS_ , pages 585–591. Springer, 2011.
  * Nori et al. [2015] Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy.  Efficient synthesis of probabilistic programs.  In _PLDI_ , pages 208–217. ACM, 2015.
  * Norman et al. [2017] Gethin Norman, David Parker, and Xueyi Zou.  Verification and control of partially observable probabilistic systems.  _Real-Time Systems_ , 53(3):354–402, 2017.
  * Pineau et al. [2006] Joelle Pineau, Geoffrey J. Gordon, and Sebastian Thrun.  Anytime point-based approximations for large POMDPs.  _J. Artif. Intell. Res._ , 27:335–380, 2006.
  * Poupart et al. [2015] Pascal Poupart, Aarti Malhotra, Pei Pei, Kee-Eung Kim, Bongseok Goh, and Michael Bowling.  Approximate linear programming for constrained partially observable Markov decision processes.  In _AAAI_ , pages 3342–3348. AAAI Press, 2015.
  * Roijers et al. [2013] Diederik M Roijers, Peter Vamplew, Shimon Whiteson, and Richard Dazeley.  A survey of multi-objective sequential decision-making.  _J. Artif. Intell. Res._ , 48:67–113, 2013.
  * Silver and Veness [2010] David Silver and Joel Veness.  Monte-carlo planning in large POMDPs.  In _NIPS_ , pages 2164–2172. Curran Associates, Inc., 2010.
  * Smallwood and Sondik [1973] Richard D Smallwood and Edward J Sondik.  The optimal control of partially observable Markov processes over a finite horizon.  _Oper. Res._ , 21(5):1071–1088, 1973.
  * Soh and Demiris [2011] Harold Soh and Yiannis Demiris.  Evolving policies for multi-reward partially observable markov decision processes (MR-POMDPs).  In _GECCO_ , pages 713–720, 2011.
  * Solar-Lezama et al. [2006] Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat.  Combinatorial sketching for finite programs.  In _ASPLOS_ , pages 404–415. ACM, 2006.
  * Spaan and Vlassis [2005] Matthijs T. J. Spaan and Nikos A. Vlassis.  Perseus: Randomized point-based value iteration for POMDPs.  _J. Artif. Intell. Res._ , 24:195–220, 2005.
  * Verma et al. [2018] Abhinav Verma, Vijayaraghavan Murali, Rishabh Singh, Pushmeet Kohli, and Swarat Chaudhuri.  Programmatically interpretable reinforcement learning.  In _ICML_ , volume 80 of _PMLR_ , pages 5052–5061. PMLR, 2018.
  * Wang and Niepert [2019] Cheng Wang and Mathias Niepert.  State-regularized recurrent neural networks.  In _ICML_ , pages 6596–6606. PMLR, 2019.
  * Winterer et al. [2020] Leonore Winterer, Ralf Wimmer, Nils Jansen, and Bernd Becker.  Strengthening deterministic policies for POMDPs.  In _NFM_ , volume 12229 of _LNCS_ , pages 115–132. Springer, 2020.
  * Wray and Zilberstein [2015] Kyle Hollins Wray and Shlomo Zilberstein.  Multi-objective POMDPs with lexicographic reward preferences.  In _IJCAI_ , pages 3418–3424, 2015.
  * Wu et al. [2021] Bo Wu, Xiaobin Zhang, and Hai Lin.  Supervisor synthesis of POMDP via automata learning.  _Automatica_ , 129:109654, 2021.


11institutetext: Department of Computer Science, University of Copenhagen
11email<EMAIL_ADDRESS>
22institutetext: Department of Odontology, University of Copenhagen

# A Sequential Framework for Detection and Classification of Abnormal Teeth in
Panoramic X-rays

Tudor Dascalu 11 0000-0002-4942-1389 Shaqayeq Ramezanzade 22
0000-0002-1012-0730 Azam Bakhshandeh 22 0000-0003-2974-1331 Lars Bjørndal 22
0000-0002-2183-6400 Bulat Ibragimov 11 0000-0001-7739-7788

###### Abstract

This paper describes our solution for the Dental Enumeration and Diagnosis on
Panoramic X-rays Challenge at MICCAI 2023. Our approach consists of a multi-
step framework tailored to the task of detecting and classifying abnormal
teeth. The solution includes three sequential stages: dental instance
detection, healthy instance filtering, and abnormal instance classification.
In the first stage, we employed a Faster-RCNN model for detecting and
identifying teeth. In subsequent stages, we designed a model that merged the
encoding pathway of a pretrained U-net, optimized for dental lesion detection,
with the Vgg16 architecture. The resulting model was first used for filtering
out healthy teeth. Then, any identified abnormal teeth were categorized,
potentially falling into one or more of the following conditions: embedded,
periapical lesion, caries, deep caries. The model performing dental instance
detection achieved an AP score of 0.49. The model responsible for identifying
healthy teeth attained an F1 score of 0.71. Meanwhile, the model trained for
multi-label dental disease classification achieved an F1 score of 0.76. The
code is available at https://github.com/tudordascalu/2d-teeth-detection-
challenge.

###### Keywords:

Multi-label object detection Panoramic X-ray

##  1 Introduction

This article provides an overview of our solution submitted in the Dental
Enumeration and Diagnosis on Panoramic X-rays Challenge held at MICCAI 2023
[1].

##  2 Method

Figure 1: The multi-step pipeline employed for detecting abnormal teeth.
Initially, the Faster-RCNN (A) detects all teeth. Subsequently, a hybrid model
incorporating features from both U-net and Vgg16 architectures (B) filters out
healthy teeth. Finally, a model of the same architecture (B) classifies the
abnormal teeth.

We proposed a multi-step framework designed for the detection and
classification of abnormal teeth. This system consisted of three sequential
stages: detection of dental instances, filtering of healthy instances, and
classification of abnormal instances (Figure 1).

In the initial phase, we employed a Faster-RCNN to identify dental instances
from 2D panoramic X-rays, classifying them by quadrant and tooth number [2].
The model’s outputs were bounding boxes, each paired with a confidence score
and an encoded value representing the tooth and quadrant numbers.

In the following stages, we utilized a U-net model to segment both caries and
periapical lesions from cropped tooth images [3]. The model was trained to
minimize the mean of the Binary Cross Entropy loss and Dice loss. The encoding
path of the trained U-net was integrated into the models used for (2)
filtering out healthy instances and (3) distinguishing abnormal instances.
These models presented a unified architecture, combining the U-net’s encoding
path with the Vgg16’s feature extraction path [4]. Subsequently, the
classification path of the Vgg16 classifier was adapted to handle the combined
feature set sourced from both the U-net and Vgg16. The objective function used
for training the models was the Binary Cross Entropy. The model designed to
differentiate between healthy and abnormal teeth required cropped teeth images
as input. It produced a binary label indicating the presence or absence of
abnormalities. Teeth identified as abnormal were then processed by another
model focused on their classification. This classification model was trained
for multi-label categorization to accommodate teeth with multiple conditions.

##  3 Experiment and results

###  3.1 Data

The dataset used in the present work was introduced in the Dental Enumeration
and Diagnosis on Panoramic X-rays Challenge. We leveraged a subset of 1039
Panoramic X-rays, with 634 X-rays associated with bonding boxes, teeth
numbers, quadrant numbers corresponding to all the teeth, and 705 X-rays
associated with bounding boxes, teeth numbers, quadrant numbers, disease type
corresponding to abnormal teeth. The images were subjected to on-the-fly
augmentation techniques such as horizontal flipping, brightness and contrast
modifications, affine transformations, and random cutouts with dimensions
reaching up to 80x80 pixels.

###  3.2 Results

In this section, the metrics presented include Average Precision at varying
IoU thresholds for object detection and the F1 score for classification tasks.
The results of our experiment are presented in Table 1. The Faster-RCNN model
achieved an AP score of 0.49. The model differentiating healthy from unhealthy
teeth obtained an F1 score of 0.71, while the classifier for abnormal teeth
registered an F1 score of 0.76.

Table 1: The performance of the models performing (1) teeth detection and numbering, (2) healthy teeth classification, and (3) abnormal teeth classification. Model | AP | AP75 | AP50 | F1
---|---|---|---|---
Teeth detection and numbering | 0.49 | 0.46 | 0.91 | -
Healthy teeth filtering | - | - | - | 0.71
Abnormal teeth classification | - | - | - | 0.76

## References

  * [1] Hamamci, I.E., Er, S., Simsar, E., Yuksel, A.E., Gultekin, S., Ozdemir, S.D., Yang, K., Li, H.B., Pati, S., Stadlinger, B., Mehl, A., Gundogar, M., Menze, B.: DENTEX: An Abnormal Tooth Detection with Dental Enumeration and Diagnosis Benchmark for Panoramic X-rays (May 2023). https://doi.org/10.48550/arXiv.2305.19112, http://arxiv.org/abs/2305.19112, arXiv:2305.19112 [cs]
  * [2] Ren, S., He, K., Girshick, R., Sun, J.: Faster R-CNN: Towards Real-Time Object Detection with Region Proposal Networks (Jan 2016), http://arxiv.org/abs/1506.01497, arXiv:1506.01497 [cs]
  * [3] Ronneberger, O., Fischer, P., Brox, T.: U-Net: Convolutional Networks for Biomedical Image Segmentation. In: Navab, N., Hornegger, J., Wells, W.M., Frangi, A.F. (eds.) Medical Image Computing and Computer-Assisted Intervention – MICCAI 2015. pp. 234–241. Lecture Notes in Computer Science, Springer International Publishing, Cham (2015)
  * [4] Simonyan, K., Zisserman, A.: Very Deep Convolutional Networks for Large-Scale Image Recognition. arXiv:1409.1556 [cs] (Apr 2015), http://arxiv.org/abs/1409.1556, arXiv: 1409.1556