Reachability in Augmented Interval Markov Chains

TL;DR

This paper introduces augmented interval Markov chains (AIMCs), a flexible model for stochastic systems with uncertain and dependent transition probabilities, and analyzes the computational complexity of reachability problems within this framework.

Contribution

It extends interval Markov chains by allowing dependent transition uncertainties and provides complexity bounds for various reachability problems in AIMCs.

Findings

Exact reachability is at least as hard as the square-root sum problem.

Approximate reachability is in NP when the graph is known.

Qualitative subproblems are NP-complete with unknown graph structure.

Abstract

In this paper we propose augmented interval Markov chains (AIMCs): a generalisation of the familiar interval Markov chains (IMCs) where uncertain transition probabilities are in addition allowed to depend on one another. This new model preserves the flexibility afforded by IMCs for describing stochastic systems where the parameters are unclear, for example due to measurement error, but also allows us to specify transitions with probabilities known to be identical, thereby lending further expressivity. The focus of this paper is reachability in AIMCs. We study the qualitative, exact quantitative and approximate reachability problem, as well as natural subproblems thereof, and establish several upper and lower bounds for their complexity. We prove the exact reachability problem is at least as hard as the famous square-root sum problem, but, encouragingly, the approximate version lies in $\mathbf{NP}$ if the underlying graph is known, whilst the restriction of the exact problem to a constant number of uncertain edges is in $\mathbf{P}$. Finally, we show that uncertainty in the graph structure affects complexity by proving $\mathbf{NP}$-completeness for the qualitative subproblem, in contrast with an easily-obtained upper bound of $\mathbf{P}$ for the same subproblem with known graph structure.

Equations

$$\phi \equiv {\phi }_1\wedge {\phi }_2\wedge \cdots \wedge {\phi }_k,$$

$${\phi }_i\equiv l_{i,1}\vee l_{i,2}\vee l_{i,3}.$$

$$V$$

$$\cup \{{\phi }_1,\dots ,{\phi }_k\}$$

$$\cup \{S,F\},$$

$$\cup \{v_0,\dots ,v_m\}$$

$$\Delta (v_{i-1},x_i)=\Delta (v_{i-1},\overline{x_i})=\Delta (x_i,v_i)=$$

$$\Delta (x_i,F)=\Delta (\overline{x_i},F)=\Delta (\overline{x_i},v_i)=[0,1].$$

$$\Delta ({\phi }_i,l_{i,j})=[0,1].$$

$$\Delta (v_m,S)=\Delta (v_m,{\phi }_i)=\left[\frac{1}{k+1},\frac{1}{k+1}\right].$$

$$C=\bigcup _{i=1,\dots ,m}\{(v_{i-1},x_i,x_i,v_i),(v_{i-1},x_i,\overline{x_i},F)\}$$

$$\delta (v_{i-1},x_i)=\delta (x_i,v_i)=\delta (\overline{x_i},F)=\sigma (x_i),$$

$$\delta (v_{i-1},\overline{x_i})=\delta (\overline{x_i},v_i)=\delta (x_i,F)=1-\sigma (x_i)$$

$$p_i=\delta (v_{i-1},x_i)=\delta (x_i,v_i)=\delta (\overline{x_i},F),$$

$$1-p_i=\delta (v_{i-1},\overline{x_i})=\delta (\overline{x_i},v_i)=\delta (x_i,F).$$

$${\mathbb{P}}^M(v_0{x}_1{F}^{\omega })={\mathbb{P}}^M(v_0\overline{x_1}{F}^{\omega })=p_1(1-p_1),$$

$${\mathbb{P}}^M(v_0{x}_1{v}_1{x}_2{F}^{\omega })={\mathbb{P}}^M(v_0{x}_1{v}_1\overline{x_2}{F}^{\omega })=p_2(1-p_2),$$

$${\mathbb{P}}^M(v_0\overline{x_1}{v}_1{x}_2{F}^{\omega })={\mathbb{P}}^M(v_0\overline{x_1}{v}_1\overline{x_2}{F}^{\omega })=p_2(1-p_2).$$

$${\mathbb{P}}^M(v_0\dots v_m{\phi }_i{l}_{i,1}{F}^{\omega })=\frac{1}{k+1}\delta ({\phi }_i,l_{i,1})\delta (l_{i,1},F)\ne 0,$$

$$U=\{s,t\}\cup \{u\in V:\exists v\in V.\Delta (u,v)\text{mbox}isnotasingleton\}.$$

$${\phi }_1\equiv$$

$$\wedge$$

$$\underset{w\in W,u\in U}{\bigwedge }\alpha (w,u)=\delta (w,u)+\sum _{w^{\prime }\in W}\delta (w,w^{\prime })\alpha (w^{\prime },u),$$

$$\beta (u_1,u_2)=\delta (u_1,u_2)+\sum _{w\in W}\delta (u_1,w)\alpha (w,u_2).$$

$$\phi \equiv \exists \mathbf{x}\exists \mathbf{y}.{\phi }_1\wedge {\phi }_2\wedge {\phi }_3,$$

