11institutetext: University of California, Berkeley, USA††thanks: This work is
partially supported by NSF grants 1545126 (VeHICaL), 1646208 and 1837132, by
the DARPA contracts FA8750-18-C-0101 (AA) and FA8750-20-C-0156 (SDCPS), by
Berkeley Deep Drive, and by Toyota under the iCyPhy center.

# Runtime Monitors for Markov Decision Processes

Sebastian Junges Hazem Torfah Sanjit A. Seshia

###### Abstract

We investigate the problem of monitoring partially observable systems with
nondeterministic and probabilistic dynamics. In such systems, every state may
be associated with a risk, e.g., the probability of an imminent crash. During
runtime, we obtain partial information about the system state in form of
observations. The monitor uses this information to estimate the risk of the
(unobservable) current system state. Our results are threefold. First, we show
that extensions of state estimation approaches do not scale due the
combination of nondeterminism and probabilities. While exploiting a geometric
interpretation of the state estimates improves the practical runtime, this
cannot prevent an exponential memory blowup. Second, we present a tractable
algorithm based on model checking conditional reachability probabilities.
Third, we provide prototypical implementations and manifest the applicability
of our algorithms to a range of benchmarks. The results highlight the
possibilities and boundaries of our novel algorithms.

##  1 Introduction

Runtime assurance is essential in deployment of safety-critical (cyber-
physical) systems [44, 12, 29, 48]. Monitors observe system behavior and
indicate when the system is at risk to violate system specifications. A
critical aspect in developing reliable monitors is their ability to handle
noisy or missing data. In cyber-physical systems, monitors observe the system
state via sensors, i.e., sensors are an interface between the system and the
monitor. A monitor has to base its decision solely on the obtained sensor
output. These sensors are not perfect, and not every aspect of a system state
can be measured.

This paper considers a model-based approach to the construction of monitors
for systems with imprecise sensors. Consider Fig. 1(b). We assume a model for
the environment together with the controller. Typically, such a model contains
both nondeterministic and probabilistic behavior, and thus describes a Markov
decision process (MDP): In particular, the sensor is a stochastic process [54]
that translates the environment state into an observation. For example, this
could be a perception module on a plane that during landing estimates the
movements of an on-ground vehicle, as depicted in Fig. 1(a). Due to lack of
precise data, the vehicle movements itself may be most accurately described
using nondeterminism.

We are interested in the associated _state risk_ of the current system state.
The state risk may encode, e.g., the probability that the plane will crash
with the vehicle within a given number of steps, or the expected time until
reaching the other side of the runway. The challenge is that the monitor
cannot directly observe the current system state. Instead, the monitor must
infer from a trace of observations the current state risk. This cannot be done
perfectly as the system state cannot be inferred precisely. Rather, we want a
sound, conservative estimate of the system state. More concretely, for a fixed
resolution of the nondeterminism, the _trace risk_ is the weighted sum over
the probability of being in a state having observed the trace, times the risk
imposed by this state. The monitoring problem is to decide whether for any
possible scheduler resolving the nondeterminism the trace risk of a given
trace exceeds a threshold.

Monitoring of systems that contain either only probabilistic or only
nondeterministic behavior is typically based on _filtering_. Intuitively, the
monitor then estimates the current system states based on the model. For
purely nondeterministic systems (without probabilities) a set of states needs
to be tracked, and purely probabilistic systems (without nondeterminism)
require tracking a distribution over states. This tracking is rather
efficient. For systems that contain both probabilistic and nondeterministic
behavior, filtering is more challenging. In particular, we show that filtering
on MDPs results in an exponential memory blowup as the monitor must track sets
of distributions. We show that a reduction based on the geometric
interpretation of these distributions is essential for practical performance,
but cannot avoid the worst-case exponential blowup. As a tractable alternative
to filtering, we rephrase the monitoring problem as the computation of
conditional reachability probabilities [9]. More precisely, we unroll and
transform the given MDP, and then model check this MDP. This alternative
approach yields a polynomial-time algorithm. Indeed, our experiments show the
feasibility of computing the risk by computing conditional probabilities. We
also show benchmarks on which filtering is a competitive option.

#### Contribution and outline.

This paper presents the first runtime monitoring for systems that can be
adequately abstracted by a combination of _probabilities and nondeterminism_
and where the system state is _partially observable_. We describe the use
case, show that typical filtering approaches in general fail to deal with this
setting, and show that a tractable alternative solution exists. In Sec. 3, we
investigate _forward filtering_ , used to estimate the possible system states
in partially observable settings. We show that this approach is tractable for
systems that have probabilistic _or_ nondeterministic uncertainty, but not for
systems that have both. To alleviate the blowup, Sec. 4 discusses an (often)
efficacious pruning strategy and its limitations. In Sec. 5 we consider model
checking as a more tractable alternative. This result utilises constructions
from the analysis of _partially observable MDPs_ and model checking MDPs with
_conditional properties_. In Sec. 6 we present baseline implementations of
these algorithms, on top of the open-source model checker Storm, and evaluate
their performance. The results show that the implementation allows for
monitoring of a variety of MDPs, and reveals both strengths and weaknesses of
both algorithms. We start with a motivating example and review related work at
the end of the paper.

#### Motivating example.

Consider a scenario where an autonomous airplane is in its final approach,
i.e., lined up with a designated runway and descending for landing, see Figure
1(a). On the ground, close to the runway, maintenance vehicles may cross the
runway. The airplane tracks the movements of these vehicles and has to decide,
depending on the movements of the vehicles, whether to abort the landing. To
simplify matters, assume that the airplane (P) is tracking the movement of one
vehicle (V) that is about to cross the runway. Let us further assume that P
tracks V using a perception module that can only determine the position of the
vehicle with a certain accuracy [33], i.e., for every position of V, the
perception module reports a noisy variant of the position of V. However, it is
important to realize that the plane obtains a sequence of these measurements.

(a) Landing plane scenario

EnvironmentControllerSensorsMonitorRisk($s$) $\geq\lambda$?$s\in
S_{\mathcal{E}}$$z\in\mathsf{Z}$_Vehicle_ _Plane_ _Perception_ World

(b) Sensor-based Monitors

$\langle M,D_{2}\rangle$$\langle R,D_{2}\rangle$$\langle L,D_{2}\rangle$
$\bullet$ $\bullet$ $\bullet$$\bullet$$\langle M,D_{1}\rangle$$\langle
R,D_{1}\rangle$$\langle L,D_{1}\rangle$ $\bullet$ $\bullet$$\bullet$$\langle
M,D_{0}\rangle$$\langle R,D_{0}\rangle$$\langle
L,D_{0}\rangle$$\\{w\\}$$\emptyset$$\frac{1}{20}$$\frac{19}{20}$$\\{p\\}$$\\{p,w\\}$$\frac{1}{2}$$\frac{1}{2}$$\emptyset$$\frac{1}{2}$$\frac{1}{2}$$\\{p\\}$$\frac{1}{10}$$\frac{9}{10}$$\emptyset$$\\{p\\}$$\\{w\\}$$\emptyset$$\frac{1}{2}$$\frac{1}{2}$$\\{p\\}$$\\{p,w\\}$$\frac{99}{100}$$\frac{1}{100}$$\emptyset$$\\{p\\}$$\frac{1}{100}$$\frac{99}{100}$$\emptyset$$\\{p\\}$∗∗∗

(c) World Model

$\mathit{sense}$$\langle
R,D_{2}\rangle/[M_{o}\colon\frac{1}{2},R_{o}\colon\frac{1}{2}]$$\langle
M,D_{0}\rangle/[L_{o}\colon\frac{1}{100},M_{o}\colon\frac{98}{100},R_{o}\colon\frac{1}{100}]$$\langle
R,D_{1}\rangle/[M_{o}\colon\frac{1}{3},R_{o}\colon\frac{2}{3}]$$\langle
R,D_{0}\rangle/[M_{o}\colon\frac{1}{20},R_{o}\colon\frac{19}{20}]$$\langle
M,D_{1}\rangle/[L_{o}\colon\frac{1}{8},M_{o}\colon\frac{3}{4},R_{o}\colon\frac{1}{8}]$$\langle
L,D_{0}\rangle/[L_{o}\colon\frac{19}{20},M_{o}\colon\frac{1}{20}]$

(d) Partial Sensor Model

Figure 1: A probabilistic world and sensor model represented by two MDPs for
the scenario of an airplane in landing approach with on-ground vehicle
movements.

Figure 1 illustrates the dynamics of the scenario. The world model describing
the movements of V and P is given in Figure 1(c), where $D_{2},D_{1}$, and
$D_{0}$ define how close P is to the runway, and $R$, $M$, and $L$ define the
position of V. Depending on what information V perceives about P, given by the
atomic proposition $\\{(p)\textit{rogress}\\}$, and what commands it receives
$\\{(w)\textit{ait}\\}$, it may or may not cross the runway. The perception
module receives the information about the state of the world and reports with
a certain accuracy (given as a probability) the position of V. The (simple)
model of the perception module is given in Figure 1(d). For example, if P is
in zone $D_{2}$ and V is in $R$ then there is high chance that the perception
module returns that V is on the runway. The probability of incorrectly
detecting V’s position reduces significantly when P is in $D_{0}$.

A monitor responsible for making the decision to land or to perform a go-
around based on the information computed by the perception module, must take
into consideration the accuracy of this returned information. For example, if
the sequence of sensor readings passed to the monitor is the sequence
$\tau=R_{o}\cdot R_{o}\cdot M_{o}$, and each state is mapped to a certain
risk, then how risky is it to land after seeing $\tau$? For example, if with
high probability the world is in state $\langle M,D_{0}\rangle$, a very risky
state, then the plane should go around. In the paper, we address the question
of computing the risk based on this observation sequence. We will use this
example as our running example.

##  2 Monitoring under Imprecise Sensors

In this section, we formalize the problem of monitoring with imprecise sensors
when both the world and sensor models are given by MDPs. We start with a recap
of MDPs, define the monitoring problem for MDPs, and finally show how the
dynamics of the system under inspection can be modeled by an MDP defined by
the composition of two MDPs of the sensors and world model of the system.

####  2.0.1 Markov decision processes.

For a countable set $X$, let $\mathsf{Distr}(X)\subset(X\rightarrow[0,1])$
define all distributions over $X$, i.e., for $d\in\mathsf{Distr}(X)$ it holds
that $\Sigma_{x\in X}d(x)=1$. For $\mu\in\mathsf{Distr}(X)$, let the _support_
of $\mu$ be defined by $\mathsf{supp}(\mu)\colonequals\\{x\mid\mu(x)>0\\}$. We
call a distribution $\mu$ _Dirac_ , if $|\mathsf{supp}(\mu)|=1$.

######  Definition 1 (Markov decision process)

A _Markov decision process_ is a tuple $\mathcal{M}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, where $S$ is a finite
set of _states_ , $\iota\in\mathsf{Distr}(S)$ is an _initial distribution_ ,
$\mathsf{Act}$ is a finite set of _actions_ , $P\colon
S\times\mathsf{Act}\rightarrow\mathsf{Distr}(S)$ is a _partial transition
function_ , $\mathsf{Z}$ is a finite set of _observations_ , and
$\mathsf{obs}\colon S\rightarrow\mathsf{Distr}({\mathsf{Z}})$ is a
_observation function_.

###### Remark 1

The observation function can also be defined as a state-action observation
function $\mathsf{obs}\colon
S\times\mathsf{Act}\rightarrow\mathsf{Distr}(\mathsf{Z})$. MDPs with state-
action observation function can be easily transformed into equivalent MDPs
with a state observation function using auxiliary states [19]. Throughout the
paper we use state-action observations to keep (sensor) models concise.