$${\phi }_2\equiv y(t)=1\wedge \underset{u\in U\setminus \{t\}}{\bigwedge }y(u)=\sum _{u^{\prime }\in U}\beta (u,u^{\prime })y(u^{\prime }),$$

$${\phi }_3\equiv y(s)\sim \tau ,$$

$$x^{\ast }:=\frac{3\sqrt{r}}{2M}\in (0,1).$$

$$\alpha$$

$$\beta$$

$$p_{opt}$$

$$\mathbb{P}(a\twoheadrightarrow S)$$

$$+\mathbb{P}(a{b}_3{c}_{3}S)+\mathbb{P}(a{b}_4{c}_4{d}_{4}S)$$

$$=\frac{\beta x^2(1-x)}{4}+\frac{\beta (1-x)}{4}$$

$$+\frac{\alpha x}{4}+\frac{\beta x(1-x)}{4}$$

$$=\frac{\alpha x-\beta x^3+\beta }{4}.$$

$$\frac{\alpha x^{\ast }-\beta (x^{\ast }{)}^3+\beta }{4}=\frac{\sqrt{r}}{N}+\frac{\beta }{4}=p_{opt}.$$

Full text

The focus of this paper is reachability in AIMCs. We study the qualitative, exact quantitative and approximate reachability problem, as well as natural subproblems thereof, and establish several upper and lower bounds for their complexity. We prove the exact reachability problem is at least as hard as the famous square-root sum problem, but, encouragingly, the approximate version lies in $\mathbf{NP}$ if the underlying graph is known, whilst the restriction of the exact problem to a constant number of uncertain edges is in $\mathbf{P}$. Finally, we show that uncertainty in the graph structure affects complexity by proving $\mathbf{NP}$-completeness for the qualitative subproblem, in contrast with an easily-obtained upper bound of $\mathbf{P}$ for the same subproblem with known graph structure.

I Introduction

Discrete-time Markov chains are a well-known stochastic model, one which has been used extensively to reason about software systems [CY95, HJ94, RKNP04]. They comprise a finite set of states and a set of transitions labelled with probabilities in such a way that the outgoing transitions from each state form a distribution. They are useful for modelling systems with inherently probabilistic behaviour, as well as for abstracting complexity away from deterministic ones. Thus, it is a long-standing interest of the verification community to develop logics for describing properties concerning realiability of software systems and to devise verification algorithms for these properties on Markov chains and their related generalisations, such as Markov decision processes [Bel57, Put14].

One well-known such generalisation is motivated by how the assumption of precise knowledge of a Markov chain’s transition relation often fails to hold. Indeed, a real-world system’s dynamics are rarely known exactly, due to incomplete information or measurement error. The need to model this uncertainty and to reason about robustness under perturbations in stochastic systems naturally gives rise to interval Markov chains (IMCs). In this model, uncertain transition probabilities are constrained to intervals, with two different semantic interpretations. Under the once-and-for-all interpretation, the given interval Markov chain is seen as representing an uncountably infinite collection of Markov chains refining it, and the goal is to determine whether some (or alternatively, all) refinements satisfy a given property. In contrast, the at-every-step interpretation exhibits a more game-theoretic flavour by allowing a choice over the outgoing transition probabilities prior to every move. The goal is then to determine strategies which optimise the probability of some property being satisfied. Originally introduced in [JL91], interval Markov chains have recently elicited considerable attention: see for example references [SVA06], [CHS08] and [BLW13], which study the complexity of model checking branching- and linear-time properties, as well as [DLL*+*11], where the focus is on consistency and refinement.

While IMCs are very natural for modelling uncertainty in stochastic dynamics, they lack the expressivity necessary to capture dependencies between transition probabilities arising out of domain-specific knowledge of the underlying real-world system. Such a dependency could state for example that, although the probabilities of some set of transitions are only known to lie within a given interval, they are all identical. Disregarding this information and studying only a dependence-free IMC is impractical, as allowing these transitions to vary independently of one another results in a vastly over-approximated space of possible behaviours.

Therefore, in the present paper we propose augmented interval Markov chains (AIMCs), a generalisation of IMCs which allows for dependencies of this type to be described. We study the effect of this added expressivity through the prism of the (existentially quantified) reachability problem under the once-and-for-all interpretation. Our results are the following. First, we show that the full problem is hard for both the famous square-root sum problem (Theorem 6) and for the class $\mathbf{NP}$ (Theorem 3). The former hardness is present even when the underlying graph structure is known and acyclic, whilst the latter arises even in the qualitative subproblem when transition intervals are allowed to include zero, rendering the structure uncertain. Second, assuming known structure, we show the approximate reachability problem to be in $\mathbf{NP}$ (Theorem 11). Third, we show that the restriction of the reachability problem to a constant number of uncertain (i.e. interval-valued) transitions is in $\mathbf{P}$ (Theorem 4).

II Preliminaries

II-A Markov chains

A discrete-time Markov chain or simply Markov chain (MC) is a tuple $M=(V,\delta)$ which consists of a finite set of vertices or states $V$ and a one-step transition function $\delta:V^{2}\rightarrow[0,1]$ such that for all $v\in V$, we have $\sum_{u\in V}\delta(v,u)=1$. For the purposes of specifying Markov chains as inputs to decision problems, we will assume $\delta$ is given by a square matrix of rational numbers. The transition function gives rise to a probability measure on $V^{\omega}$ in the usual way. We denote the probability of reaching a vertex $t$ starting from a vertex $s$ in $M$ by $\mathbb{P}^{M}(s\twoheadrightarrow t)$. The structure of $M$ is its underlying directed graph, with vertex set $V$ and edge set $E=\{(u,v)\in V^{2}:\delta(u,v)\neq 0\}$. Two Markov chains with the same vertex set are said to be structurally equivalent if their edge sets are identical.

An interval Markov chain (IMC) generalises the notion of a Markov chain. Formally, it is a pair $(V,\Delta)$ comprising a vertex set $V$ and a transition function $\Delta$ from $V^{2}$ to the set $\mathit{Int}_{[0,1]}$ of intervals contained in $[0,1]$. For the purposes of representing an input IMC, we will assume that each transition is given by a lower and an upper bound, together with two boolean flags indicating the strictness of the inequalities. A Markov chain $M=(V,\delta)$ is said to refine and interval Markov chain $\mathcal{M}=(V,\Delta)$ with the same vertex set if $\delta(u,v)\in\Delta(u,v)$ for all $u,v\in V$. We denote by $[\mathcal{M}]$ the set of Markov chains which refine $\mathcal{M}$. An IMC’s structure is said to be known if all elements of $[\mathcal{M}]$ are structurally equivalent. Moreover, if there exists some $\epsilon>0$ such that for all $M=(V,\delta)\in[\mathcal{M}]$ and all $u,v\in V$, either $\delta(u,v)=0$ or $\delta(u,v)>\epsilon$, then the IMC’s structure is $\epsilon$-known. An IMC can have known structure but not $\epsilon$-known structure for example by having an edge labelled with an open interval whose lower bound is [math].

An augmented interval Markov chain (AIMC) generalises the notion of an IMC further by equipping it with pairs of edges whose transition probabilities are required to be identical. Formally, an AIMC is a tuple $(V,\Delta,C)$, where $(V,\Delta)$ is an IMC and $C\subseteq V^{4}$ is a set of edge equality constraints. A Markov chain $(V,\delta)$ is said to refine an AIMC $(V,\Delta,C)$ if it refines the IMC $(V,\Delta)$ and for each $(u,v,x,y)\in C$, we have $\delta(u,v)=\delta(x,y)$. We extend the notation $[\mathcal{M}]$ to AIMCs for the set of Markov chains refining $\mathcal{M}$.

The reachability problem for AIMCs is the problem of deciding, given an AIMC $\mathcal{M}=(V,\Delta,C)$, an initial vertex $s\in V$, a target vertex $t\in V$, a threshold $\tau\in[0,1]$ and a relation $\sim\in\{\leq,\geq\}$, whether there exists $M\in[\mathcal{M}]$ such that \mathbb{P}^{M}(\mbox{s\twoheadrightarrow t})\sim\tau. The qualitative subproblem is the restriction of the reachability problem to inputs where $\tau\in\{0,1\}$.

Finally, in the approximate reachability problem, we are given a (small) rational number $\varepsilon$ and a reachability problem instance. If $\sim$ is $\geq$, our procedure is required to accept if there exists some refining Markov chain with reachability probability greater than $\tau+\varepsilon/2$, it is required to reject if all refining Markov chains have reachability probability less than $\tau-\varepsilon/2$, and otherwise it is allowed to do anything. Similarly if $\sim$ is $\leq$. Intuitively, this is a promise problem: in the given instance the optimal reachability probability is guaranteed to be outside the interval $[\tau-\varepsilon/2,\tau+\varepsilon/2]$.

II-B First-order theory of the reals

We denote by $\mathcal{L}$ the first-order language $\mathbb{R}\langle+,\times,0,1,<,=\rangle$. Atomic formulas in this language are of the form $P(x_{1},\dots,x_{n})=0$ and $P(x_{1},\dots,x_{n})>0$ for $P\in\mathbb{Z}[x_{1},\dots,x_{n}]$ a polynomial with integer coefficients. We denote by $\mathit{Th(\mathbb{R})}$ the first-order theory of the reals, that is, the set of all valid sentences in the language $\mathcal{L}$. Let $\mathit{Th^{\exists}(\mathbb{R})}$ be the existential first-order theory of the reals, that is, the set of all valid sentences in the existential fragment of $\mathcal{L}$. A celebrated result [Tar51] is that $\mathcal{L}$ admits quantifier elimination: each formula $\phi_{1}(\bar{x})$ in $\mathcal{L}$ is equivalent to some effectively computable formula $\phi_{2}(\bar{x})$ which uses no quantifiers. This immediately entails the decidability of $\mathit{Th(\mathbb{R})}$. Tarski’s original result had non-elementary complexity, but improvements followed, culminating in the detailed analysis of [Ren92]:

Theorem 1**.**

$\mathit{Th(\mathbb{R})}$* is complete for $\mathbf{2}\mbox{-}\mathbf{EXPTIME}$.* 2. 2.