We denote $\mathsf{AvAct}(s)=\\{\alpha\mid P(s,\alpha)\neq\bot\\}$. W.l.o.g.,
$|\mathsf{AvAct}(s)|\geq 1$. If all distributions in $\mathcal{M}$ are Dirac,
we refer to $\mathcal{M}$ as a _Kripke structure_ ($\mathsf{KS}$). If
$|\mathsf{AvAct}(s)|=1$ for all $s\in S$, we refer to $\mathcal{M}$ as a
_Markov chain_ ($\mathsf{MC}$). When $\mathsf{Z}=S$, we refer to $\mathcal{M}$
as _fully observable_ and omit $\mathsf{Z}$ and $\mathsf{obs}$ from its
definition. A _finite path_ in an MDP $\mathcal{M}$ is a sequence
$\pi=s_{0}a_{0}s_{1}\dots s_{n}\in S\times\big{(}\mathsf{Act}\times
S\big{)}^{*}$ such that for every $0\leq i<n$ it holds that
$P(s_{i},a_{i})(s_{i+1})>0$ and $\iota(s_{0})>0$. We denote the set of finite
paths of $\mathcal{M}$ by $\Pi_{\mathcal{M}}$. The _length_ of the path is
given by the number of actions along the path. The set $\Pi_{\mathcal{M}}^{n}$
for some $n\in\mathbb{N}$ denotes the set of finite paths of length $n$. We
use ${\pi}_{\downarrow}$ to denote the last state in $\pi$. We omit
$\mathcal{M}$ whenever it is clear from the context. A _trace_ is a sequence
of observations $\tau=z_{0}\ldots z_{n}\in\mathsf{Z}^{+}$. Every path induces
a distribution over traces. As standard, we need resolve any nondeterminism by
means of a scheduler.

######  Definition 2 (Scheduler)

A _scheduler_ for MDP $\mathcal{M}$ is a function
$\sigma\colon\Pi_{\mathcal{M}}\rightarrow\mathsf{Distr}(\mathsf{Act})$ with
$\mathsf{supp}(\sigma(\pi))\subseteq\mathsf{AvAct}({\pi}_{\downarrow})$ for
every $\pi\in\Pi_{\mathcal{M}}$.

We use $\textit{Sched}(\mathcal{M})$ to denote the set of schedulers. For a
fixed scheduler $\sigma\in\textit{Sched}(\mathcal{M})$, the probability
$\mathsf{Pr}_{\sigma}(\pi)$ of a path $\pi$ (under the scheduler $\sigma$) is
the product of the transition probabilities in the induced Markov chain. For
more details we refer the reader to [8].

####  2.0.2 Formal Problem Statement.

Our goal is to determine the risk that the system is exposed to having
observed a trace $\tau\in\mathsf{Z}^{+}$. Let $r\colon
S\rightarrow\mathbb{R}_{\geq 0}$ map states in $\mathcal{M}$ to some risk in
$\mathbb{R}_{\geq 0}$. We call $r$ a _state-risk function_ for $\mathcal{M}$.
This function maps to the risk that is associated with being in every state.
For example, in our experiments, we flexibly define the state risk using the
(expected reward extension of the) temporal logic PCTL [8], to define the
probability of reaching a fail state. E.g., we can define risk as the
probability to crash within $H$ steps. The use of expected rewards allows for
even more flexible definitions.

Intuitively, to compute this risk of the system we need to determine the
current system state having observed $\tau$ considering the probabilistic and
nondeterministic context. Towards this, we formalize the (conditional)
probabilities and risks of paths and traces. Let
$\mathsf{Pr}_{\sigma}(\pi\mid\tau)$ define the probability of a path $\pi$,
under a scheduler $\sigma$, having observed $\tau$. Since a scheduler may
define many paths that induce the observation trace $\tau$, we are interested
in the weighted risk over all paths, i.e.,
$\sum_{\pi\in\Pi_{\mathcal{M}}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow})$. The monitoring problem for MDPs then conservatively
over-approximate the risk of a trace by assuming an adversarial scheduler,
that is, by taking the supremum risk estimate over all schedulers111We later
see in Lemma 8 that this is indeed a maximum..

The Monitoring Problem. Given an MDP $\mathcal{M}$, a state-risk $r\colon
S\rightarrow\mathbb{R}_{\geq 0}$, an observation trace
$\tau\in\mathsf{Z}^{+}$, and a threshold $\lambda\in[0,\infty)$, decide
$R_{r}(\tau)>\lambda$, where the _weighted risk function_
$R_{r}\colon\mathsf{Z}^{+}\rightarrow\mathbb{R}_{\geq 0}$ is defined as
$R_{r}(\tau)\quad\colonequals\quad\sup_{\sigma\in\textit{Sched}(\mathcal{M})}\sum_{\pi\in\Pi_{\mathcal{M}}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow}).$

The conditional probability $\mathsf{Pr}_{\sigma}(\pi\mid\tau)$ can be
characterized using Bayes’ rule222for conciseness we assume throughout the
paper that $\frac{0}{0}=0$:

$\mathsf{Pr}_{\sigma}(\pi\mid\tau)=\frac{\mathsf{Pr}(\tau\mid\pi)\cdot\mathsf{Pr}_{\sigma}(\pi)}{\mathsf{Pr}_{\sigma}(\tau)}.$

The probability $\mathsf{Pr}(\tau\mid\pi)$ of a trace $\tau$ for a fixed path
$\pi$ is $\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)$, where

$\mathsf{obs}_{\mathsf{tr}}(s)\colonequals\mathsf{obs}(s),\quad\mathsf{obs}_{\mathsf{tr}}(\pi\alpha
s^{\prime})\colonequals\\{\tau\cdot
z\mapsto\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)\cdot\mathsf{obs}(s^{\prime})(z)\\},$

when $|\pi|=|\tau|$, and $\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)=0$ otherwise.
The probability $\mathsf{Pr}_{\sigma}(\tau)$ of a trace $\tau$ is
$\sum_{\pi}\mathsf{Pr}_{\sigma}(\pi)\cdot\mathsf{Pr}(\tau\mid\pi)$.

We call the special variant with $\lambda=0$ the _qualitative monitoring
problem_. The problems are (almost) equivalent on Kripke structures, where
considering a single path to an adequate state suffices. Details are given in
the appendix.

###### Lemma 1

For Kripke structures the monitoring and qualitative monitoring problems are
logspace interreducible.

In the next sections we present two types of algorithms for the monitoring
problem. The first algorithm is based on the widespread (forward) filtering
approach [43]. The second is new algorithm based on model checking conditional
probabilities. While filtering approaches are efficacious in a purely
nondeterministic or a purely probabilistic setting, it does not scale on
models such as MDPs that are both probabilistic and nondeterministic. In those
models, model checking provides a tractable alternative. However, we first
connect the problem statement more formally to our motivating example.

####  2.0.3 An MDP defining the system dynamics.

Before we solve the monitoring problem for MDPs, we show how the weighted risk
for a system given by a world and sensor model can be formalized as a
monitoring problem for MDPs. To this end, we define the dynamics of the world
and sensors that we use as basis for our monitor as the following joint MDP.

For a fully observable world MDP $\mathcal{E}=\langle
S_{\mathcal{E}},\iota_{\mathcal{E}},\mathsf{Act}_{\mathcal{E}},P_{\mathcal{E}}\rangle$
and a sensor MDP $\mathcal{S}=\langle
S_{\mathcal{S}},\iota_{\mathcal{S}},S_{\mathcal{E}},P_{\mathcal{S}},\mathsf{Z},\mathsf{obs}\rangle$,
where $\mathsf{obs}$ is state-action based, the _inspected system_ is defined
by an MDP $\llbracket\langle\mathcal{E},\mathcal{S}\rangle\rrbracket=\langle
S_{\mathcal{J}},\iota_{\mathcal{J}},\mathsf{Act}_{\mathcal{E}},P_{\mathcal{J}},\mathsf{Z},\mathsf{obs}_{\mathcal{J}}\rangle$
being the synchronous composition of $\mathcal{E}$ and $\mathcal{S}$:

  * •

$S_{\mathcal{J}}\colonequals S_{\mathcal{E}}\times S_{\mathcal{S}}$,

  * •

$\iota_{\mathcal{J}}$ is defined as $\iota_{\mathcal{J}}(\langle
u,s\rangle)\colonequals\iota_{\mathcal{E}}(u)\cdot\iota_{\mathcal{S}}(s)$ for
each $u\in S_{\mathcal{E}}$ and $s\in S_{\mathcal{S}}$,

  * •

$P_{\mathcal{J}}\colon
S_{\mathcal{J}}\times\mathsf{Act}_{\mathcal{E}}\rightarrow\mathsf{Distr}(S_{\mathcal{J}})$
such that for all $\langle u,s\rangle\in S_{\mathcal{J}}$ and
$\alpha\in\mathsf{Act}_{\mathcal{E}}$;

$P_{\mathcal{J}}(\langle
u,s\rangle,\alpha)=d_{u,s}\in\mathsf{Distr}(S_{\mathcal{J}}),$

where for all $u^{\prime}\in S_{\mathcal{E}}$ and $s^{\prime}\in
S_{\mathcal{S}}$: $d_{u,s}(\langle
u^{\prime},s^{\prime}\rangle)=P_{\mathcal{E}}(u,\alpha)(u^{\prime})\cdot
P_{\mathcal{S}}(s,u)(s^{\prime})$,

  * •

$\mathsf{obs}_{\mathcal{J}}\colon
S_{\mathcal{J}}\rightarrow\mathsf{Distr}(\mathsf{Z})$ with
$\mathsf{obs}_{\mathcal{J}}\colon\langle u,s\rangle\mapsto\mathsf{obs}(s,u)$.

$\langle R,D_{2}\rangle$$\mathcal{E}:$$\langle R,D_{1}\rangle$$\langle
M,D_{1}\rangle$$\langle M,D_{0}\rangle$$\langle
L,D_{0}\rangle$$\mathit{sense}$$\mathcal{S}:$$\mathit{sense}$$\mathit{sense}$$\mathit{sense}$$\mathit{sense}$$M_{o}:\frac{1}{2}$$R_{o}:\frac{1}{2}$$M_{o}:\frac{1}{3}$$R_{o}:\frac{2}{3}$$L_{o}:\frac{1}{8}$$M_{o}:\frac{3}{4}$$R_{o}:\frac{1}{8}$$L_{o}:\frac{1}{100}$$M_{o}:\frac{98}{100}$$R_{o}:\frac{1}{100}$$L_{o}:\frac{19}{20}$$M_{o}:\frac{1}{20}$$\\{p\\}$$\emptyset$$\\{p\\}$$\\{p\\}$$\langle
R,D_{2}\rangle$$\langle R,D_{1}\rangle$$\langle M,D_{1}\rangle$$\langle
M,D_{0}\rangle$$\langle L,D_{0}\rangle$$\mathsf{obs}_{\mathcal{J}}:$

Figure 2: A run with its observations of the inspected system
$\llbracket\langle\mathcal{E},\mathcal{S}\rangle\rrbracket$ where
$\mathcal{E}$ and $\mathcal{S}$ are the models given in Figure 1.

In Figure 2 we illustrate a run of
$\llbracket\langle\mathcal{E},\mathcal{S}\rangle\rrbracket$ for the world and
sensor MDPs presented in Figure 1. We particularly show the observations of
the joint MDP given by the distributions over the observations for each
transition in the run (we omitted the probabilistic transitions for
simplicity). The observations of the MDP $\mathcal{M}$ present the output of
the sensor upon a path through $\mathcal{M}$. These observations in turn are
the inputs to a monitor on top of the system. The role of the monitor is then
to compute the risk of being in a critical state based on the previously
received observations.

##  3 Forward Filtering for State Estimation

We start by showing why standard forward filtering does not scale well on
MDPs. We briefly show how filtering can be used to solve the monitoring
problem for purely nondeterministic systems (Kripke structures) or purely
probabilistic systems (Markov Chains). Then, we show why for MDPs, the forward
filtering needs to manage, although finite but an exponential set of
distributions. In Section 4 we present a new improved variant of forward
filtering for MDPs based on filtering with vertices of the convex hull. In
Section 5 we present a new polynomial-time model checking-based algorithm for
solving the problem.

###  3.1 State estimators for Kripke structures.