$\mathit{Th^{\exists}(\mathbb{R})}$* is decidable in $\mathbf{PSPACE}$.* 3. 3.

If $m\in\mathbb{N}$ is a fixed constant and we consider only existential sentences where the number of variables is bounded above by $m$, then validity is decidable in $\mathbf{P}$.

We denote by $\exists\mathbb{R}$ the class, introduced in [SŠ11], which lies between $\mathbf{NP}$ and $\mathbf{PSPACE}$ and comprises all problems reducible in polynomial time to the problem of deciding membership in $\mathit{Th^{\exists}(\mathbb{R})}$.

II-C Square-root sum problem

The square-root sum problem is the decision problem where, given $r_{1},\dots,r_{m},k\in\mathbb{N}$, one must determine whether $\sqrt{r_{1}}+\dots+\sqrt{r_{m}}\geq k$. Originally posed in [O’R81], this problem arises naturally in computational geometry and other contexts involving Euclidean distance. Its exact complexity is open. Membership in $\mathbf{PSPACE}$ is straightforward via a reduction to the existential theory of the reals. Later this was sharpened in [ABKPM09] to $\mathbf{PosSLP}$, the complexity class whose complete problem is deciding whether a division-free arithmetic circuit represents a positive number. This class was introduced and bounded above by the fourth level of the counting hierarchy $\mathbf{CH}$ in the same paper. However, containment of the square-root sum problem in $\mathbf{NP}$ is a long-standing open question, originally posed in [GGJ76], and the only obstacle to proving membership in $\mathbf{NP}$ for the exact Euclidean travelling salesman problem. This highlights a difference between the familiar integer model of computation and the Blum-Shub-Smale Real RAM model [BSS89], under which the square-root sum is decidable in polynomial time [Tiw92]. See also [EY09] for more background.

III Qualitative case

In this section, we will focus on the qualitative reachability problem for AIMCs. We show that, whilst membership in $\mathbf{P}$ is straightforward when the underlying graph is known, uncertainty in the structure renders the qualitative problem $\mathbf{NP}$-complete.

Theorem 2**.**

The qualitative reachability problem for AIMCs with known structure is in $\mathbf{P}$.

Proof.

Let the given AIMC be $\mathcal{M}$ and $s,t$ the initial and target vertices, respectively. Since the structure $G=(V,E)$ of $\mathcal{M}$ is known, the qualitative reachability problem can be solved simply using standard graph analysis techniques on $G$. More precisely, for any $M\in[\mathcal{M}]$, $\mathbb{P}^{M}(s\twoheadrightarrow t)=1$ if and only if there is no path in $G$ which starts in $s$, does not enter $t$ and ends in a bottom strongly connected component which does not contain $t$. Similarly, $\mathbb{P}^{M}(s\twoheadrightarrow t)=0$ if and only if there is no path from $s$ to $t$ in $G$. ∎

Theorem 3**.**

The qualitative reachability problem for AIMCs is $\mathbf{NP}$-complete.

Proof.

Membership in $\mathbf{NP}$ is straightforward. The equivalence classes of $[\mathcal{M}]$ under structure equivalence are at most $2^{n^{2}}$, where $n$ is the number of vertices, since for each pair $(u,v)$ of vertices, either an edge $(u,v)$ is present in the structure or not. This upper bound is exponential in the size of the input. Thus, we can guess the structure of the Markov chain in nondeterministic polynomial time and then proceed to solve an instance of the qualitative reachability problem on an AIMC with known structure in polynomial time by Theorem 2.

We now proceed to show $\mathbf{NP}$-hardness using a reduction from 3-SAT. Suppose we are given a propositional formula $\varphi$ in 3-CNF:

[TABLE]

where each clause is a disjunction of three literals:

[TABLE]

Let the variables in $\varphi$ be $x_{1},\dots,x_{m}$.

Let $\mathcal{M}=(V,\Delta,C)$ be the following AIMC, also depicted in Figure 1. The vertex set has $3m+k+3$ vertices:

[TABLE]

that is, one vertex for each possible literal over the given variables, one vertex for each clause, two special sink vertices $S,F$ (success and failure) and $m+1$ auxiliary vertices. Through a slight abuse of notation, we use $x_{i},\overline{x_{i}}$ to refer both to the literals over the variable $x_{i}$ and to their corresponding vertices in $\mathcal{M}$, and similarly, $\varphi_{i}$ denotes both the clause in the formula and its corresponding vertex.

The transitions are the following. For all $i\in\{1,\dots,m\}$, we have:

[TABLE]

For all $i\in\{1,\dots,k\}$ and $j\in\{1,\dots,3\}$, we have:

[TABLE]

For all $i\in\{1,\dots,k\}$,

[TABLE]

Finally, $\Delta(S,S)=\Delta(F,F)=[1,1]$. For all other pairs of vertices $u,v$, we have $\Delta(u,v)=[0,0]$.

The edge equality constraints are:

[TABLE]