For Kripke structures, we maintain a set of possible states that agree with
the observed trace. This set of states is inductively characterized by the
function $\mathsf{est_{\mathsf{KS}}}\colon\mathsf{Z}^{+}\rightarrow 2^{S}$
which we define formally below. For an observation trace $\tau$,
$\mathsf{est_{\mathsf{KS}}}(\tau)$ defines the set of states that can be
reached with positive probability. This set can be computed by a forward state
traversal [31]. To illustrate how $\mathsf{est_{\mathsf{KS}}}(\tau)$ is
computed for $\tau$, consider the underlying Kripke structure of the inspected
system $\llbracket\langle\mathcal{E},\mathcal{S}\rangle\rrbracket$ for our
running example in Figure 1 (to make this a Kripke structure, we remove the
probabilities). Consider further the observation trace $\tau=R_{o}\cdot
M_{o}\cdot L_{o}$. Since
$\llbracket\langle\mathcal{E},\mathcal{S}\rangle\rrbracket$ has only one
initial state $\langle\langle R,D_{2}\rangle,\mathit{sense}\rangle$ and
$R_{o}$ is observable with a positive probability in this state,
$\mathsf{est_{\mathsf{KS}}}(R_{o})=\\{\langle\langle
R,D_{2}\rangle,\mathit{sense}\rangle\\}$. As $M_{o}$ is observed next,
$\mathsf{est_{\mathsf{KS}}}(R_{o}\cdot M_{o})$ computes the states reached
from $\langle\langle R,D_{2}\rangle,\mathit{sense}\rangle$ and where $M_{o}$
can be observed with a positive probability, i.e.,
$\mathsf{est_{\mathsf{KS}}}(R_{o}M_{o})=\\{\langle\langle
R,D_{1}\rangle,\mathit{sense}\rangle,\langle\langle
R,M_{1}\rangle,\mathit{sense}\rangle\\}$. Finally the current state having
observed $R_{o}\cdot M_{o}\cdot L_{o}$ may be one of the the states
$\mathsf{est_{\mathsf{KS}}}(\tau)=\\{\langle\langle
M,D_{1}\rangle,\mathit{sense}\rangle$, $\langle\langle
L,D_{1}\rangle,\mathit{sense}\rangle$, $\langle\langle
L,D_{0}\rangle,\mathit{sense}\rangle$, $\langle\langle
M,D_{0}\rangle,\mathit{sense}\rangle\\}$, which especially shows that we might
be in the high-risk world state $\langle M,D_{0}\rangle$.

######  Definition 3 ($\mathsf{KS}$ state estimator)

For $\mathsf{KS}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, the state estimation
function $\mathsf{est_{\mathsf{KS}}}\colon\mathsf{Z}^{+}\rightarrow 2^{S}$ is
defined as

$\displaystyle\mathsf{est_{\mathsf{KS}}}(z)\colonequals\\{s\in
S\mid\iota(s)>0\wedge\mathsf{obs}(s)(z)>0\\}$
$\displaystyle\mathsf{est_{\mathsf{KS}}}(\tau\cdot
z)\colonequals\Big{\\{}s^{\prime}\in S\mid\exists
s\in\mathsf{est_{\mathsf{KS}}}(\tau),\exists\alpha\in\mathsf{Act},P(s,\alpha)(s^{\prime})>0\wedge\mathsf{obs}(s^{\prime})(z)>0\Big{\\}}.$

For a Kripke structure $\mathsf{KS}$ and a given trace $\tau$, the monitoring
problem can be solved by computing $\mathsf{est_{\mathsf{KS}}}(\tau)$, using
[31] and Lemma 1.

###### Lemma 2

For a Kripke stucture $\mathsf{KS}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, a trace
$\tau\in\mathsf{Z}^{+}$, and a state-risk function $r\colon
S\rightarrow\mathbb{R}_{\geq 0}$, it holds that
$R_{r}(\tau)=\max\limits_{s\in\mathsf{est_{\mathsf{KS}}}(\tau)}r(s)$.
Computing $R_{r}(\tau)$ requires time $\mathcal{O}(|\tau|\cdot|P|)$ and space
$\mathcal{O}(|S|)$.

A more detailed proof can be found in the appendix.

The time and space requirements follow directly from the inductive definition
of $\mathsf{est_{\mathsf{KS}}}$ which resembles solving a forward state
traversal problem in automata [31]. In particular, the algorithm allows
updating the result after extending $\tau$ in $\mathcal{O}(|P|)$.

###  3.2 State estimators for Markov chains.

For Markov chains, in addition to tracking the potential reachable system
states, we also need to take the transition probabilities into account. When a
system is (observation-)deterministic, we can adapt the notion of beliefs,
similar to RVSE [52], and similar to the construction of belief MDPs for
_partially observable MDPs_ , cf. [51]:

######  Definition 4 (Belief)

For an MDP $\mathcal{M}$ with a set of states $S$, a belief $\mathsf{bel}$ is
a distribution in $\mathsf{Distr}(S)$.

In the remainder of the paper, we will denote the function
$S\rightarrow\\{0\\}$ by $\mathbf{0}$ and the set
$\mathsf{Distr}(S)\cup\\{\mathbf{0}\\}$ by $\mathsf{Bel}$. A state estimator
based on $\mathsf{Bel}$ is then defined as follows [49, 55, 52]333For the
deterministic case, we omit the unique action for brevity:

######  Definition 5 (MC state estimator)

For $\mathsf{MC}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, a trace
$\tau\in\mathsf{Z}^{+}$ the state estimation function
$\mathsf{est_{\mathsf{MC}}}\colon\mathsf{Z}^{+}\rightarrow\mathsf{Bel}$ is
defined as

$\displaystyle\mathsf{est_{\mathsf{MC}}}(z)$
$\displaystyle\colonequals\begin{cases}\big{\\{}s\mapsto\frac{\iota(s)\cdot\mathsf{obs}(s)(z)}{\sum\limits_{\hat{s}\in
S}\iota(\hat{s})\cdot\mathsf{obs}(\hat{s})(z)}\big{\\}}&\exists s\in
S.\leavevmode\nobreak\ \iota(s)\cdot\mathsf{obs}(z)>0,\\\
\mathbf{0}&\text{otherwise}.\end{cases}$
$\displaystyle\mathsf{est_{\mathsf{MC}}}(\tau\cdot z)$
$\displaystyle\colonequals\left\\{s^{\prime}\mapsto\frac{\sum\limits_{s\in
S}\mathsf{est_{\mathsf{MC}}}(\tau)(s)\cdot
P(s,s^{\prime})\cdot\mathsf{obs}(s^{\prime})(z)}{\sum\limits_{s\in
S}\mathsf{est_{\mathsf{MC}}}(\tau)(s)\cdot\big{(}\sum\limits_{\hat{s}\in
S}P(s,\hat{s})\cdot\mathsf{obs}(\hat{s})(z)\big{)}}\right\\}$

To illustrate how $\mathsf{est_{\mathsf{MC}}}$ is computed, consider again our
system in Figure 1 and assume that the MDP has only the actions labeled with
$\\{p\\}$ (reducing it to the Markov chain induced by the a scheduler that
only performs the $\\{p\\}$ actions). Again we consider the observation trace
$\tau=R_{o}\cdot M_{o}\cdot L_{o}$ and compute
$\mathsf{est_{\mathsf{MC}}}{\tau}$. For the first observation $R_{o}$, and
since there is only one initial state, it follows that
$\mathsf{est_{\mathsf{MC}}}(R_{o})=\\{\langle R,D_{2}\rangle\mapsto 1\\}$444We
omit the (single) sensor state for conciseness.. From $\langle R,D_{2}\rangle$
and having observed $M_{o}$ we can reach the states $\langle R,D_{1}\rangle$
and $\langle M,D_{1}\rangle$ with probabilities
$\mathsf{est_{\mathsf{MC}}}(R_{o}\cdot M_{o})=\\{\langle
R,D_{1}\rangle\mapsto\frac{\frac{1}{2}\cdot\frac{1}{3}}{\frac{1}{2}\cdot\frac{1}{3}+\frac{1}{2}\cdot\frac{3}{4}}=\frac{4}{13},\langle
M,D_{1}\rangle\mapsto\frac{\frac{1}{2}\cdot\frac{3}{4}}{\frac{1}{2}\cdot\frac{1}{3}+\frac{1}{2}\cdot\frac{3}{4}}=\frac{9}{13}\\}$.
Finally, from the later two states, when observing $L_{o}$, the states
$\langle M,D_{0}\rangle$ and $\langle L,D_{0}\rangle$ can be reached with
probabilities $\mathsf{est_{\mathsf{MC}}}(R_{o}\cdot M_{o}\cdot
L_{o})=\\{\langle M,D_{0}\rangle\mapsto 0.0001,\langle L,D_{0}\rangle\mapsto
0.999\\}$. Notice that although the state $\langle R,D_{0}\rangle$ can be
reached from $\langle R,D_{1}\rangle$, the probability of being in this state
is 0 since observing $L_{o}$ in this state is $\mathsf{obs}(\langle
R,D_{0}\rangle)(L_{o})=0$.

###### Lemma 3

For a Markov chain $\mathsf{MC}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, a trace
$\tau\in\mathsf{Z}^{+}$, and a state-risk function $r\colon
S\rightarrow\mathbb{R}_{\geq 0}$, it holds that $R_{r}(\tau)=\sum_{s\in
S}\mathsf{est_{\mathsf{MC}}}(\tau)(s)\cdot r(s).$ Computing $R_{r}(\tau)$ can
be done in time $\mathcal{O}(|\tau|\cdot|S|\cdot|P|)$ , and using $|S|$ many
rational numbers. The size of the rationals555To avoid growth, one may use
fixed-precision numbers that over-approximate the probability of being in any
state—inducing a growing (but conservative) error. may grow linearly in
$\tau$.

_Proof sketch._ Since the system is deterministic, there is a unique scheduler
$\sigma$, thus
$R_{r}(\tau)=\sum_{\pi\in\Pi_{\mathsf{MC}}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow})$ by definition. We can show by induction over the length
of $\tau$ that
$\mathsf{Pr}_{\sigma}(\pi\mid\tau)=\mathsf{est_{\mathsf{MC}}}(\tau)({\pi}_{\downarrow})$
and conclude that
$R_{r}(\tau)=\sum_{\pi\in\Pi_{\mathcal{M}}^{|\tau|}}\mathsf{est_{\mathsf{MC}}}(\tau)({\pi}_{\downarrow})\cdot
r({\pi}_{\downarrow})=\sum_{s\in S}\mathsf{est_{\mathsf{MC}}}(\tau)(s)\cdot
r(s)$ because $\mathsf{est_{\mathsf{MC}}}(\tau)(s)=0$ for all $s\in S$ for
which there is no path $\pi\in\Pi_{\mathcal{M}}^{|\tau|}$ with
${\pi}_{\downarrow}=s$. The complexity follows from the inductive definition
of $\mathsf{est_{\mathsf{MC}}}$ that requires in each inductive step to
iterate over all transitions of the system and maintain a belief over the
states of the system. ∎

###  3.3 State estimators for Markov decision processes.

In an MDP, we have to account for every possible resolution of nondeterminism,
which means that a belief can evolve into a set of beliefs:

######  Definition 6 (MDP state estimator)

For an MDP $\mathcal{M}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, a trace
$\tau\in\mathsf{Z}^{+}$, and a state-risk function $r\colon
S\rightarrow\mathbb{R}_{\geq 0}$, the state estimation function
$\mathsf{est_{MDP}}\colon\mathsf{Z}^{+}\rightarrow 2^{\mathsf{Bel}}$ is
defined as

$\displaystyle\mathsf{est_{MDP}}(z)$ $\displaystyle=$
$\displaystyle\\{\mathsf{est_{\mathsf{MC}}}(z)\\},$
$\displaystyle\mathsf{est_{MDP}}(\tau\cdot z)$ $\displaystyle=$
$\displaystyle\Big{\\{}\mathsf{bel}^{\prime}\in\mathsf{Bel}\Bigm{|}\exists\mathsf{bel}\in\mathsf{est_{MDP}}(\tau).\leavevmode\nobreak\
\mathsf{bel}^{\prime}\in\mathsf{est_{MDP}^{up}}(\mathsf{bel},z)\Big{\\}},$

and where $\mathsf{bel}^{\prime}\in\mathsf{est_{MDP}^{up}}(\mathsf{bel},z)$ if
there exists $\varsigma_{\mathsf{bel}}\colon
S\rightarrow\mathsf{Distr}(\mathsf{Act})$ such that:

$\forall s^{\prime}.\mathsf{bel}^{\prime}(s^{\prime})=\frac{\sum\limits_{s\in
S}\mathsf{bel}(s)\cdot\sum\limits_{\alpha\in\mathsf{Act}}\varsigma_{\mathsf{bel}}(s)(\alpha)\cdot
P(s,\alpha,s^{\prime})\cdot\mathsf{obs}(s^{\prime})(z)}{\sum\limits_{s\in
S}\mathsf{bel}(s)\cdot\sum\limits_{\alpha\in\mathsf{Act}}\varsigma_{\mathsf{bel}}(s)(\alpha)\cdot\
\sum\limits_{\hat{s}\in S}P(s,\alpha,\hat{s})\cdot\mathsf{obs}(\hat{s})(z)}.$

The definition conservatively extends both Def. 3 and Def. 5. Furthermore, we
remark that we do not restrict how the nondeterminism is resolved: any
distribution over actions can be chosen, and the distributions may be
different for different traces.