Intuitively, the sequence of ‘diamonds’ comprised by $v_{0},\dots,v_{m}$ and the vertices corresponding to literals is a variable setting gadget. Choosing transition probabilities $\delta(v_{i-1},x_{i})=\delta(x_{i},v_{i})=1$, and hence necessarily $\delta(x_{i},F)=0$, corresponds to setting $x_{i}$ to true, whereas $\delta(v_{i-1},\overline{x_{i}})=\delta(\overline{x_{i}},v_{i})=1$ and $\delta(\overline{x_{i}},F)=0$ corresponds to setting $x_{i}$ to false. On the other hand, the branching from $v_{m}$ into $\varphi_{1},\dots,\varphi_{k}$ and the edges from clauses to their literals makes up the assignment testing gadget. Assigning non-zero probability to the edge $(\varphi_{i},l_{i,j})$ corresponds to selecting the literal $l_{i,j}$ as witness that the clause $\varphi_{i}$ is satisfied.

Formally, we claim that there exists a Markov chain $M\in[\mathcal{M}]$ such that $\mathbb{P}^{M}(v_{0}\twoheadrightarrow S)=1$ if and only if $\varphi$ is satisfiable.

Suppose first that $\varphi$ is satisfiable and choose some satisfying assignment $\sigma:\{x_{1},\dots,x_{m}\}\rightarrow\{0,1\}$. Let $M=(V,\delta)\in[\mathcal{M}]$ be the refining Markov chain which assigns the following transition probabilities to the interval-valued edges of $\mathcal{M}$. First, let

[TABLE]

for all $i\in\{1,\dots,m\}$. Second, for each clause $\varphi_{i}$, choose some literal $l_{i,j}$ which is true under $\sigma$ and set $\delta(\varphi_{i},l_{i,j})=1$ and consequently $\delta(\varphi_{i},l)=0$ for the other literals $l$. Now we can observe that the structure of $M$ has two bottom strongly-connected components, namely $\{S\}$ and $\{F\}$, and moreover, $F$ is unreachable from $v_{0}$. Therefore, $\mathbb{P}^{M}(v_{0}\twoheadrightarrow S)=1$.

Conversely, suppose there exists some $M=(V,\delta)\in[\mathcal{M}]$ such that $\mathbb{P}^{M}(v_{0}\twoheadrightarrow S)=1$. We will prove that $\varphi$ has a satisfying assignment. For each $i\in\{1,\dots,m\}$, write

[TABLE]

Notice that

[TABLE]

so we can conclude $p_{1}\in\{0,1\}$, otherwise $\mathbb{P}^{M}(v_{0}\twoheadrightarrow S)\neq 1$, a contradiction. If $p_{1}=1$, then

[TABLE]

whereas if $p_{1}=0$, then

[TABLE]

Either way, we must have $p_{2}\in\{0,1\}$ to ensure $\mathbb{P}^{M}(v_{0}\twoheadrightarrow S)=1$. Unrolling this argument further shows $p_{i}\in\{0,1\}$ for all $i$. In particular, there is exactly one path from $v_{0}$ to $v_{m}$ and it has probability $1$. Let $\sigma$ be the truth assignment $x_{i}\rightarrow p_{i}$, we show that $\sigma$ satisfies $\varphi$. Indeed, if some clause $\varphi_{i}$ is unsatisfied under $\sigma$, then its three literals $l_{i,1},\dots,l_{i,3}$ are all unsatisfied, so $\delta(l_{i,j},F)>0$ for all $j=1,\dots,3$. Moreover, for at least one of these three literals, say $l_{i,1}$, we will have $\delta(\varphi_{i},l_{i,1})>0$, so the path $v_{0}\dots v_{m}\varphi_{i}l_{i,1}F^{\omega}$ will have non-zero probability:

[TABLE]

which contradicts $\mathbb{P}^{M}(v_{0}\twoheadrightarrow S)=1$. Therefore, $\sigma$ satisfies $\varphi$, which completes the proof of $\mathbf{NP}$-hardness and of the Theorem.

∎

IV Constant number of uncertain edges

We now shift our attention to the subproblem of AIMC reachability which arises when the number of interval-valued transitions is fixed, that is, bounded above by some absolute constant. Our result is the following.

Theorem 4**.**

Fix a constant $N\in\mathbb{N}$. The restriction of the reachability problem for AIMCs to inputs with at most $N$ interval-valued transitions lies in $\mathbf{P}$. Hence, the approximate reachability problem under the same restriction is also in $\mathbf{P}$.

Proof.

Let $\mathcal{M}=(V,\Delta,C)$ be the given AIMC and suppose we wish to decide whether there exists $M\in[\mathcal{M}]$ such that $\mathbb{P}^{M}(s\twoheadrightarrow t)\sim\tau$. Let $U\subseteq V$ be the set of vertices which have at least one interval-valued outgoing transition, together with $s$ and $t$:

[TABLE]

Notice that $|U|\leq N+2=\mathit{const}$. Write $W=V\setminus U$, so that $\{U,W\}$ is a partition of $V$.