Consider our system in Figure 1. For the trace $\tau=R_{o}\cdot M_{o}\cdot
L_{o}$, $\mathsf{est_{MDP}}(\tau)$ is computed as follows. First, when
observing $R_{o}$, the state estimator computes the initial belief set
$\mathsf{est_{MDP}}(R_{o})=\\{\\{\langle R,D_{2}\rangle\mapsto 1\\}\\}$. From
this set of beliefs, when observing $M_{o}$, a set
$\mathsf{est_{MDP}}(R_{o}\cdot M_{o})$ can be computed since all transitions
$\emptyset,\\{p\\},\\{w\\},\\{p,w\\}$ (as well as their convex combinations)
are possible from $\langle R,D_{2}\rangle$. One of these beliefs is for
example $\\{\langle R,D_{1}\rangle\mapsto\frac{4}{13},\langle
M,D_{1}\rangle\mapsto\frac{9}{13}\\}$ when a scheduler takes the transition
$\\{p\\}$ (as was computed in our example for the Markov chain case). Having
additionally observed $L_{o}$ a new set $\mathsf{est_{MDP}}(R_{o}M_{o}L_{o})$
of beliefs can be computed based on the beliefs in
$\mathsf{est_{MDP}}(R_{o}M_{o})$. For example from the belief $\\{\langle
R,D_{1}\rangle\mapsto\frac{4}{13},\langle
M,D_{1}\rangle\mapsto\frac{9}{13}\\}$, two of the new beliefs are $\\{\langle
L,D_{0}\rangle\mapsto 0.999,\langle M,D_{0}\rangle\mapsto 0.0001\\}$ and
$\\{\langle M,D_{1}\rangle\mapsto 0.0287,\langle M,D_{0}\rangle\mapsto
0.0001,\langle L,D_{0}\rangle\mapsto 0.9712\\}$. The first belief is reached
by a scheduler that takes a transition $\\{p\\}$ at both $\langle
R,D_{1}\rangle$ and $\langle M,D_{1}\rangle$. Notice that the belief does not
give a positive probability to the state $\langle R,D_{0}\rangle$ because
$L_{o}$ cannot be observed in this state. The second belief is reached by
considering a scheduler that takes transition $\\{p\\}$ at $\langle
M,D_{1}\rangle$ and transition $\emptyset$ at $\langle R,D_{1}\rangle$.

###### Theorem 3.1

For an MDP $\mathcal{M}=\langle
S,\iota,\mathsf{Act},P,\mathsf{Z},\mathsf{obs}\rangle$, a trace
$\tau\in\mathsf{Z}^{+}$, and a state-risk function $r\colon
S\rightarrow\mathbb{R}_{\geq 0}$, it holds that
$R_{r}(\tau)=\sup_{\mathsf{bel}\in\mathsf{est_{MDP}}(\tau)}\sum_{s\in
S}\mathsf{bel}(s)\cdot r(s)$.

_Proof sketch._ For a given trace $\tau$, each (history-dependent,
randomizing) scheduler induces a belief over the states of the Markov chain
induced by the scheduler. Also, each belief in $\mathsf{est_{MDP}}(\tau)$
corresponds to a fixed scheduler, namely that one used to compute the belief
recursively (i.e., an arbitrary randomizing memoryless scheduler for every
time step). Once a scheduler $\sigma$ and its corresponding belief
$\mathsf{bel}$ is fixed, or vice versa, we can show using induction over the
length of $\tau$ that
$\sum_{\pi\in\Pi_{\mathcal{M}}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow})=\sum_{s\in S}\mathsf{bel}(s)\cdot r(s)$. ∎

##  4 Convex Hull-based Forward Filtering

In this section, we show that we can use a finite representation for
$\mathsf{est_{MDP}}(\tau)$, but that this representation is exponentially
large for some MDPs.

###  4.1 Properties of $\mathsf{est_{MDP}}(\tau)$.

First, observe that $\mathbf{0}$ never maximises the risk. Furthermore,
$\mathsf{est_{MDP}^{up}}(\mathbf{0},z)=\\{\mathbf{0}\\}$. We can thus w.l.o.g.
assume that $\mathbf{0}\not\in\mathsf{est_{MDP}}(\tau)$. Second, observe that
$\mathsf{est_{MDP}}(\tau)\neq\emptyset$ if $\mathsf{Pr}_{\sigma}(\tau)>0$.

We can interpret a belief $\mathsf{bel}\in\mathsf{Bel}$ as point in (a bounded
subset of) $\mathbb{R}^{(|S|-1)}$. We are in particular interested in convex
sets of beliefs. A set $B\subseteq\mathsf{Bel}$ is convex if the convex hull
$\mathsf{CH}(B)$ of $B$, i.e. all convex combination of beliefs in $B$ 666That
is, $\mathsf{CH}(B)=\\{\sum_{\mathsf{bel}\in B}\sum_{s\in
S}\;w_{s}\cdot\mathsf{bel}(s)\mid\text{for all }w_{s}\in\mathbb{R}_{\geq
0}\text{ with }\sum w_{s}=1\\}$., coincides with $B$, $\mathsf{CH}(B)=B$. For
a set $B\subseteq\mathsf{Bel}$, a belief $\mathsf{bel}\in B$ is an interior
belief if it can be expressed as convex combination of the beliefs in
$B\setminus\\{\mathsf{bel}\\}$. All other beliefs are (extremal) points or
_vertices_. Let the set $\mathcal{V}(B)\subseteq B$ denote the set of
_vertices of the convex hull_ of $B$.

$s_{1}$$s_{0}$$s_{3}$$s_{2}$$s_{4}$$1$$\nicefrac{{1}}{{4}}$$\nicefrac{{3}}{{4}}$$1$$1$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$

$1,0$$\nicefrac{{3}}{{4}},\nicefrac{{1}}{{4}}$ (a) $B$ over $s_{1},s_{3}$

$1,0,0$$0,1,0$$0,\nicefrac{{1}}{{2}},\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{8}},\nicefrac{{3}}{{4}},\nicefrac{{1}}{{8}}$$\nicefrac{{7}}{{8}},0,\nicefrac{{1}}{{8}}$$\nicefrac{{1}}{{8}},\nicefrac{{3}}{{8}},\nicefrac{{1}}{{2}}$
(b) $B$ over $s_{0},s_{1},s_{3}$

$\nicefrac{{1}}{{2}},\nicefrac{{1}}{{2}}$ (c) $B$ over $s_{2},s_{3}$

Figure 3: Beliefs in $\mathbb{R}^{n}$ on $\mathcal{M}$ for
$\tau={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}z_{0}}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}z_{1}}$,
respectively.

###### Example 1

Consider Fig. 3. All observation are Dirac, and only states $s_{2}$ and
$s_{4}$ have observation
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}z_{1}}$.
The beliefs having observed
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}$
are distributions over $s_{1},s_{3}$, and can thus be depicted in a one-
dimensional simplex. In particular, we have
$\mathcal{V}(\mathsf{est_{MDP}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}))=\left\\{\\{s_{1}\mapsto
1\\},\\{s_{1}\mapsto\nicefrac{{3}}{{4}},s_{3}\mapsto\nicefrac{{1}}{{4}}\\}\right\\}$,
as depicted in Fig. 3(a). The six beliefs having observed
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}z_{0}}$
are distributions over $s_{0},s_{1},s_{3}$, depicted in Fig. 3(b). Five out of
six beliefs are vertices. The belief having observed
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}z_{1}}$
is in Fig. 3(c).

###### Remark 2

Observe that we illustrate the beliefs over only the states
$\mathsf{est_{\mathsf{KS}}}(\tau)$. We therefore call
$|\mathsf{est_{\mathsf{KS}}}(\tau)|$ the dimension of
$\mathsf{est_{MDP}}(\tau)$.

From the fundamental theorem of linear programming [46, Ch. 7] it immediately
follows that the trace risk $R_{\tau}$ is obtained at a vertex of the beliefs
of $\mathsf{est_{MDP}}{\tau}$. We obtain the following refinement over Theorem
3.1:

###### Theorem 4.1

For every $\tau$ and $r$:
$R_{r}(\tau)=\max\limits_{\mathsf{bel}\in{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathcal{V}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathsf{est_{MDP}}(\tau)})}}\sum_{s\in
S}\mathsf{bel}(s)\cdot r(s).$

Lemma 5 below clarifies that this maximum indeed exists.

We make some observations that allow us to compute the vertices more
efficiently: Let $\mathsf{est_{MDP}^{up}}(B,z)$ denote
$\bigcup_{\mathsf{bel}\in B}\mathsf{est_{MDP}^{up}}(\mathsf{bel},z)$. From the
properties of convex sets [18, Ch. 2], we make the following observations: If
$B$ is convex $\mathsf{est_{MDP}^{up}}(B,z)$ is convex, as all operations in
computing a new belief are convex-set preserving777The scaling is called a
_projection_.. Furthermore, if $B$ has a finite set of vertices, then
$\mathsf{est_{MDP}^{up}}(B,z)$ has a finite set of vertices. The following
lemma which is based on the observations above clarifies how to compute the
vertices:

###### Lemma 4

For a convex set of beliefs $B$ with a finite set of vertices and an
observation $z$:

$\mathcal{V}(\mathsf{est_{MDP}^{up}}(B,z))=\mathcal{V}(\mathsf{est_{MDP}^{up}}(\mathcal{V}(B),z)).$

By induction and using the facts above we obtain:

###### Lemma 5

Any $\mathcal{V}(\mathsf{est_{MDP}}(\tau))$ is finite.

A monitor thus only needs to track the vertices. Furthermore,
$\mathsf{est_{MDP}^{up}}(B,z)$ can be adapted to compute only vertices by
limiting $\varsigma_{\mathsf{bel}}$ to $S\rightarrow\mathsf{Act}$.

###  4.2 Exponential lower bounds on the relevant vertices.

We show that a monitor in general cannot avoid an exponential blow-up in the
beliefs it tracks. First observe that updating $\mathsf{bel}$ yields up to
$\prod_{s}|\mathsf{Act}(s)|$ new beliefs (vertex or not), a prohibitively
large number. The number of vertices is also exponential:

###### Lemma 6

There exists a family of MDPs $\mathcal{M}_{n}$ with $2n+1$ states such that
${|\mathcal{V}(\mathsf{est_{MDP}}(\tau))|=2^{n}}$ for every $\tau$ with
$|\tau|>2$.

$s_{0}$$h_{1}$$l_{1}$$h_{2}$$l_{2}$$h_{3}$$l_{3}$$C_{1}$$C_{2}$$C_{3}$$A$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$A$$B$$A$$A$$B$$A$$A$$B$$A$

(a) $\mathcal{M}_{3}$. Observations $\mathsf{Z}=\mathsf{Act}$ with
$\mathsf{obs}(s,\alpha)=\alpha$ if $\alpha\neq B$ and $\mathsf{obs}(s,B)=A$
for every $s$. Initial belief is $A$, all probabilities are $1$, unless stated
otherwise.

$l_{1}$$h_{1}$$\times$$l_{2}$$h_{2}$$\times$$l_{3}$$h_{3}$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$ (b) Beliefs after $AA$

$l_{1}$$h_{1}$$\times$$l_{2}$$h_{2}$$\times$$l_{3}$$h_{3}$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$ (c) Beliefs after $AAA$

$l_{1}$$h_{1}$$\times$$l_{2}$$h_{2}$$\times$$l_{3}$$h_{3}$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$$\langle\nicefrac{{1}}{{3}},0\rangle$$\langle
0,\nicefrac{{1}}{{3}}\rangle$ (d) Beliefs after $AAAA^{+}$

Figure 4: Construction for the correctness of Lemma 6.

_Proof sketch._ We construct $\mathcal{M}_{n}$ with $n=3$, that is,
$\mathcal{M}_{3}$ in Fig. 4(a). For this MDP and $\tau=AAA$,
$|\mathcal{V}(\mathsf{est_{MDP}}(\tau))|=2^{3}$. In particular, observe how
the belief factorizes into a belief within each component
$C_{i}=\\{h_{i},l_{i}\\}$ and notice that $\mathcal{M}_{n}$ has components
$C_{1}$ to $C_{n}$. In particular, for each component, the belief being that
we are with probability mass $\nicefrac{{1}}{{n}}$ (for
$n=3,\nicefrac{{1}}{{3}}$) in the ’low’ state $l_{i}$ or the ’high’ state
$h_{i}$. We depict the beliefs in Fig. 4(b,c,d). Thus, for any $\tau$ with
$|\tau|>2$ we can compactly represent $\mathcal{V}(\mathsf{est_{MDP}}(\tau))$
as bit-strings of length $n$. Concretely, the belief