Let $\mathbf{x}$ be a vector of variables, one for each interval-valued transition of $\mathcal{M}$. For vertices $v_{1},v_{2}$, let $\delta(v_{1},v_{2})$ denote the corresponding variable in $\mathbf{x}$ if the transition $(v_{1},v_{2})$ is interval-valued, and the only element of the singleton set $\Delta(v_{1},v_{2})$ otherwise. Let $\varphi_{1}$ be the following propositional formula over the variables $\mathbf{x}$ which captures the set of ‘sensible’ assignments:

[TABLE]

There is clearly a bijection between $[\mathcal{M}]$ and assignments of $\mathbf{x}$ which satisfy $\varphi_{1}$.

For vertices $v_{1},v_{2}$, use the notation $v_{1}\rightsquigarrow v_{2}$ to denote the event ‘$v_{2}$ is reached from $v_{1}$ along a path consisting only of vertices in $W$, with the possible exception of the endpoints $v_{1},v_{2}$’. Notice that for all $u\in U$ and $w\in W$, $\mathbb{P}^{M}(w\rightsquigarrow u)$ is independent of the choice of $M\in[\mathcal{M}]$. Denote these probabilities by $\alpha(w,u)$. They satisfy the system

[TABLE]

which is linear and therefore easy to solve with Gaussian elimination. Thus, assume that we have computed $\alpha(w,u)\in\mathbb{Q}$ for all $w\in W$ and $u\in U$.

Similarly, for all $u_{1},u_{2}\in U$, write $\beta(u_{1},u_{2})$ for the probability of $u_{1}\rightsquigarrow u_{2}$. Notice that $\beta(u_{1},u_{2})$ is a polynomial of degree at most $1$ over the variables $\mathbf{x}$, given by

[TABLE]

Thus, assume we have computed symbolically $\beta(u_{1},u_{2})\in\mathbb{Q}[\mathbf{x}]$ for all $u_{1},u_{2}\in U$.

Finally, for each $u\in U$, let $y(u)$ be a variable and write $\mathbf{y}$ for the vector of variables $y(u)$ in some order. Consider the following formula in the existential first-order language of the real field:

[TABLE]

where

[TABLE]

and $\varphi_{1}$ is as above. Intuitively, $\varphi_{1}$ states that the variables $\mathbf{x}$ descibe a Markov chain in $[\mathcal{M}]$, $\varphi_{2}$ states that $\mathbf{y}$ gives the reachability probabilities from $U$ to $t$, and $\varphi_{3}$ states that the reachability probability from $s$ to $t$ meets the required threshold $\tau$. The problem instance is positive if and only if $\varphi$ is a valid sentence in the existential theory of the reals, which is decidable. Moreover, the formula uses exactly $2|U|\leq 2(N+2)=\mathit{const}$ variables, so by Theorem 1, the problem is decidable in polynomial time, as required. ∎

Notice that removing the assumption of a constant number of interval-valued transitions only degrades the complexity upper bound, but not the described reduction to the problem of checking membership in $\mathit{Th^{\exists}(\mathbb{R})}$. As an immediate corollary, we have:

Theorem 5**.**

The reachability problem and the approximate reachability problem for AIMCs are in $\exists\mathbb{R}$.

Note that Theorem 5 can be shown much more easily, without the need to consider separately $U$-vertices and $W$-vertices as in the proof of Theorem 4. It is sufficient to use one variable per interval-valued transition to capture its transition probability as above and one variable per vertex to express its reachability probability to the target. Then write down an existentially quantified formula with the the usual system of equations for reachability in a Markov chain obtained by conditioning on the first step from each vertex. While this easily gives the $\exists\mathbb{R}$ upper bound, it uses at least $|V|$ variables, so it is insufficient for showing membership in $\mathbf{P}$ for the restriction to a constant number of interval-valued transitions.

V Hardness for square-root sum problem

In this section, we give a lower bound for the AIMC reachability problem. This bound remains in place even when the structure of the AIMC is $\epsilon$-known and acyclic, except for the self-loops on two sink vertices.

Theorem 6**.**

The AIMC reachability problem is hard for the square-root sum problem, even when the structure of the AIMC is $\epsilon$-known and is acyclic, except for the self-loops on two sink vertices.

Proof.

The reduction is based on the gadget depicted in Figure 2. It is an AIMC with two sinks, $S$ and $F$ (success and failure), each with a self-loop with probability $1$, and $12$ vertices: $\{a,b_{1},\dots,b_{4},c_{1},\dots,c_{4},d_{1},d_{4},e\}$. The structure is acyclic and comprises four chains leading to $S$, namely, $ab_{1}c_{1}d_{1}eS$, $ab_{2}c_{2}S$, $ab_{3}c_{3}S$ and $ab_{4}c_{4}d_{4}S$. From each vertex other than $a$ and $S$ there is also a transition to $F$.

The probabilities are as follows. The transition $(b_{3},c_{3})$ has probability $\alpha$, whilst $(b_{1},c_{1})$, $(b_{2},c_{2})$, $(b_{4},c_{4})$ have probability $\beta$, for rationals $\alpha,\beta$ to be specified later. Consequently, the remaining outgoing transition to $F$ out of each $b_{i}$ has probability $1-\alpha$ or $1-\beta$. The transitions $(a,b_{i})$ for $i=1,\dots,4$ all have probability $1/4$. Finally, the transitions $(c_{1},F)$, $(c_{2},F)$, $(c_{3},S)$, $(c_{4},F)$, $(d_{1},e)$, $(d_{4},S)$ and $(e,S)$ are interval-valued and must all have equal probability in any refining Markov chain. Assign the variable $x$ to the probability of these transitions. The interval to which these transition probabilities are restricted (i.e. the range of $x$) is to be specified later. Consequently, the remaining transitions $(c_{1},d_{1})$,$(d_{1},F)$,$(e,F)$,$(c_{2},S)$, $(c_{3},F)$,$(c_{4},d_{4})$,$(d_{4},F)$ are also interval-valued, with probability $1-x$.

Let $M$ be a positive integer large enough to ensure

[TABLE]

Then choose a positive integer $N$ large enough, so that

[TABLE]

Now, a straightforward calculation shows

[TABLE]

Analysing the derivative of this cubic, we see that $\mathbb{P}(a\twoheadrightarrow S)$ increases on $[0,x^{*})$, has its maximum at $x=x^{*}$ and then decreases on $(x^{*},1]$. This maximum is

[TABLE]

Thus, if we choose some closed interval which contains $x^{*}$ but not [math] and $1$ to be the range of $x$, then the gadget described thus far will have $\epsilon$-known structure and maximum reachability probability from $a$ to $S$ given by $\sqrt{r}$ scaled by a constant and offset by another constant.

Now, suppose we wish to decide whether $\sqrt{r_{1}}+\dots+\sqrt{r_{m}}\geq k$ for given positive integers $r_{1},\dots,r_{m}$ and $k$. Construct a gadget as above for each $r_{i}$. The constants $\alpha,N,M$ are shared across the gadgets, as are the sinks $S,F$, but each gadget has its own constant $\beta_{i}$ in place of $\beta$, and its own copy of each non-sink vertex. The edge equality constraints are the same as above within each gadget, and there are no equality constraints across gadgets. Assign a variable $x_{i}$ to those edges in the $i$-th gadget which in the description above were labelled $x$, and choose a range for $x_{i}$ as described above for $x$. Finally, add a new initial vertex $v_{0}$, with $m$ equiprobable outgoing transitions to the $a$-vertices of the gadgets.

In this AIMC, the probability of $v_{0}\twoheadrightarrow S$ is given by the multivariate polynomial

[TABLE]

whose maximum value on $[0,1]^{m}$ is

[TABLE]

Therefore, $\sqrt{r_{1}}+\dots+\sqrt{r_{m}}\geq k$ if and only if there exists a refining Markov chain of this AIMC with

[TABLE]

so the reduction is complete. ∎

Remark 7*.*

It is easy to see that if we are given an acyclic AIMC with the interval-valued edges labelled with variables, the reachability probabilities from all vertices to a single target vertex are multivariate polynomials and can be computed symbollically with a backwards breadth-first search from the target. Then optimising reachability probabilities reduces to optimising the value of a polynomial over given ranges for its variables.

It is interesting to observe that a reduction holds in the other direction as well. Suppose we wish to decide whether there exist values of $x_{1}\in I_{1},\dots,x_{n}\in I_{n}$ such that $P(x_{1},\dots,x_{n})\geq\tau$ for a given multivariate polynomial $P$, intervals $I_{1},\dots,I_{n}\subseteq[0,1]$ and $\tau\in\mathbb{Q}$. Notice that $P$ can easily be written in the form $P(x_{1},\dots,x_{n})=\beta+N\sum_{i=1}^{m}\alpha_{i}Q_{i}(x_{1},\dots,x_{n})$, where $N>0$, $\alpha_{1},\dots,\alpha_{m}\in(0,1)$ are constants such that $\sum_{i=1}^{m}\alpha_{i}\leq 1$, each $Q_{i}$ is a non-empty product of terms drawn from $\bigcup_{j=1}^{n}\{x_{j},(1-x_{j})\}$, and $\beta$ is a (possibly negative) constant term. For example, the monomial $-2x_{1}x_{2}x_{3}$ has a negative coefficient, so rewrite it as $2(1-x_{1})x_{2}x_{3}+2(1-x_{2})x_{3}+2(1-x_{3})-2$. Do this to all monomials with a negative coefficient, then choose an appropriately large $N$ to obtain the desired form.

Now it is easy to construct an AIMC with two sinks $S,F$ and a designated initial vertex $v_{0}$ where the probability of $v_{0}\twoheadrightarrow S$ is $\sum_{i=1}^{m}\alpha_{i}Q_{i}$. We use a chain to represent each $Q_{i}$, and then branch from $v_{0}$ into the first vertices of the chains with distribution given by the $\alpha_{i}$. There exist values of the $x_{i}$ in their appropriate intervals such that $P(x_{1},\dots,x_{n})\geq\tau$ if and only if there exists a refining Markov chain such that $\mathbb{P}(v_{0}\twoheadrightarrow S)\geq(\tau-\beta)/N$.

VI Approximate case