$\displaystyle\\{h_{1},l_{2},l_{3}\mapsto\nicefrac{{1}}{{3}},l_{1},h_{2},h_{3}\mapsto
0\\}\text{ maps to }100,\text{ and }$
$\displaystyle\\{h_{1},l_{2},h_{3}\mapsto\nicefrac{{1}}{{3}},l_{1},h_{2},l_{3}\mapsto
0\\}\text{ maps to }101.$

These are exponentially many beliefs for bit strings of length $n$.∎

One might ask whether a symbolic encoding of an exponentially large set may
result in a more tractable approach to filtering. While Theorem 4.1 allows to
compute the associated risk from a set of linear constraints with standard
techniques, it is not clear whether the concise set of constraints can be
efficiently constructed and updated in every step. We leave this concern for
future work.

In the remainder we investigate whether we need to track all these beliefs.
First, when the monitor is unaware of the state-risk, this is trivially
unavoidable. More precisely, all vertices may induce the maximal weighted
trace risk by choosing an appropriate state-risk:

###### Lemma 7

For every $\tau$ and every
$\mathsf{bel}\in\mathcal{V}(\mathsf{est_{MDP}}(\tau))$ there exists an $r$
s.t.

$\sum_{s\in S}\mathsf{bel}(s)\cdot
r(s)\geq\max\limits_{\mathsf{bel}^{\prime}\in\mathcal{V}(\mathsf{est_{MDP}}(\tau))\setminus\\{\mathsf{bel}\\}}\sum_{s\in
S}\mathsf{bel}^{\prime}(s)\cdot r(s)\text{ with
$\max_{\mathsf{bel}\in\emptyset}=-\infty.$ }$

_Proof sketch._ We construct $r$ such that $r(s)>r(s^{\prime})$ if
$\mathsf{bel}(s)>\mathsf{bel}(s^{\prime})$. ∎

Second, even if the monitor is aware of the state risk $r$, it may not be able
to prune enough vertices to avoid exponential growth. The crux here is that
while some of the current beliefs may induce a smaller risk, an extension of
the trace may cause the belief to evolve into a belief that induces the
maximal risk.

###### Theorem 4.2

There exist MDPs $\mathcal{M}_{n}$ a $\tau$ with
$B\colonequals\mathcal{V}(\mathsf{est_{MDP}}(\tau))$ and a state-risk $r$ such
that $|B|=2^{n}$ and for all $\mathsf{bel}\in B$ exists
$\tau^{\prime}\in\mathsf{Z}^{+}$ with
$R_{r}(\tau\cdot\tau^{\prime})>\sup_{\mathsf{bel}\in
B^{\prime}}\sum_{s}\mathsf{bel}(s)\cdot r(s)$, where
$B^{\prime}=\mathsf{est_{MDP}^{up}}(B\setminus\\{\mathsf{bel}\\},\tau^{\prime})$.

It is helpful to understand this theorem as describing the outcome of a game
between monitor and environment: The statement says if the monitor decides to
drop some vertices from $\mathsf{est_{MDP}}{\tau}$, the environment may
produce an observation trace $\tau^{\prime}$ that will lead the monitor to
underestimate the weighted risk at $R_{r}(\tau\cdot\tau^{\prime})$.

_Proof sketch._ We extend the construction of Fig. 4(a) with choices to go to
a final state. The full proof sketch can be found in Appendix 0.C.

###  4.3 Approximation by pruning

Finally, we illustrate that we cannot simply prune small probabilities from
beliefs. This indicates that an approximative version of filtering for the
monitoring problem is nontrivial. Reconsider observing
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}$
in the MDP of Fig. 3, and, for the sake of argument, let us prune the (small)
entry $s_{3}\mapsto\nicefrac{{1}}{{4}}$ to $0$. Now, continuing with the trace
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}z_{1}}$,
we would update the beliefs from before and then conclude that this trace
cannot be observed with positive probability. With pruning, there is no upper
bound on the difference between the _computed_ $R_{\tau}$ and the _actual_
$R_{\tau}$. Thus, forward filtering is, in general, not tractable on MDPs.

##  5 Unrolling with Model Checking

We present a tractable algorithm for the monitoring problem. Contrary to
filtering, this method incorporates the state risk. We briefly consider the
qualitative case. An algorithm that solves that problem iteratively guesses a
successor such that the given trace has positive probability, and reaches a
state with sufficient risk. The algorithm only stores the current and next
state and a counter.

###### Theorem 5.1

The Monitoring Problem with $\lambda=0$ is in NLOGSPACE.

This result implies the existence of a polynomial time algorithm, e.g., using
a graph-search on a graph growing in $|\tau|$. There also is a deterministic
algorithm with space complexity $\mathcal{O}(log^{2}(|\mathcal{M}|+|\tau|))$,
which follows from applying Savitch’s Theorem [45], but that algorithm has
exponential time complexity.

We now present a tractable algorithm for the quantitative case, where we need
to store all paths. We do this efficiently by storing an unrolled MDP with
these paths using ideas from [9, 19]. In particular, on this MDP, we can
efficiently obtain the scheduler that optimizes the risk by model checking
rather than enumerating over all schedulers explicitly. We give the result
before going into details.

###### Theorem 5.2

The Monitoring Problem (with $\lambda>0$) is P-complete.

The problem is P-hard, as unary-encoded step-bounded reachability is P-hard
[40]. It remains to show a P-time algorithm888On first sight, this might be
surprising as step-bounded reachability in MDPs is PSPACE-hard and only quasi-
polynomial. However, our problem gets a trace and therefore (assuming that the
trace is not compressed) can be handled in time polynomial in the length of
the trace., which is outlined below. Roughly, the algorithm constructs an MDP
$\mathcal{M}^{\prime\prime\prime}$ from $\mathcal{M}$ in three conceptual
steps, such that the maximal probability of reaching a state in
$\mathcal{M}^{\prime\prime\prime}$ coincides with the $R_{r}(\tau)$. The
former can be solved by linear programming in polynomial time. The downside is
that even in the best case, the memory consumption grows linearly in $|\tau|$.

We outline the main steps of the algorithm and exemplify them below: First, we
transform $\mathcal{M}$ into an MDP $\mathcal{M}^{\prime}$ with _deterministic
state_ observations, i.e., with $\mathsf{obs}^{\prime}\colon
S\rightarrow\mathsf{Z}$. This construction is detailed in [19, Remark 1], and
runs in polynomial time. The new initial distribution takes into account the
initial observation and the initial distribution. Importantly, for each path
$\pi$ and each trace $\tau$, $\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)$ is
preserved. From here, the idea for the algorithm is a tailored adaption of the
construction for conditional reachability probabilities in [9]. We ensure that
$r(s)\in[0,1]$ by scaling $r$ and $\lambda$ accordingly. Now, we construct a
new MDP $\mathcal{M}^{\prime\prime}=\langle
S^{\prime\prime},\iota^{\prime\prime},\mathsf{Act}^{\prime\prime},P^{\prime\prime}\rangle$
with state space
$S^{\prime\prime}\colonequals(S^{\prime}\times\\{0,\ldots,|\tau|{-}1\\})\cup\\{\bot,\top\\}$
and an $n$-times unrolled transition relation. Furthermore, from the states
$\langle s,|\tau|{-}1\rangle$, there is a single outgoing action that with
probability $r(s)$ leads to $\top$ and with probability $1-r(s)$ leads to
$\bot$. Observe that the risk is now the supremum of conditioned reachability
probabilities over paths that reach $\top$, conditioned by the trace $\tau$.
The MDP $\mathcal{M}^{\prime\prime}$ is only polynomially larger. Then, we
construct MDP $\mathcal{M}^{\prime\prime\prime}$ by copying
$\mathcal{M}^{\prime\prime}$ and replacing (part of) the transition relation
$P^{\prime\prime}$ by $P^{\prime\prime\prime}$ such that paths $\pi$ with
$\tau\not\in\mathsf{obs}_{\mathsf{tr}}(\pi)$ are looped back to the initial
state (resembling rejection sampling). Formally,

$\displaystyle P^{\prime\prime\prime}(\langle
s,i\rangle,\alpha)=\begin{cases}P^{\prime\prime}(\langle
s,i\rangle,\alpha)&\text{if }\mathsf{obs}^{\prime}(s)=\tau_{i},\\\
\iota&\text{otherwise}.\end{cases}$

The maximal conditional reachability probability in
$\mathcal{M}^{\prime\prime}$ is the maximal reachability probability in
$M^{\prime\prime\prime}$ [9]. Maximal reachability probabilities can be
computed by solving a linear program [42], and can thus be computed in
polynomial time.

$s_{0}$$s_{1}$$s_{1}$$\alpha$$\beta$$\alpha$$1$$1$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$s_{2}$
(a) $\mathcal{M}$

$s_{0}$$s_{1}$$s_{2}$$s_{2}$$1$$\nicefrac{{1}}{{4}}$$\nicefrac{{3}}{{4}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{8}}$$\nicefrac{{3}}{{8}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{8}}$$\nicefrac{{3}}{{8}}$
(b) $\mathcal{M}^{\prime}$

$s_{0}^{0}$$s_{1}^{0}$$s_{2}$$s_{2}^{0}$$s_{0}^{1}$$s_{1}^{1}$$s_{2}^{1}$$\bot$$\top$$1$$\nicefrac{{1}}{{4}}$$\nicefrac{{3}}{{4}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{8}}$$\nicefrac{{3}}{{8}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{8}}$$\nicefrac{{3}}{{8}}$$\nicefrac{{1}}{{2}}$$1$$1$$\nicefrac{{1}}{{2}}$
(c) $\mathcal{M}^{\prime\prime}$

$s_{0}^{0}$$s_{1}^{0}$$s_{2}$$s_{2}^{0}$$s_{0}^{1}$$s_{1}^{1}$$s_{2}^{1}$$\bot$$\top$$1$$\nicefrac{{1}}{{4}}$$\nicefrac{{3}}{{4}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{8}}$$\nicefrac{{3}}{{8}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$1$$\nicefrac{{1}}{{2}}$
(d) $\mathcal{M}^{\prime\prime\prime}$

Figure 5: Polynomial-time algorithm for solving Problem 1 illustrated.

###### Example 2

We illustrate the construction in Fig. 5. In Fig. 5(a), we depict an MDP
$\mathcal{M}$, with $\iota=\\{s_{0},s_{1}\mapsto\nicefrac{{1}}{{2}}\\}$.
Furthermore, let
$\tau={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}}$
and let $r(s_{0})=1$ and $r(s_{1})=2$. Let
$\mathsf{obs}(s_{0})=\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}}\mapsto
1\\}$ and
$\mathsf{obs}(s_{1})=\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}}\mapsto\nicefrac{{1}}{{4}},{\color[rgb]{1,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.5,0}z_{1}}\mapsto\nicefrac{{3}}{{4}}\\}$.
State $s_{1}$ has two possible observations, so we split $s_{1}$ into $s_{1}$
and $s_{2}$ in MDP $\mathcal{M}^{\prime}$, each with their own observations.
Any transition into $s_{1}$ is now split. As $|\tau|=2$, we unroll the MDP
$\mathcal{M}^{\prime}$ into MDP $\mathcal{M}^{\prime\prime}$ to represent two
steps, and add goal and sink states. After rescaling, we obtain that
$r(s_{0})=\nicefrac{{1}}{{2}}$, whereas
$r(s_{1})=r(s_{2})=\nicefrac{{2}}{{2}}=1$, and we add the appropriate outgoing
transitions to the states $s^{1}_{\ast}$. In a final step, we create MDP
$\mathcal{M}^{\prime\prime\prime}$ from $\mathcal{M}^{\prime\prime}$: we
reroute all probability mass that does not agree with the observations to the
initial states. Now,
$R_{r}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{0}z_{0}})$
is given by the probability to reach, in $\mathcal{M}^{\prime\prime\prime}$,
in an unbounded number of steps, $\top$.

The construction also implies that maximizing over a finite set of schedulers,
namely the deterministic schedulers with a counter from $0$ to $|\tau|$,
suffices. We denote this class $\Sigma_{\text{DC}}(|\tau|)$. Formally, a
scheduler is in $\Sigma_{\text{DC}}(k)$ if $\text{for all }\pi,\pi^{\prime}$:

$\Big{(}{\pi}_{\downarrow}={\pi^{\prime}}_{\downarrow}\land\big{(}|\pi|=|\pi^{\prime}|\lor(|\pi|>k\land|\pi^{\prime}|>k)\big{)}\Big{)}\text{
implies }\sigma(\pi)=\sigma(\pi^{\prime}).$

###### Lemma 8

For every $\tau$, it holds that

$R_{r}(\tau)\quad=\quad\max_{\sigma\in\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\Sigma_{\text{DC}}(|\tau|)\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}\sum_{\pi\in\Pi_{M}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow}).$

The crucial idea underpinning this lemma is that memoryless schedulers suffice
for the unrolling, and that the states of the unrolling can be uniquely mapped
to a state and the length of the history for every $\pi$ through
$\mathcal{M}$. By reducing step-bounded reachability we can also show that
this set of schedulers is necessary [4].

##  6 Empirical Evaluation

##### Implementation.

We provide prototype implementations for both filtering- and model-checking-
based approaches from Sec. 3, built on top of the probabilistic model checker
Storm [30]. We provide a schematic setup of our implementation in Fig. 6.

SystemSimulatorModelcheckerState risktemporal specMDP(Prism
lang.)SeedUnrollingSec. 5Forw. FilterSec.
4ConvexHullModelcheckingMonitorUnrollingSec. 5Forw. FilterSec.
4ConvexHullModelchecking$r\colon S\rightarrow\mathbb{R}_{\geq 0}$obs
$z_{i}$$<$internal memory$>$ after $z_{0}\ldots z_{i-1}$iterative processinput
_uses_ _uses_ risk$R_{i}$ Figure 6: Schematic setup for prototype mapping
stream $z_{0}\ldots z_{k}$ to stream $R_{0}\ldots R_{k}$.

As input, we consider a symbolic description of MDPs with state-based
observation labels, based on an extended dialect of the Prism language. We
define the state risk in this MDP via a temporal property (given as a PCTL
formula), and obtain the concrete state-risk by model checking. We take a seed
that yields a trace using the simulator. For the experiments, actions are
resolved uniformly in this simulator999This is not an assumption but rather
our evaluation strategy.. The simulator iteratively feeds observations into
the monitor, running either of our two algorithms (implemented in C++). After
each observation $z_{i}$, the monitor computes the risk $R_{i}$ having
observed $z_{0}\ldots z_{i}$. We flexibly combine these components via a
Python API 101010Available at https://github.com/monitoring-MDPs/premise.

For filtering as in Sec. 4, we provide a sparse data structure for beliefs
that is updated using only deterministic schedulers. This is sufficient, see
Lemma 4. To further prune the set of beliefs, we implement an SMT-driven
elimination [47] of interior beliefs, inside of the convex hull111111Advanced
algorithms like Quickhull [10] are not without significant adaptions
applicable as the set of beliefs can be degenerate (roughly, a set without
full rank).. We construct the unrolling as described in Sec. 5 and apply model
checking via any sparse engines in Storm.

##### Reproducibility.

We archived a container with sources, benchmarks, and scripts to reproduce our
experiments: https://doi.org/10.5281/zenodo.4724622.

##### Set-up.

For each benchmark described below, we sampled 50 random traces using seeds
0–49 of lengths up to $|\tau|=500$. We are interested in the _promptness_ ,
that is, the delay of time between getting an observation $z_{i}$ and
returning corresponding risk $r_{i}$, as well as the _cumulative performance_
obtained by summing over the promptness along the trace. We use a timeout of
$1$ second for this query. We compare the forward filtering (FF) approach with
and without convex hull (CH) reduction, and the model unrolling approach (UNR)
with two model checking engines of Storm: exact policy iteration (EPI, [42])
and optimistic value iteration (OVI, [28]). All experiments are run on a
MacBook Pro MV962LL/A, using a single core. The memory limit of 6GB was not
violated. We use Z3 [37] as SMT-solver [11] for the convex hull reduction.

##### Benchmarks.

We present three benchmark families, all MDPs with a combination of
probabilities, nondeterminism and partial observability.

Airport-A is as in Sec. 1, but with a higher resolution for both ground
vehicle in the middle lane and the plane. Airport-B has a two-state sensor
model with stochastic transitions between them.

Refuel-A models robots with a depleting battery and recharging stations. The
world model consists of a robot moving around in a $D{\times}D$ grid with some
dedicated charging cells, where each action costs energy. The risk is to
deplete the battery within a fixed horizon. Refuel-B is a two-state sensor
variant.

Evade-I is inspired by a navigation task in a multi-agent setting in a
$D{\times}D$ grid. The monitored robot moves randomly, and the risk is defined
as the probability of crashing with the other robot. The other robot has an
internal incentive in the form of a cardinal direction, and
nondeterministically decides to move or to uniformly randomly change its
incentive. The monitor observes everything except the incentive of the other
robot. Evade-V is an alternative navigation task: Contrary to above, the other
robot does not have an internal state and indeed navigates
nondeterministically in one of the cardinal directions. We only observe the
other robot location is within the view range.

Table 1: Performance for promptness of online monitoring on various
benchmarks.

|  |  |  |  |  | Forward Filtering | Unrolling
---|---|---|---|---|---|---|---
Id | Name | Inst | $|S|$ | $|P|$ | $|\tau|$ | $N$ | $\underset{\text{avg}}{T}$ | $\underset{\text{max}}{T}$ | $\underset{\text{avg}}{B}$ | $\underset{\text{max}}{B}$ | $\underset{\text{avg}}{D}$ | $\underset{\text{max}}{D}$ | $N$ | $\underset{\text{avg}}{T}$ | $\underset{\text{max}}{T}$ | $\underset{\text{avg}}{|S_{u}|}$ | $\underset{\text{max}}{|S_{u}|}$
1 | airport-A | 7,50,30 | 20910 | 114143 | 100 | 50 | 0.01 | 0.01 | 4.5 | 7 | 4.6 | 7 | 50 | 0.04 | 0.11 | 524 | 599
500 | 50 | 0.01 | 0.01 | 1.0 | 1 | 1.0 | 1 | 50 | 0.01 | 0.01 | 1075 | 1258
2 | airport-B | 3,50,30 | 20232 | 106012 | 100 | 0 |  |  |  |  |  |  | 50 | 0.09 | 0.16 | 556 | 629
500 | 0 |  |  |  |  |  |  | 50 | 0.01 | 0.01 | 1460 | 1647
3 | airport-B | 7,50,30 | 41820 | 308474 | 100 | 0 |  |  |  |  |  |  | 50 | 0.14 | 0.33 | 1000 | 1183
500 | 0 |  |  |  |  |  |  | 11 | 0.02 | 0.02 | 2097 | 2297
4 | refuel-A | 12,50 | 45073 | 2431691 | 100 | 50 | 0.01 | 0.01 | 2.2 | 4 | 2.8 | 5 | 50 | 0.01 | 0.05 | 325 | 409
500 | 50 | 0.01 | 0.01 | 1.5 | 4 | 1.7 | 5 | 50 | 0.01 | 0.19 | 1071 | 2409
5 | refuel-B | 12,50 | 90145 | 9725277 | 100 | 50 | 0.06 | 0.23 | 4.2 | 8 | 5.6 | 10 | 50 | 0.04 | 0.17 | 608 | 732
500 | 50 | 0.01 | 0.01 | 2.9 | 8 | 3.3 | 10 | 46 | 0.04 | 0.09 | 2171 | 4688
6 | evade-I | 15 | 377101 | 2022295 | 100 | 50 | 0.01 | 0.02 | 2.6 | 10 | 3.3 | 4 | 49 | 0.01 | 0.06 | 332 | 363
500 | 50 | 0.01 | 0.01 | 2.4 | 5 | 3.4 | 4 | 45 | 0.08 | 0.90 | 1655 | 1891
7 | evade-V | 5,3 | 1001 | 5318 | 100 | 26 | 0.01 | 0.01 | 1.0 | 1 | 1.0 | 1 | 50 | 0.00 | 0.02 | 134 | 241
500 | 25 | 0.01 | 0.01 | 1.0 | 1 | 1.0 | 1 | 50 | 0.00 | 0.01 | 538 | 671
8 | evade-V | 6,3 | 2161 | 11817 | 100 | 1 | 0.01 | 0.01 | 1.0 | 1 | 1.0 | 1 | 50 | 0.02 | 0.32 | 319 | 861
500 | 1 | 0.01 | 0.01 | 1.0 | 1 | 1.0 | 1 | 49 | 0.01 | 0.02 | 777 | 1484

##### Results.

We split our results in two tables. In Table 1, we give an ID for every
benchmark name and instance, along with the size of the MDP (nr. of states
$|S|$ and transitions $|P|$) our algorithms operate on. We consider the
promptness after prefixes of length $|\tau|$. In particular, for forward
filtering with the convex hull optimization, we give the number $N$ of traces
that did not time out before, and consider the average $T_{\text{avg}}$ and
maximal time $T_{\text{max}}$ needed (over all sampled traces that did not
time-out before). Furthermore, we give the average, $B_{\text{avg}}$, and
maximal, $B_{\text{max}}$, number of beliefs stored (after reduction), and the
average, $D_{\text{avg}}$, and maximal, $D_{\text{max}}$, dimension of the
belief support. Likewise, for unrolling with exact model checking, we give the
number $N$ of traces that did not time out before, and we consider average
$T_{\text{avg}}$ and maximal time $T_{\text{max}}$, as well as the average
size and maximal number of states of the unfolded MDP.

Table 2: Summarized performance for online monitoring

|  | FF w/ CH | FF w/o CH | UNR (EPI) | UNR (OVI)
---|---|---|---|---|---
Id | $|\tau|$ | $N$ | $\underset{\text{avg}}{T}$ | $\underset{\text{max}}{T}$ | $\underset{\text{avg}}{B}$ | $\underset{\text{avg}}{E}$ | $N$ | $\underset{\text{avg}}{T}$ | $\underset{\text{max}}{T}$ | $\underset{\text{avg}}{B}$ | $N$ | $\underset{\text{avg}}{T}$ | $\underset{\text{max}}{T}$ | $\underset{\text{avg}}{Bld^{\%}}$ | $\underset{\text{max}}{Bld^{\%}}$ | N | $\underset{\text{avg}}{T}$ | $\underset{\text{max}}{T}$
1 | 100 | 50 | 0.9 | 1.1 | 493 | 241 | 0 |  |  |  | 50 | 2.9 | 3.6 | 6 | 56 | 50 | 0.0 | 0.1
| 500 | 50 | 3.7 | 4.3 | 1040 | 316 | 0 |  |  |  | 50 | 7.5 | 10.7 | 21 | 24 | 50 | 0.4 | 0.8
2 | 100 | 0 |  |  |  |  | 0 |  |  |  | 50 | 3.7 | 4.7 | 6 | 54 | 50 | 0.1 | 0.1
| 500 | 0 |  |  |  |  | 0 |  |  |  | 50 | 11.9 | 17.1 | 18 | 23 | 50 | 0.6 | 0.8
3 | 100 | 0 |  |  |  |  | 0 |  |  |  | 50 | 7.6 | 10.6 | 5 | 55 | 50 | 0.1 | 0.2
| 500 | 0 |  |  |  |  | 0 |  |  |  | 11 | 21.3 | 28.7 | 19 | 23 | 50 | 0.9 | 1.7
4 | 100 | 50 | 0.7 | 0.8 | 241 | 138 | 1 | 0.9 | 0.9 | 1473 | 50 | 0.7 | 1.0 | 35 | 69 | 50 | 0.0 | 0.1
| 500 | 50 | 3.4 | 3.7 | 868 | 226 | 1 | 0.9 | 0.9 | 1873 | 50 | 5.6 | 21.2 | 57 | 67 | 50 | 0.5 | 0.9
5 | 100 | 50 | 7.4 | 10.7 | 442 | 2267 | 0 |  |  |  | 50 | 2.5 | 4.4 | 32 | 57 | 50 | 0.1 | 0.2
| 500 | 50 | 16.5 | 42.2 | 1781 | 4249 | 0 |  |  |  | 46 | 19.5 | 64.2 | 55 | 70 | 50 | 1.3 | 2.3
6 | 100 | 50 | 1.1 | 4.8 | 273 | 160 | 13 | 0.7 | 2.9 | 2055 | 49 | 0.5 | 2.0 | 34 | 65 | 47 | 0.0 | 0.1
| 500 | 50 | 5.1 | 11.5 | 1237 | 632 | 2 | 4.4 | 6.8 | 20524 | 45 | 22.4 | 53.6 | 13 | 29 | 43 | 0.5 | 0.7
7 | 100 | 26 | 0.8 | 1.2 | 106 | 11 | 13 | 0.1 | 0.5 | 274 | 50 | 0.4 | 1.0 | 19 | 45 | 48 | 0.0 | 0.1
| 500 | 25 | 3.7 | 4.2 | 505 | 7 | 13 | 0.1 | 0.5 | 674 | 50 | 1.3 | 4.4 | 46 | 58 | 47 | 0.2 | 0.3
8 | 100 | 1 | 1.3 | 1.3 | 124 | 109 | 0 |  |  |  | 50 | 1.5 | 7.0 | 15 | 39 | 36 | 0.4 | 5.6
| 500 | 1 | 4.3 | 4.3 | 524 | 109 | 0 |  |  |  | 49 | 4.9 | 28.1 | 37 | 56 | 35 | 0.7 | 6.4

In Table 2, we consider for the benchmarks above the cumulative performance.
In particular, this table also considers an alternative implementation for
both FF and UNR. We use the IDs to identify the instance, and sum for each
prefix of length $|\tau|$ the time. For filtering, we recall the number of
traces $N$ that did not time out, the average and maximal cumulative time
along the trace, the average cumulative number of beliefs that were
considered, and the average cumulative number of beliefs eliminated. For the
case without convex hull, we do not eliminate any vertices. For unrolling, we
report average $T_{\text{avg}}$ and maximal cumulative time using EPI, as well
as the time required for model building, $\mathit{Bld^{\%}}$ (relative to the
total time, per trace). We compare this to the average and maximal cumulative
time for using OVI (notice that building times remain approximately the same).

##### Discussion.

The results from our prototype show that conservative (sound) predictive
modeling of systems that combine probabilities, nondeterminism and partial
observability is within reach with the methods we proposed and state-of-the-
art algorithms. Both forward filtering and an unrolling-based approaches have
their merits. The practical results thus slightly diverge from the complexity
results in Sec. 3.1, due to structural properties of some benchmarks. In
particular, for airport-A and refuel-A, the nondeterminism barely influences
the belief, and so there is no explosion, and consequentially the dimension of
the belief is sufficiently small that the convex hull can be efficiently
computed. Rather than the number of states, this belief dimension makes
evade-V a difficult benchmark121212The max dimension ${=}1$ in evade-V is only
over the traces that did not time-out. The dimension when running in time-outs
is above $5$.. _If many states can be reached with a particular trace, and if
along these paths there are some probabilistic states, forward filtering
suffers significantly_. We see that if the benchmark allows for efficacious
forward filtering, it is not slowed down in the way that unrolling is slower
on longer traces. For UNR, we observe that OVI is typically the fastest, but
EPI does not suffer from the numerical worst-cases as OVI does. _If an
observation trace is unlikely, the unrolled MDP constitutes a numerically
challenging problem, in particular for value-iteration based model checkers_ ,
see [27]. For FF, the convex hull computation is essential for any dimension,
and eliminating some vertices in every step keeps the number of belief states
manageable.

##  7 Related work

We are not the first to consider model-based runtime verification in the
presence of partial observability and probabilities. Runtime verification with
state estimation on hidden Markov models (HMM)—without nondeterminism has been
studied for various types of properties [49, 55, 52] and has been extended to
hybrid systems [50]. The tool Prevent focusses on black-box systems by
learning an HMM from a set of traces. The HMM approximates (with only
convergence-in-the-limit guarantees) the actual system [6], and then estimates
during runtime the most likely trace rather than estimating a distribution
over current states. Extensions consider symmetry reductions on the models
[7]. These techniques do not make a conservative (sound) risk estimation. The
recent framework for runtime verification in the presence of partial
observability [23] takes a more strict black-box view and cannot provide state
estimates. Finally, [26] chooses to have partial observability to make
monitoring of software systems more efficient, and [56] monitors a noisy
sensor to reduce energy consumption.

State beliefs are studied when verifying HMMs [57], where the question whether
a sequence of observations likely occurs, or which HMM is an adequate
representation of a system [36]. State beliefs are prominent in the
verification of partially observable MDPs [39, 32, 16], where one can observe
the actions taken (but the problem itself is to find the right scheduler). Our
monitoring problem can be phrased as a special case of verification of
partially observable stochastic games [20], but automatic techniques for those
very general models are lacking. Likewise, the idea of _shielding_
(pre)computes all action choices that lead to safe behavior [15, 3, 24, 35, 5,
34]. For partially observable settings, shielding again requires to compute
partial-information schedulers [38, 21], contrary to our approach. Partial
observability has also been studied in the context of diagnosability, studying
if a fault has occurred (in the past) [14], or what actions uncover faults
[13]. We, instead assume partial observability in which we do detect faults,
but want to estimate the risk that these faults occur in the future.

The assurance framework for reinforcement learning [41] implicitly allows for
stochastic behavior, but cannot cope with partial observability or
nondeterminism. Predictive monitoring has been combined with deep learning
[17] and Bayesian inference [22], where the key problem is that the
computation of an imminent failure is too expensive to be done exactly. More
generally, learning automata models has been motivated with runtime assurance
[1, 53]. Testing approaches statistically evaluate whether traces are likely
to be produced by a given model [25]. The approach in [2] studies stochastic
black-box systems with controllable nondeterminism and iteratively learns a
model for the system.

##  8 Conclusion

We have presented the first framework for monitoring based on a trace of
observations on models that combine nondeterminism and probabilities. Future
work includes heuristics for approximate monitoring and for faster convex hull
computations, and to apply this work to grey-box (learned) models.

## References

  * [1] Aichernig, B.K., Bloem, R., Ebrahimi, M., Horn, M., Pernkopf, F., Roth, W., Rupp, A., Tappler, M., Tranninger, M.: Learning a behavior model of hybrid systems through combining model-based testing and machine learning. In: ICTSS. LNCS, vol. 11812, pp. 3–21. Springer (2019)
  * [2] Aichernig, B.K., Tappler, M.: Probabilistic black-box reachability checking (extended version). Formal Methods Syst. Des. 54(3), 416–448 (2019)
  * [3] Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI. pp. 2669–2678. AAAI Press (2018)
  * [4] Andova, S., Hermanns, H., Katoen, J.: Discrete-time rewards model-checked. In: FORMATS. LNCS, vol. 2791, pp. 88–104. Springer (2003)
  * [5] Avni, G., Bloem, R., Chatterjee, K., Henzinger, T.A., Könighofer, B., Pranger, S.: Run-time optimization for learned controllers through quantitative games. In: CAV (1). LNCS, vol. 11561, pp. 630–649. Springer (2019)
  * [6] Babaee, R., Gurfinkel, A., Fischmeister, S.: _P_ revent : A predictive run-time verification framework using statistical learning. In: SEFM. LNCS, vol. 10886, pp. 205–220. Springer (2018)
  * [7] Babaee, R., Gurfinkel, A., Fischmeister, S.: Predictive run-time verification of discrete-time reachability properties in black-box systems using trace-level abstraction and statistical learning. In: RV. LNCS, vol. 11237, pp. 187–204. Springer (2018)
  * [8] Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)
  * [9] Baier, C., Klein, J., Klüppelholz, S., Märcker, S.: Computing conditional probabilities in Markovian models efficiently. In: TACAS. LNCS, vol. 8413, pp. 515–530. Springer (2014)
  * [10] Barber, C.B., Dobkin, D.P., Huhdanpaa, H.: The quickhull algorithm for convex hulls. ACM Trans. Math. Softw. 22(4), 469–483 (1996)
  * [11] Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press (2009)
  * [12] Bartocci, E., Deshmukh, J.V., Donzé, A., Fainekos, G.E., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In: Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS, vol. 10457, pp. 135–175. Springer (2018)
  * [13] Bertrand, N., Fabre, E., Haar, S., Haddad, S., Hélouët, L.: Active diagnosis for probabilistic systems. In: FoSSaCS. LNCS, vol. 8412, pp. 29–42. Springer (2014)
  * [14] Bertrand, N., Haddad, S., Lefaucheux, E.: A tale of two diagnoses in probabilistic systems. Inf. Comput. 269 (2019)
  * [15] Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: - runtime enforcement for reactive systems. In: TACAS. LNCS, vol. 9035, pp. 533–548. Springer (2015)
  * [16] Bork, A., Junges, S., Katoen, J., Quatmann, T.: Verification of indefinite-horizon POMDPs. In: ATVA. LNCS, vol. 12302, pp. 288–304. Springer (2020)
  * [17] Bortolussi, L., Cairoli, F., Paoletti, N., Smolka, S.A., Stoller, S.D.: Neural predictive monitoring. In: RV. LNCS, vol. 11757, pp. 129–147. Springer (2019)
  * [18] Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press (2014)
  * [19] Chatterjee, K., Chmelik, M., Gupta, R., Kanodia, A.: Optimal cost almost-sure reachability in pomdps. Artif. Intell. 234, 26–48 (2016)
  * [20] Chatterjee, K., Doyen, L.: Partial-observation stochastic games: How to win when belief fails. ACM Trans. Comput. Log. 15(2), 16:1–16:44 (2014)
  * [21] Chatterjee, K., Novotný, P., Pérez, G.A., Raskin, J., Zikelic, D.: Optimizing expectation with guarantees in POMDPs. In: AAAI. pp. 3725–3732. AAAI Press (2017)
  * [22] Chou, Y., Yoon, H., Sankaranarayanan, S.: Predictive runtime monitoring of vehicle models using bayesian estimation and reachability analysis. In: IROS (2020), to appear
  * [23] Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: RV. LNCS, vol. 11757, pp. 165–184. Springer (2019)
  * [24] Dräger, K., Forejt, V., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log. Methods Comput. Sci. 11(2) (2015)
  * [25] Gerhold, M., Stoelinga, M.: Model-based testing of probabilistic systems. Formal Asp. Comput. 30(1), 77–106 (2018)
  * [26] Grigore, R., Kiefer, S.: Selective monitoring. In: CONCUR. LIPIcs, vol. 118, pp. 20:1–20:16. Dagstuhl - LZI (2018)
  * [27] Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111–131 (2018)
  * [28] Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). LNCS, vol. 12225, pp. 488–511. Springer (2020)
  * [29] Havelund, K., Rosu, G.: Runtime verification - 17 years later. In: RV. LNCS, vol. 11237, pp. 3–17. Springer (2018)
  * [30] Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. CoRR abs/2002.07080 (2020)
  * [31] Henzinger, T.A., Pei-Hsin Ho, Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43(4), 540–554 (1998)
  * [32] Horák, K., Bosanský, B., Chatterjee, K.: Goal-HSVI: Heuristic search value iteration for goal POMDPs. In: IJCAI. pp. 4764–4770. ijcai.org (2018)
  * [33] Jansen, N., Humphrey, L.R., Tumova, J., Topcu, U.: Structured synthesis for probabilistic systems. In: NFM. LNCS, vol. 11460, pp. 237–254. Springer (2019)
  * [34] Jansen, N., Könighofer, B., Junges, S., Serban, A., Bloem, R.: Safe reinforcement learning using probabilistic shields (invited paper). In: CONCUR. LIPIcs, vol. 171, pp. 3:1–3:16. Dagstuhl - LZI (2020)
  * [35] Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.: Safety-constrained reinforcement learning for MDPs. In: TACAS. LNCS, vol. 9636, pp. 130–146. Springer (2016)
  * [36] Kiefer, S., Sistla, A.P.: Distinguishing hidden Markov chains. In: LICS. pp. 66–75. ACM (2016)
  * [37] de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS. LNCS, vol. 4963, pp. 337–340. Springer (2008)
  * [38] Nam, W., Alur, R.: Active learning of plans for safety and reachability goals with partial observability. IEEE Trans. Syst. Man Cybern. Part B 40(2), 412–420 (2010)
  * [39] Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real Time Syst. 53(3), 354–402 (2017)
  * [40] Papadimitriou, C.H., Tsitsiklis, J.N.: The complexity of Markov decision processes. Math. Oper. Res. 12(3), 441–450 (1987)
  * [41] Phan, D., Paoletti, N., Grosu, R., Jansen, N., Smolka, S.A., Stoller, S.D.: Neural simplex architecture. CoRR abs/1908.00528 (2019), appears at NFM2020
  * [42] Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994)
  * [43] Rabiner, L.R.: A tutorial on hidden markov models and selected applications in speech recognition. Proc. of the IEEE 77(2), 257–286 (1989)
  * [44] Sánchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstic, S., Lourenço, J.M., Nickovic, D., Pace, G.J., Rufino, J., Signoles, J., Traytel, D., Weiss, A.: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 54(3), 279–335 (2019)
  * [45] Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)
  * [46] Schrijver, A.: Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization, Wiley (1999)
  * [47] Seidel, R.: Convex hull computations. In: Handbook of Discrete and Computational Geometry, 2nd Ed, pp. 495–512. Chapman and Hall/CRC (2004)
  * [48] Seshia, S.A.: Introspective environment modeling. In: RV. LNCS, vol. 11757, pp. 15–26. Springer (2019)
  * [49] Sistla, A.P., Srinivas, A.R.: Monitoring temporal properties of stochastic systems. In: VMCAI. LNCS, vol. 4905, pp. 294–308. Springer (2008)
  * [50] Sistla, A.P., Žefran, M., Feng, Y.: Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: RV. Springer (2012)
  * [51] Spaan, M.T.J.: Partially observable Markov decision processes. In: Reinforcement Learning, Adaptation, Learning, and Optimization, vol. 12, pp. 387–414. Springer (2012)
  * [52] Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: RV. LNCS, vol. 7186, pp. 193–207. Springer (2011)
  * [53] Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: L${}^{\mbox{*}}$-based learning of Markov decision processes. In: FM. LNCS, vol. 11800, pp. 651–669. Springer (2019)
  * [54] Thrun, S., Burgard, W., Fox, D.: Probabilistic robotics. Intelligent robotics and autonomous agents, MIT Press (2005)
  * [55] Wilcox, C.M., Williams, B.C.: Runtime verification of stochastic, faulty systems. In: RV. LNCS, vol. 6418, pp. 452–459. Springer (2010)
  * [56] Woo, H., Mok, A.K.: Real-time monitoring of uncertain data streams using probabilistic similarity. In: RTSS. pp. 288–300. IEEE CS (2007)
  * [57] Zhang, L., Hermanns, H., Jansen, D.N.: Logic and model checking for hidden Markov models. In: FORTE. LNCS, vol. 3731, pp. 98–112. Springer (2005)