In this section, we focus on the approximate reachability problem for AIMCs. To obtain our upper bound, we will use a result from [Cha12].

Definition 8**.**

If $M_{1}=(V,\delta_{1})$ and $M_{2}=(V,\delta_{2})$ are Markov chains with the same vertex set, then their absolute distance is

[TABLE]

Lemma 9**.**

(Appears in [Cha12].) Let $M_{1}=(V,\delta_{1})$ and $M_{2}=(V,\delta_{2})$ be structurally equivalent Markov chains, where $n=|V|$ and for all $u,v\in V$, we have either $\delta_{1}(u,v)=0$ or $\delta_{1}(u,v)\geq\epsilon$. Let also $d\leq\mathit{dist}_{A}(M_{1},M_{2})$ and fix two vertices $s,t\in V$. Then

[TABLE]

We will also need the following well-known inequality:

Lemma 10**.**

For all $x\geq-1$ and $r\in[0,1]$, we have

[TABLE]

Now we proceed to prove our upper bound.

Theorem 11**.**

The approximate reachability problem for AIMCs with $\epsilon$-known structure is in $\mathbf{NP}$.

Proof.

Let $\mathcal{M}$ be the given AIMC and let $\epsilon>0$ be a lower bound on all non-zero transitions across all $M\in[\mathcal{M}]$. Suppose we are solving the maximisation version of the problem: we are given vertices $s,t$ and a rational $\varepsilon>0$, we must accept if $\mathbb{P}^{M}(s\twoheadrightarrow t)>\tau+\varepsilon/2$ for some $M\in[\mathcal{M}]$ and we must reject if $\mathbb{P}^{M}(s\twoheadrightarrow t)<\tau-\varepsilon/2$ for all $M\in[\mathcal{M}]$.

Let $n$ be the number of vertices and let

[TABLE]

For each interval-valued transition, split its interval into at most $1/d$ intervals of length at most $d$ each. For example, $[l,r]$ partitions into $[l,l+d),[l+d,l+2d),\dots,[l+kd,r]$, where $k$ is the largest natural number such that $l+kd\leq r$. Call the endpoints defining these subintervals grid points. Let $\langle\mathcal{M}\rangle\subseteq[\mathcal{M}]$ be the set of Markov chains refining $\mathcal{M}$ such that the probabilities of all interval-valued transitions are chosen from among the grid points. Observe that for all $M_{1}\in[\mathcal{M}]$, there exists $M_{2}\in\langle\mathcal{M}\rangle$ such that $\mathit{dist}_{A}(M_{1},M_{2})\leq d$.

Our algorithm showing membership in $\mathbf{NP}$ will be the following. We will choose $M\in\langle\mathcal{M}\rangle$ nondeterministically and compute $p:=\mathbb{P}^{M}(s\twoheadrightarrow t)$ using Gaussian elimination. Then if $p\geq\tau-\varepsilon/2$, we will accept, and otherwise we will reject.

To complete the proof, we need to argue two points. First, that $\langle\mathcal{M}\rangle$ is at most exponentially large in the size of the input, so that $M$ can indeed be guessed in nondeterministic polynomial time. Second, that if for all $M\in\langle\mathcal{M}\rangle$ we have $\mathbb{P}^{M}(s\twoheadrightarrow t)<\tau-\varepsilon/2$, then it is safe to reject, that is, there is no $M^{\prime}$ with $\mathbb{P}^{M^{\prime}}(s\twoheadrightarrow t)\geq\tau+\varepsilon/2$. (Note that the procedure is obviously correct when it accepts.)

To the first point, we apply Lemma 10 with $x=-\varepsilon/(\varepsilon+1)$ and $r=1/2n$:

[TABLE]

and hence,

[TABLE]

This upper bound is a polynomial in $n$, $1/\varepsilon$ and $1/\epsilon$, and hence at most exponential in the length of the input data. Therefore, for each interval-valued transition, we can write down using only polynomially many bits which grid point we wish to use for the probability of that transition. Since the number of transitions is polynomial in the length of the input, it follows that an element of $\langle\mathcal{M}\rangle$ may be specified using only polynomially many bits, as required.

To the second point, consider $M_{1},M_{2}\in[\mathcal{M}]$ such that $\mathit{dist}_{A}(M_{1},M_{2})\leq d$. Then by Lemma 9, we have

[TABLE]

In other words, changing the transition probabilities by at most $d$ does not alter the reachability probability from $s$ to $t$ by more than $\varepsilon$. However, recall that we chose $\langle\mathcal{M}\rangle$ in such a way that for all $M_{1}\in[\mathcal{M}]$, there is some $M_{2}\in\langle\mathcal{M}\rangle$ with $\mathit{dist}_{A}(M_{1},M_{2})\leq d$. In particular, if $\mathbb{P}^{M_{2}}(s\twoheadrightarrow t)<\tau-\varepsilon/2$ for all $M_{2}\in\langle\mathcal{M}\rangle$, then certainly $\mathbb{P}^{M_{1}}(s\twoheadrightarrow t)<\tau+\varepsilon/2$ for all $M_{1}\in[\mathcal{M}]$, so it is safe to reject. This completes the proof. ∎