##  Appendix 0.A On qualitative variants of the problem

We may reformulate the qualitative problem as follows: First, define the risk
as the maximum over reached states, i.e.,

$R_{r}^{\max}(\tau)=\max\limits_{\pi\in\Pi\text{ s.t.
}\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)>0}r({\pi}_{\downarrow}).$

This _maximum risk estimation_ conservatively states the highest risk that can
be achieved after an observation. The quantitative (qualitative) _maximal risk
estimation problem_ analogously is to decide $R_{r}^{\max}(\tau)>\lambda$ with
$\lambda\geq 0$ ($\lambda=0$).

###### Lemma 9

The qualitative risk estimation problem and the quantitative and qualitative
maximum risk estimation problem are all logspace interreducible.

######  Proof (Lemma 1 )

The qualitative case is a special case of the quantitative case. Now consider
the quantitative case, and assume some fixed $\lambda>0$. Observe that for any
fixed scheduler, $\sum_{\pi}\mathsf{Pr}_{\sigma}(\pi\mid\tau)=1$, and that
there is a unique path $\pi$ such that $\mathsf{Pr}_{\sigma}(\pi\mid\tau)=1$.
We can reduce the quantitative maximum risk estimation problem to a
qualitative monitoring problem as follows. We modify the state risk function
by checking state-wise whether the risk at a state is above $\lambda$. If it
is, then we set the state risk to $1$, and to zero otherwise. If
$R_{r}(\tau)>\lambda$ for some $\lambda\in\mathbb{R}_{\geq 0}$, then there is
a path $\pi\in\Pi_{\mathcal{M}}^{|\tau|}$ with
$r({\pi}_{\downarrow})>\lambda$. This in turn means that
$\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot r({\pi}_{\downarrow})>0$. The other
way around, if the sum over all paths is zero, then there is no such path.

######  Proof (Lemma 9 )

  * •

_The qualitative weighted risk estimation problem and the qualitative maximum
risk estimation problem coincide._

The qualitative weighted risk estimation problem and the qualitative maximum
risk estimation problem coincide. In the qualitative case $R_{r}(\tau)>0$
holds when at least one path $\pi$ matches the trace $\tau$ with a positive
probability and $r({\pi}_{\downarrow})>0$. In this case,
$R_{r}^{\max}(\tau)>0$ also holds, since $r({\pi}_{\downarrow})>0$ and
$\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)>0$.

When $R_{r}^{\max}(\tau)>0$ holds then there is a path $\pi$ such that
$r({\pi}_{\downarrow})>0$ and $\mathsf{obs}_{\mathsf{tr}}(\pi)(\tau)>0$. This
implies that $\mathsf{Pr}(\sigma)(\pi\mid\tau)>0$ and in turn that
$R_{r}(\tau)>0$. ∎

  * •

_The qualitative weighted risk estimation problem and the quantitative maximum
risk estimation problem are logspace interreducible._ From the qualitative
weighted risk estimation problem to the qualitative maximum risk estimation
problem is trivial and follows from the last lemma since the qualitative
maximum risk estimation problem is an instance of the quantitative maximum
risk estimation problem.

In the other direction, we can reduce the quantitative maximum risk estimation
problem to a qualitative weighted risk estimation problem as follows. We
modify the state risk function by checking state-wise whether the risk at a
state is above $\lambda$. If it is, then we set the state risk to $1$, and to
zero otherwise. If $R_{r}^{\max}(\tau)>\lambda$ for some
$\lambda\in\mathbb{R}_{\geq 0}$, then there is a path
$\pi\in\Pi_{\mathcal{M}}^{|\tau|}$ with $r({\pi}_{\downarrow})>\lambda$. This
in turn means that $\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow})>0$. Furthermore, if $R_{r}^{\max}(\tau)\leq\lambda$,
then for all $\pi\in\Pi_{\mathcal{M}}^{|\tau|}$, it holds that
$\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot r({\pi}_{\downarrow})=0$.

Both reduction can be performed in logspace. In the first direction we only
need to set the lambda. In the second direction we just need to iterate over
the states and change the risk function accordingly. ∎

##  Appendix 0.B Proof of Lemma 2

We show $R_{r}(\tau)=\max_{s\in\mathsf{est_{\mathsf{KS}}}(\tau)}r(s)$. We show
this by proving the following three equalities. Let
$\Pi_{{\mathsf{KS},\sigma}}^{|\tau|}=\\{\pi\in\Pi_{\mathsf{KS}}^{|\tau|}\mid\mathsf{Pr}_{\sigma}(\pi)>0\\}$
and let $\mathit{DetSched}(\mathsf{KS})$ be the set of deterministic
schedulers of $\mathsf{KS}$:

$\displaystyle R_{r}(\tau)$
$\displaystyle=\sup_{\sigma\in\textit{Sched}(\mathsf{KS})}\sum_{\pi\in\Pi_{\mathsf{KS}}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow})$ (1)
$\displaystyle=\sup_{\sigma\in\mathit{DetSched}(\mathsf{KS})}\sum_{\pi\in\Pi_{\mathsf{KS}}^{|\tau|}}\mathsf{Pr}_{\sigma}(\pi\mid\tau)\cdot
r({\pi}_{\downarrow})$ (2)
$\displaystyle=\max_{\sigma\in\mathit{DetSched}{\mathsf{KS}}}\max_{\pi\in\Pi_{{\mathsf{KS},\sigma}}^{|\tau|}}r({\pi}_{\downarrow})$
(3) $\displaystyle=\max_{s\in\mathsf{est_{\mathsf{KS}}}(\tau)}r(s)$ (4)

We start with $(1)=(2)$. The case $(1)\geq(2)$ is trivial since
$\mathit{DetSched}(\mathcal{M})\subseteq\textit{Sched}(\mathcal{M})$. The case
$(1)\leq(2)$ follows from as convex sums are maximized on their vertices. The
case $(2)=(3)$ holds because deterministic schedulers induce unique paths.
More precisely, since all distributions in a Kripke structure are Dirac, a
(deterministic) scheduler $\sigma$ and a trace $\tau$ defines a unique path
$\pi_{\sigma}$ in the Kripke structure. Due to the absence of probabilities,
for every path $\pi$, we have $\mathsf{Pr}_{\sigma}(\pi\mid\tau)\in\\{0,1\\}$,
and thus we have $\Pi_{{\mathsf{KS},\sigma}}^{|\tau|}=\\{\pi_{\sigma}\\}$. For
$(3)=(4)$, the path $\pi_{\sigma}$ has a unique last state
$s={\pi_{\sigma}}_{\downarrow}$ that is obtained having observed $\tau$. Let
$S_{\tau}=\\{{\pi}_{\downarrow}\mid\exists\sigma.\\{\pi\\}=\Pi_{{\mathsf{KS},\sigma}}^{|\tau|}\\}$.
It follows that

$\max_{\sigma\in\textit{Sched}(\mathsf{KS})}\max_{\pi\in\Pi_{{\mathsf{KS},\sigma}}^{|\tau|}}r({\pi}_{\downarrow})=\max_{s\in
S_{\tau}}r(s).$

By induction over $|\tau|$, we can show
$S_{\tau}=\mathsf{est_{\mathsf{KS}}}(\tau)$.

##  Appendix 0.C Proof of Thm 4.2

$s_{0}$$h_{1}$$l_{1}$$h_{2}$$l_{2}$$h_{3}$$l_{3}$$\bot$$\top$$C_{1}$$C_{2}$$C_{3}$$A$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$\nicefrac{{1}}{{6}}$$A$$B$$A$$A$$B$$A$$A$$B$$A$$H_{1}$$L_{1}$$H_{1}$$L_{1}$$H_{2}$$L_{2}$$H_{2}$$L_{2}$$H_{3}$$L_{3}$$H_{3}$$L_{3}$$H_{2},L_{2}$$H_{3},L_{3}$$H_{1},L_{1}$$H_{3},L_{3}$$H_{1},L_{1}$$H_{2},L_{2}$∗∗

Figure 7: Construction for the correctness of Thm. 4.2, showing
$\mathcal{M}_{3}$’. Observations $\mathsf{Z}=\mathsf{Act}$ with
$\mathsf{obs}(s,\alpha)=\alpha$ if $\alpha\neq B$ and $\mathsf{obs}(s,B)=A$
for every $s$. Initial belief is $A$, all probabilities are $1$, unless stated
otherwise. Self-loops at the components $C_{1},C_{2},C_{3}$ reflect self-loops
on the states in the components.

We extend the construction of Fig. 4(a), to obtain the MDP
$\mathcal{M}^{\prime}_{3}$ in Fig. 7. By taking an action $H_{i}$ or $L_{i}$,
the probability mass leaves both the low and high-state of a component
$C_{i}$. In all other components, the probability mass remains. We can
represent states with extended bit-strings, concretely, we can think of

$\displaystyle\\{h_{1},l_{3},\top\mapsto\nicefrac{{1}}{{3}},l_{1},l_{2},h_{2},h_{3},\bot\mapsto
0\\}\text{ as }1\text{\char 51}0,\text{ and}$
$\displaystyle\\{\bot\mapsto\nicefrac{{2}}{{3}},l_{3},\top\mapsto\nicefrac{{1}}{{3}},l_{1},l_{2},h_{1},h_{2},h_{3},\bot\mapsto
0\\}\text{ as }\text{\char 55}\text{\char 55}0.$

We define the risk as $r(\top)=1$ and $r(s)=0$ for all $s\neq\top$. Thus, the
belief ✓✓✓ has maximal risk. Now, we show that if we have
$B\colonequals\mathcal{V}(\mathsf{est_{MDP}}(AAA))=\mathbb{B}^{n}$. Let us fix
$\mathsf{bel}\colonequals 100$. Then
$B^{\prime}=\mathsf{est_{MDP}^{up}}(B\setminus\\{\mathsf{bel}\\},H_{1}L_{2}L_{3})$
does not contain $\mathsf{bel}^{\prime}\colonequals\text{\char 51}\text{\char
51}\text{\char 51}$, but $\mathcal{V}(\mathsf{est_{MDP}}(AAAH_{1}L_{2}L_{3}))$
does. Thus, the estimated risk after $AAAH_{1}L_{2}L_{3}$ will be below the
maximum if we remove $\mathsf{bel}^{\prime}$ after seeing $AAA$.
Symmetrically, we can show that all other beliefs need to remain in $B$.∎