Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems

TL;DR

This paper introduces a method for verifying mixed monotone stochastic systems against omega-regular specifications by constructing finite-state interval-valued Markov chain abstractions and iteratively refining them based on specification-guided analysis.

Contribution

It presents a novel abstraction and verification framework for mixed monotone stochastic systems using interval Markov chains and a specification-guided refinement process.

Findings

Efficient computation of finite-state abstractions for mixed monotone systems.

Successful verification of complex specifications using the proposed method.

Case study demonstrating practical applicability and effectiveness.

Abstract

This paper addresses the problem of verifying discrete-time stochastic systems against omega-regular specifications using finite-state abstractions. Omega-regular properties allow specifying complex behavior and encompass, for example, linear temporal logic. We focus on a class of systems with mixed monotone dynamics. This class has recently been show to be amenable to efficient reachable set computation and models a wide-range of physically relevant systems. In general, finite-state abstractions of continuous state stochastic systems give rise to augmented Markov Chains wherein the probabilities of transition between states are restricted to an interval. We present a procedure to compute a finite-state Interval-valued Markov Chain abstraction of discrete-time, mixed monotone stochastic systems subject to affine disturbances given a rectangular partition of the state-space. Then, we suggest an algorithm for performing verification against omega-regular properties in IMCs. Specifically, we aim to compute bounds on the probability of satisfying the specification of interest from any initial state in the IMC. This is achieved by solving a reachability problem on sets of so-called winning and losing components in the Cartesian product between the IMC and a Rabin automaton representing the specification. Next, the verification of IMCs may yield a set of states whose acceptance status is undecided with respect to the specification, requiring a refinement of the abstraction. We describe a specification-guided approach that compares the best-case and worst-case behaviors of accepting paths in the IMC and targets the appropriate states accordingly. Finally, we show a case study.

Equations

$$x[k+1]=\mathcal{F}(x[k],w[k])$$

$$x\models {\mathcal{P}}_{\bowtie p_{sat}}[\Psi ]\iff p_{\Psi }^x\bowtie p_{sat},$$

$$\varphi ={\mathcal{P}}_{\bowtie p_{sat}}[\Psi ].$$

$$\sum _{Q_{\ell }\in Q}\text{ooalign}\text{raise}7.09259pt\text{scalebox}1.0[-1.0]\text{lower}7.09259pt\widehat{\text{vrule}width=0.0pt,height=6.83331pt\text{vrule}height=0.0pt,width=7.23265pt}\text{cr}T(Q_j,Q_{\ell })\le 1\le \sum _{Q_{\ell }\in Q}\hat{T}(Q_j,Q_{\ell })$$

$${\text{ooalign}\text{raise}7.09259pt\text{scalebox}1.0[-1.0]\text{lower}7.09259pt\widehat{\text{vrule}width=0.0pt,height=6.83331pt\text{vrule}height=0.0pt,width=7.23265pt}\text{cr}T}_{Q_j\to Q_{\ell }}$$

$${\hat{T}}_{Q_j\to Q_{\ell }}$$

$$Q_j\models {\mathcal{P}}_{\bowtie p_{sat}}[\Psi ]\iff (p_{\Psi }^{Q_j}{)}_{\nu }\bowtie p_{sat}\forall \nu \in {\nu }_{\mathcal{I}},$$

$$x[k+1]=\mathcal{F}(x[k])+w[k]$$

$$\{\mathcal{F}(x):a\le x\le b\}\subseteq \{z:g(a,b)\le z\le g(b,a)\}.$$

$$\underset{x\in Q_1}{\min }Pr(\mathcal{F}(x)+w\in Q_2)$$

$$\ge \prod _{i=1}^n\underset{\begin{array}{c}{z}_i\in [g_i(a^1,b^1),g_i(b^1,a^1)]\end{array}}{\min }{\int }_{a_i^2}^{b_i^2}{f}_{w_i}(x-z_i)dx$$

$$\underset{x\in Q_1}{\max }Pr(\mathcal{F}(x)+w\in Q_2)$$

$$\le \prod _{i=1}^n\underset{\begin{array}{c}{z}_i\in [g_i(a^1,b^1),g_i(b^1,a^1)]\end{array}}{\max }{\int }_{a_i^2}^{b_i^2}{f}_{w_i}(x-z_i)dx$$

$$s_{max}=\frac{a+b}{2}-c$$

$$s_{max}^r$$

$$s_{min}^r$$

$$\underset{s\in [r_1,r_2]}{\max }{\int }_a^b{f}_{\omega }(x-s)dx$$

$$\underset{s\in [r_1,r_2]}{\min }{\int }_a^b{f}_w(x-s)dx$$

$$s_{i,max}^{\ell }$$

$${\text{ooalign}\text{raise}6.25pt\text{scalebox}1.0[-1.0]\text{lower}6.25pt\widehat{\text{vrule}width=0.0pt,height=4.30554pt\text{vrule}height=0.0pt,width=4.78937pt}\text{cr}r}^j$$

$${\hat{r}}^j$$

$${\hat{T}}_{Q_j\to Q_{\ell }}$$

$$\displaystyle=\prod_{i=1}^{n}\bigg{(}F_{w_{i}}(b^{\ell}_{i}-s_{i,max}^{j\rightarrow\ell})-F_{w_{i}}(a^{\ell}_{i}-s_{i,max}^{j\rightarrow\ell})\bigg{)},$$

$${\text{ooalign}\text{raise}7.09259pt\text{scalebox}1.0[-1.0]\text{lower}7.09259pt\widehat{\text{vrule}width=0.0pt,height=6.83331pt\text{vrule}height=0.0pt,width=7.23265pt}\text{cr}T}_{Q_j\to Q_{\ell }}$$

$$\displaystyle=\prod_{i=1}^{n}\bigg{(}F_{w_{i}}(b^{\ell}_{i}-s_{i,min}^{j\rightarrow\ell})-F_{w_{i}}(a^{\ell}_{i}-s_{i,min}^{j\rightarrow\ell})\bigg{)}$$

$$s_{i,max}^{j\to \ell }$$

$$s_{i,min}^{j\to \ell }$$

$${\text{ooalign}\text{raise}7.09259pt\text{scalebox}1.0[-1.0]\text{lower}7.09259pt\widehat{\text{vrule}width=0.0pt,height=6.83331pt\text{vrule}height=0.0pt,width=6.80557pt}\text{cr}\mathcal{P}}_{\mathcal{I}}(Q_j\models \Psi )\le {\mathcal{P}}_{\mathcal{I}[\nu ]}(Q_j\models \Psi )\le {\hat{\mathcal{P}}}_{\mathcal{I}}(Q_j\models \Psi ).$$

$$\exists i:$$

$$\displaystyle\wedge\Big{(}\;\forall\left<Q_{j},s_{\ell}\right>\in B\;.\;E_{i}\not\in L^{\prime}(\left<Q_{j},s_{\ell}\right>)\;\Big{)}.$$

$$\underset{\nu \in {\nu }_{\mathcal{I}}}{\inf }{\mathcal{P}}_{\mathcal{I}[\nu ]}(Q_i\models \Psi )$$

$$\underset{\nu \in {\nu }_{\mathcal{I}}}{\sup }{\mathcal{P}}_{\mathcal{I}[\nu ]}(Q_i\models \Psi )$$

$${\mathcal{P}}_{{\mathcal{M}}_{\otimes }^{\mathcal{A}}}(⟨Q_i,s_0⟩\models ◊U^A)$$

$${\mathcal{P}}_{{\mathcal{M}}_{\otimes }^{\mathcal{A}}}(⟨Q_i,s_0⟩\models ◊U^N)$$

$${\text{ooalign}\text{raise}7.09259pt\text{scalebox}1.0[-1.0]\text{lower}7.09259pt\widehat{\text{vrule}width=0.0pt,height=6.83331pt\text{vrule}height=0.0pt,width=6.80557pt}\text{cr}\mathcal{P}}_{\mathcal{I}}(Q_i\models \Psi )$$

$${\hat{\mathcal{P}}}_{\mathcal{I}}(Q_i\models \Psi )$$

$$x_1[k+1]$$

$$x_2[k+1]$$

Full text

{IEEEkeywords}

finite-state abstractions, interval-valued Markov chains, mixed monotone systems, stochastic systems.

1 Introduction

Recent years have witnessed a growing effort to design tools for verifying and optimizing the behavior of systems with respect to increasingly complex specifications. Many efficient verification techniques can be readily applied in the context of purely deterministic models. Yet, the study of stochastic systems generally requires a machinery of its own. For example, the model checking problem for discrete-time and continuous-time Markov Chains (MC) has been solved for the Probablistic Computation Tree Logic (PCTL) and $\omega$-regular properties [1] [2] [3]. Numerous off-the-shelf tools, such as PRISM [4], can efficiently verify MCs for a wide range of specifications.

However, these MC models assume that the probabilities of transition between states are known exactly. While computationally convenient, such representations may not be realistic in practice. In particular, the verification of continuous state systems is often performed by partitioning its domain into a discrete set of states. Because these states abstract a collection of continuous behaviors simultaneously, modeling a stochastic finite-state abstraction as a transition system can be challenging. One approach uses approximate Markov chains [5] as in the FAUST2 model checker [6], where each discrete state is reduced to a single representative point. Another approach uses Markov set-chains [7] to abstract the evolution of such systems so that existing techniques are applicable. Similar automata-based techniques are found in [8] and [9] for linear time objectives. However, these techniques generally rely on a fine gridding of the continuous state-space which overlooks qualitative aspects that are important to certain specifications, e.g. the creation of absorbing states as pointed out in [8]. Abstraction-based methods have been employed as well for the verification of continuous-time stochastic hybrid models against safety specifications in [10] and [11].

Instead of approximate Markov chains, finite-state abstractions of continuous state-space, discrete-time stochastic systems are also amenable to Markovian models where the probabilities of transitions are restricted to some interval [12] [13], referred to as Interval-valued Markov Chains (IMC) [14]. We consider this approach in this work. Constructing interval-valued abstractions of stochastic systems with continuous state-spaces is often a computationally expensive process. Indeed, in the general case, calculating the exact lower and upper bounds of transitions between all discrete states involves numerical searches over the state-space, rendering this procedure highly time-inefficient. Nevertheless, we aim to show that this impractical computational blowup can be avoided in some cases by exploiting the inherent structure of the system’s dynamics. Our proposed approach results in an IMC abstraction with conservative transition probability ranges, which remains sufficient for verification.

In particular, we consider a class of stochastic systems for which the dynamics exhibits a mixed monotone property [15, 16]. Mixed monotonicity generalizes the property of monotonicity for dynamical systems for which trajectories maintain a partial ordering on states [17], [18], [19]. Many physical systems have been shown to be monotone or mixed monotone such as biological systems [20] and transportation networks [21], [22], [23]. This property enables efficient computation of reachable sets: a rectangular over-approximation of the one-step reachable set from any rectangular discrete state is determined by evaluating a certain decomposition function at the least and the greatest point of that state. In this paper, we study mixed monotone systems that are subject to an affine random disturbance vector whose components are mutually independent and for which the probability distribution for each component is unimodal and symmetric. For such systems, we show that an upper bound and a lower bound on the probability of transitions between states of a rectangular partition are found by evaluating only two integrals per dimension and per transition. We use these bounds to create an IMC abstraction of the original system that is suitable for verification.

Efficient verification algorithms for IMCs have been derived for the logic PCTL [12]. However, many specifications of interest cannot be expressed using PCTL, such as liveness, i.e., the infinitely repeated occurrence of an event [24]. This motivates the implementation of a machinery for handling such properties for the class of abstractions mentioned above. As a superset of the broadly used Linear Temporal Logic (LTL), $\omega$-regular properties exhibit considerable expressiveness.

In this work, we treat the problem of verification for discrete-time, continuous-space stochastic systems against $\omega$-regular properties. To this end, we use finite state abstractions in the form of IMCs. We develop an algorithm for determining the best and worst-case outcome of the IMC by solving a reachability problem in the product between the IMC and a Rabin automaton corresponding to the specification of interest. Our approach can be decomposed into a graph search which identifies the largest and permanent so-called winning and losing components [25] in the product IMC, and the computation of bounds on the probability of reaching these components.

Such verification techniques may yield a set of states whose satisfiability status with respect to the desired specification is undecided. Previous works suggested a methodology to compute a gridding parameter that guarantees an upper bound on the size of the interval of satisfaction for all states in the resulting partition and for all specifications in the logic PCTL [5]. This parameter is a function of the system’s properties only, such as Lipschitz constants. However, this method is often conservative and likely to provide very fine partitions and is therefore computationally expensive. Instead, we apply a specification-guided refinement procedure on an initial crude partition of the state-space and iteratively produce finer IMC abstractions until some precision criterion is attained. Verification is performed on each new partition and a specific set of states is selected for the next refinement step. Refinement heuristics were proposed for the PCTL framework in [12] and [13]. We present a technique for the $\omega$-regular framework that accounts for the behavior of the paths generated by the best and worst case adversary of the IMC to refine regions of the state-space with the highest potential of reducing uncertainty.

In summary, the first contribution of this paper is an efficient procedure for constructing an IMC abstraction of stochastic mixed-monotone systems subject to affine, unimodal and symmetrical disturbances. The second contribution is a technique for computing satisfiability bounds on $\omega$-regular specifications in IMCs. The third contribution is a specification-guided refinement method that selectively and iteratively partitions certain regions of the continuous domain of stochastic systems for the purpose of verification against $\omega$-regular properties. This technique improves on other specification-guided approaches by inspecting the accepting paths produced by the worst and best case adversary of the IMC instead of observing only the one-step transitions of each state and by considering the qualitative structure of the product IMC through its largest and permanent components to target the states accordingly.

The paper is organized as follows: Section II introduces preliminaries; Section III presents the problems investigated in this paper; Section IV derives an IMC abstraction techniques for affine-in-disturbance mixed monotone systems; Section V discusses the verification of IMCs against $\omega$-regular properties; Section VI discusses state-space refinement; Section VII contains case studies; Section VIII summarizes the conclusions.

Preliminary results were reported in the conference papers [13] and [26]. The verification approach considered here is a significant improvement of these prior works. Specifically, the methodology proposed here does not require computing the complement of the system specification and presents a more advanced algorithm for partition refinement.

\IEEEpeerreviewmaketitle

2 Preliminaries

A Deterministic Rabin Automaton (DRA) [1] is a 5-tuple $\mathcal{A}=(S,\Sigma,\delta,s_{0},Acc)$ where:

• •

$S$ is a finite set of states,

• •

$\Sigma$ is an alphabet,

• •

$\delta:S\times\Sigma\rightarrow S$ is a transition function

• •

$s_{0}$ is an initial state

• •

$Acc\subseteq 2^{S}\times 2^{S}$. An element $(E_{i},F_{i})\in Acc$, with $E_{i},F_{i}\subset S$, is called a Rabin Pair.

A DRA $\mathcal{A}$ reads an infinite string or word over alphabet $\Sigma$ as an input and transitions from state to state according to $\delta$. The resulting sequence of states or run is an accepting run if it contains an infinite number of states belonging to $F_{i}$ and a finite number of states in $E_{i}$ for some $i$. A word is said to be accepted by $\mathcal{A}$ if it produces an accepting run in $\mathcal{A}$. We call a set of words a property. The property accepted by $\mathcal{A}$ is the set of all words accepted by $\mathcal{A}$.

A property over an alphabet $\Sigma$ is $\omega$-regular if and only if it is accepted by a Rabin Automaton with alphabet $\Sigma$ (for more detailed definitions of $\omega$-regular properties, see [1, Section 4.3.1]). In particular, all properties defined by a Linear Temporal Logic (LTL) formula are $\omega$-regular. See [1] for a description of the semantics of LTL.

Throughout, all inequalities are interpreted elementwise so that, for $x,y\in\mathbb{R}^{n}$, $x\leq y$ means $x_{i}\leq y_{i}$ for $i=1,\ldots,n$, and similarly for $\geq,<$ and $>$.

$Q_{j}=\{x:a^{j}\leq x\leq b^{j}\}$ for some $a^{j},b^{j}\in\mathbb{R}^{n}$ such that $a^{j}\leq b^{j}$ is a compact rectangular set and $a^{j}$, $b^{j}$ are respectively called the least point and the greatest point of $Q_{j}$. For vectors, we reserve the subscript to index elements of the vector so that, e.g., $a^{j}_{i}$ for $i\in\{1,\ldots,n\}$ denotes the $i$-th element of $a^{j}\in\mathbb{R}^{n}$.

3 Problem Formulation

We consider the discrete-time, continuous-state stochastic system

[TABLE]

where $x[k]\in D\subset\mathbb{R}^{n}$ is the state of the system at time $k$, $w[k]\in W\subset\mathbb{R}^{p}$ is a random disturbance and $\mathcal{F}:D\times W\rightarrow D$ is a continuous map. At each time-step $k$, the random disturbance $w[k]$ is sampled from a probability distribution with density function $f_{w}:\mathbb{R}^{p}\to\mathbb{R}_{\geq 0}$ satisfying $f_{w}(z)=0$ if $z\not\in W$. Let $L:D\rightarrow\Sigma$ be a labeling function, where $\Sigma$ is a finite alphabet. A random path $x[0]x[1]\ldots$ satisfying (1) generates the word $L(x[1])L(x[2])\ldots$ over $\Sigma$.

We denote by $\Psi$ an $\omega$-regular property over alphabet $\Sigma$ and define a probability operator $\mathcal{P}_{\bowtie p_{sat}}[\Psi]$ over $\omega$-regular properties, with $\bowtie\;\in\{\leq,<,\geq,>\}$, $p_{sat}\in[0,1]$. For any initial state $x\in D$, we define the satisfaction relation $\models$ where

[TABLE]

with $p^{x}_{\Psi}$ being the probability that the word generated by a random path starting in $x$ satisfies property $\Psi$ (for a rigorous formalization, see, e.g., [5]). In this paper, we concentrate on formulas of the type

[TABLE]

Our objective is to sort all initial states of system (1) into those that satisfy and those that do not satisfy specification (2), denoted by the sets $Q^{yes}_{\phi}$ and $Q^{no}_{\phi}$ respectively.

Problem: *Given a system of the form (1), find the sets of initial states $Q^{yes}_{\phi}\subseteq D$ and $Q^{no}_{\phi}\subseteq D$ that respectively satisfy and do not satisfy a formula $\phi$ of the form (2).

The domain $D$ of system (1) generally contains an uncountably infinite number of states and obtaining exact solutions to this problem may be infeasible for rich specifications. A common approximation approach consists in partitioning $D$ into a finite collection of states $P$ to obtain a finite abstraction of the stochastic dynamics. In this paper, we only consider partitions which are rectangular.

Definition 1** (Rectangular Partition)**

A rectangular partition $P$ of the compact domain $D\subset\mathbb{R}^{n}$ is a collection of discrete states $P=\{Q_{j}\}_{j=1}^{m},\;Q_{j}\subset D,$ satisfying

• •

$Q_{j}$* is a compact rectangular set $\forall j=1,\ldots,m$,*

• •

$\bigcup_{j=1}^{m}Q_{j}=D$,

• •

$\text{int}(Q_{j})\cap\text{int}(Q_{\ell})=\emptyset\;\;\forall j,\ell,\;j\not=\ell\;\;,$**

*where int denotes the interior. For any continuous state $x$ belonging to a state $Q_{j}$, we write $x\in Q_{j}$.

Henceforth, we assume that $D$ in system (1) is amenable to a rectangular partition.

Given a rectangular partition $P$ for a system (1), the likelihood of transitioning from a state $Q_{j}$ of $P$ to another state $Q_{\ell}$ generally varies with the continuous state abstracted by $Q_{j}$ from which the transition is actually taking place. This prevents using the partition $P$ to uniquely abstract (1) as a finite discrete-time MC. Instead, we produce an IMC abstraction of the system where the transition probabilities between states are constrained within some bounds. Fig. 1 depicts a schematic of a partition-based finite abstraction.

Definition 2** (Interval-Valued Markov Chain)**

An Interval-Valued Markov Chain (IMC) [13] is a 5-tuple \mathcal{I}=(Q,{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}},\widehat{T},\Sigma,L) where:

• •

$Q$* is a finite set of states,*

• •

{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}}:Q\times Q\rightarrow[0,1]* maps pairs of states to a lower transition bound so that {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}}_{Q_{j}\rightarrow Q_{\ell}}:={\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}}(Q_{j},Q_{\ell}) denotes the lower bound of the transition probability from state $Q_{j}$ to state $Q_{\ell}$, and*

• •

$\widehat{T}:Q\times Q\rightarrow[0,1]$* maps pairs of states to an upper transition bound so that $\widehat{T}_{Q_{j}\rightarrow Q_{\ell}}:=\widehat{T}(Q_{j},Q_{\ell})$ denotes the upper bound of the transition probability from state $Q_{j}$ to state $Q_{\ell}$,*

• •

$\Sigma$* is a finite set of atomic propositions,*

• •

$L:Q\rightarrow\Sigma$* is a labeling function from states to $\Sigma$,*

*and

$\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}$

$\textstyle T$ and $\widehat{T}$ satisfy {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}}(Q_{j},Q_{\ell})\leq\widehat{T}(Q_{j},Q_{\ell}) for all $Q_{j},Q_{\ell}\in Q$ and*

[TABLE]

for all $Q_{j}\in Q$.

Definition 3** (Markov Chain)**

A Markov Chain (MC) $\mathcal{M}=(Q,T,\Sigma,L)$ is defined similarly to an IMC with the difference that the transition probability function or transition matrix $T:Q\times Q\rightarrow[0,1]$ satisfies $0\leq T(Q_{j},Q_{\ell})\leq 1$ for all $Q_{j},Q_{\ell}\in Q$ and $\sum_{Q_{\ell}\in Q}T(Q_{j},Q_{\ell})=1$ for all $Q_{j}\in Q$.

A Markov Chain $\mathcal{M}=(Q,T,\Sigma,L)$ is said to be induced by IMC \mathcal{I}=(Q,{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}},\widehat{T},\Sigma,L) if they share the same $Q$, $\Sigma$ and $L$, and for all $Q_{j},Q_{\ell}\in Q$, {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}}(Q_{j},Q_{\ell})\leq T(Q_{j},Q_{\ell})\leq\widehat{T}(Q_{j},Q_{\ell}). A transition matrix $T$ satisfying this inequality is said to be induced by $\mathcal{I}$.

The notation $\mathcal{P}_{\mathcal{M}}(Q_{i}\models\Diamond U)$ for $U\subseteq Q$ denotes the probability of eventually reaching set $U$ from initial state $Q_{i}$ in Markov Chain $\mathcal{M}$. With a slight abuse of notation, when the probability of reaching $U$ is the same from all states in a set $G$, we write it as $\mathcal{P}_{\mathcal{M}}(G\models\Diamond U)$.

An IMC $\mathcal{I}$ is interpreted as an Interval Markov Decision Process (IMDP) [27] if, at each time step $k$, the environment non-deterministically chooses a transition matrix $T_{k}$ induced by $\mathcal{I}$ and the next transition occurs according to $T_{k}$. A mapping $\mathcal{\nu}$ from a finite path $\pi=q_{0}q_{1}\ldots q_{k}$ in $\mathcal{I}$ to a transition matrix $T_{k}$ is called an adversary. The set of all adversaries of $\mathcal{I}$ is denoted by $\mathcal{\nu}_{\mathcal{I}}$.

The probability of satisfying $\omega$-regular property $\Psi$ starting from initial state $Q_{i}$ in IMC $\mathcal{I}$ under adversary $\mathcal{\nu}$ is denoted by $\mathcal{P}_{\mathcal{I}[\mathcal{\nu}]}(Q_{i}\models\Psi)$. The greatest lower bound and least upper bound on the probability of satisfying property $\Psi$ starting from initial state $Q_{i}$ in IMC $\mathcal{I}$ are denoted by {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\displaystyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\textstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=4.7639pt}}}}}\cr\hbox{\scriptstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.40279pt}}}}}\cr\hbox{\scriptscriptstyle\mathcal{P}}}}}}_{\mathcal{I}}(Q_{i}\models\Psi)=\inf_{\nu\in\nu_{\mathcal{I}}}\mathcal{P}_{\mathcal{I}[\mathcal{\nu}]}(Q_{i}\models\Psi) and $\widehat{\mathcal{P}}_{\mathcal{I}}(Q_{i}\models\Psi)=\sup_{\nu\in\nu_{\mathcal{I}}}\mathcal{P}_{\mathcal{I}[\mathcal{\nu}]}(Q_{i}\models\Psi)$ respectively.

Definition 4** (IMC Abstraction)**

Given the system (1) evolving on a domain $D\subset\mathbb{R}^{n}$ and a partition $P=\{Q_{j}\}_{j=1}^{m}$ of $D$, an IMC \mathcal{I}=(Q,{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}},\widehat{T},\Sigma,L) is an abstraction of (1) if:

• •

$P=Q$, i.e., the set of states of the IMC is the partition $P$,

• •

For all $Q_{j},Q_{\ell}\in P$,

[TABLE]

where $Pr(\mathcal{F}(x,w)\in Q_{\ell})$ for fixed $x$ is the probability that (1) transitions from $x$ to a state $x^{\prime}=F(x,w)$ in $Q_{\ell}$,

• •

For all $Q_{j}\in P$ and for any two states $x_{i},x_{\ell}\in Q_{j}$, it holds that $L(Q_{j}):=L(x_{i})=L(x_{\ell})$, that is, the partition respects the boundaries induced by the labeling function,

• •

$\mathcal{I}$* is interpreted as an IMDP.*

**

The fact that two continuous states within the same discrete state of the abstraction may engender different transition probabilities is captured by interpreting the IMC as an IMDP.

One can always build a trivial IMC abstraction where all transitions are set to range from 0 to 1. The ease of finding tighter bounds on the transitions between states is dictated by the dynamics of the system and the geometry of the states in the partition. A contribution of this paper is to show that affine-in-disturbance stochastic mixed monotone systems evolving on a domain amenable to a rectangular partition can efficiently be abstracted by IMCs. A formal definition of such systems is provided in the next section.

Subproblem 1: *Given an affine-in-disturbance stochastic mixed monotone system, construct a non-trivial IMC abstraction from a rectangular partition of its domain.

Performing verification on an IMC abstraction provides probabilistic guarantees with respect to the original system’s states. A consequence of model checking an IMC $\mathcal{I}$ is that the probability of satisfying property $\Psi$ from any of its initial states $Q_{j}$ must be specified as an interval $I_{j}=[p^{j}_{min},p^{j}_{max}]$, where $\mathcal{P}_{\mathcal{I}[\mathcal{\nu}]}(Q_{j}\models\Psi)\in I_{j},\;\forall\nu\in\nu_{\mathcal{I}}$. For any initial state $Q_{j}$ in an IMC $\mathcal{I}$, we define the satisfaction relation $\models$ for formulas of the type (2) where

[TABLE]

with $(p^{Q_{j}}_{\Psi})_{\nu}$ being the probability that the word generated by a random path starting in $Q_{j}$ satisfies property $\Psi$ under adversary $\nu$. We denote the set of initial states satisfying $\phi$ in $\mathcal{I}$ by $(Q^{yes}_{\phi})_{\mathcal{I}}$, while states that do not satisfy $\phi$ are in $(Q^{no}_{\phi})_{\mathcal{I}}$. Note that any $Q_{j}$ such that $p_{sat}\in\;]p^{j}_{min},p^{j}_{max}[$ if $\bowtie\;\in\{\leq,\geq\}$, or $p_{sat}\in[p^{j}_{min},p^{j}_{max}]$ if $\bowtie\;\in\{<,>\}$, is undecided with respect to $\phi$ in (2) and we write $Q_{j}\in(Q^{?}_{\phi})_{\mathcal{I}}$. The remaining states either satisfy $\phi$ or do not satisfy $\phi$.

Fact 1

Let $\mathcal{I}$ be an IMC abstraction of (1) induced by a partition $P=\{Q_{j}\}_{j=1}^{m}$ of $D$. For any formula of the form (2), it holds that:

• •

$Q_{j}\in(Q^{yes}_{\phi})_{\mathcal{I}}\Rightarrow x\in Q^{yes}_{\phi}\;\;\forall x\in Q_{j}$**

• •

$Q_{j}\in(Q^{no}_{\phi})_{\mathcal{I}}\;\Rightarrow x\in Q^{no}_{\phi}\;\;\;\forall x\in Q_{j}\;.$**

Given an IMC abstraction $\mathcal{I}$ of (1) generated from a partition $P$ of $D$, our approach for addressing the Verification Problem is thus to implement a technique for determining non-trivial values of $p^{j}_{min}$ and $p^{j}_{max}$ and sort all states of $P$ into the sets $(Q^{yes}_{\phi})_{\mathcal{I}},(Q^{no}_{\phi})_{\mathcal{I}}$ and $(Q^{?}_{\phi})_{\mathcal{I}}$.

Subproblem 2: *Given an IMC $\mathcal{I}$ interpreted as an IMDP and an $\omega$-regular property $\Psi$, find the greatest lower bound {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\displaystyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\textstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=4.7639pt}}}}}\cr\hbox{\scriptstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.40279pt}}}}}\cr\hbox{\scriptscriptstyle\mathcal{P}}}}}}_{\mathcal{I}}(Q_{j}\models\Psi) and the least upper bound $\widehat{\mathcal{P}}_{\mathcal{I}}(Q_{j}\models\Psi)$ on the probability of satisfying $\Psi$ from any initial state $Q_{j}$ in $\mathcal{I}$.

It may be the case that the total volume of uncertain states in $Q^{?}_{\phi}$ is unsatisfactorily large due to a crude partition $P$ of the continuous state-space. In such event, we aim to produce a finer partition $P^{\prime}$ from $P$ which gives rise to a new IMC abstraction of the system with a greater number of states with tighter transition bounds between them. Verifying this finer IMC yields a decreased volume of uncertain states. This refinement procedure is applied to subsequent partitions until some discretionary level of precision is reached.

Subproblem 3: *Given a system of the form (1) with an IMC abstraction $\mathcal{I}$ of (1) and the corresponding sets $Q^{yes}_{\phi}$, $Q^{no}_{\phi}$ and $Q^{?}_{\phi}$ obtained by solving Subproblem 2, refine the partition $P$ of $D$ until a predefined threshold of precision has been met.

In order to avoid state-space explosion, a careful choice of the states to be refined in partition $P$ has to be made. In this work, we suggest a novel method for targeting the states that have the greatest potential of reducing the uncertainty of an abstraction with respect to the particular specification $\Psi$.

4 IMC Abstraction of Mixed Monotone Systems Affine in Disturbance

In this section, we study a large class of stochastic systems that proves amenable to efficient computation. In particular, we consider affine-in-disturbance systems of the form

[TABLE]

with specific assumptions on $\mathcal{F}$ and the distribution of the disturbance $w$. We introduce several definitions and specify these necessary assumptions for addressing Subproblem 1.

Definition 5** (Mixed monotone function)**

A function $\mathcal{F}:D\rightarrow D$ is mixed monotone if there exists a decomposition function $g:D\times D\rightarrow D$ satisfying [15, 16]:

• •

$\forall x\in D:\mathcal{F}(x)=g(x,x)$**

• •

$\forall x^{1},x^{2},y\in D:x^{1}\leq x^{2}$* implies $g(x^{1},y)\leq g(x^{2},y)$*

• •

$\forall x,y^{1},y^{2}\in D:y^{1}\leq y^{2}$* implies $g(x,y^{2})\leq g(x,y^{1})$*

Mixed monotonicity generalizes the notion of monotonicity in dynamical systems, which is recovered when $g(x,y)=\mathcal{F}(x)$ for all $x,y$. Systems with monotone state update maps exhibit considerable structure useful for analysis [28, 19, 18]. Systems with mixed monotone state update maps have been shown to enjoy many of these same structural properties [16, 15]. For example, for mixed monotone $\mathcal{F}$ with decomposition function $g$, for $x,y,z\in D$ satisfying $x\leq z\leq y$, we have $g(x,y)\leq\mathcal{F}(z)\leq g(y,x)$. This leads to the following proposition.

Proposition 1** ([16, Theorem 1])**

Let $\mathcal{F}:D\rightarrow D$ be mixed monotone with decomposition function $g:D\times D\rightarrow D$, and let $a,b\in D$ satisfy $a\leq b$. Then

[TABLE]

Proposition 1 implies that the one-step reachable set from the rectangular region bounded between $a$ and $b$ is overapproximated by the rectangular region bounded by the two points $g(a,b)$ and $g(b,a)$. This property will prove key for efficient computation of IMC abstractions.

Definition 6** (Unimodal symmetric distribution)**

For a random disturbance $\omega\in\Omega\subset\mathbb{R}$ with $\Omega$ an interval, its probability density function $f_{\omega}:\mathbb{R}\rightarrow\mathbb{R}$ is unimodal if $f_{\omega}$ is differentiable on $\Omega$ and there exists a unique number $c\in\mathbb{R}$, referred as the mode of the distribution, such that, for $x\in\Omega$:

• •

$x<c\Rightarrow f_{\omega}^{\prime}(x)\geq 0$,

• •

$x=c\Rightarrow f_{\omega}^{\prime}(x)=0$, and

• •

$x>c\Rightarrow f_{\omega}^{\prime}(x)\leq 0$.

We only consider distributions without a “flat” peak, that is, unimodal distributions with a unique mode $c$. The probability density function $f_{\omega}$ is symmetric if there exists a number $d\in\mathbb{R}$ such that $f_{\omega}(d-x)=f_{\omega}(d+x)$ for all $x$.

Note that if $f_{\omega}$ is unimodal with mode $c$ and symmetric, then it must be that $f_{\omega}(c-x)=f_{\omega}(c+x)$.

Henceforth, we make the following assumptions.

Assumption 1

$\mathcal{F}(x)$* in (14) is mixed monotone with decomposition function $g(x,y)$. Furthermore, the domain $D$ of (14) can be partitioned into a rectangular partition.*

Assumption 2

The random disturbance $w[k]$ in (14) is of the form $w[k]=\begin{bmatrix}w_{1}[k]&w_{2}[k]&\ldots&w_{n}[k]\end{bmatrix}^{T}$, where each $w_{i}\in W_{i}\subset\mathbb{R}$ has probability density function $f_{w_{i}}(x_{i})$, $W_{i}$ is an interval, and the collection $\{w_{i}\}_{i=1}^{n}$ is mutually independent. Denote by $F_{w_{i}}(x)=\int_{-\infty}^{x}f_{w_{i}}(\sigma)d\sigma$ the cumulative distribution function for $w_{i}$.

Assumption 3

The probability density function $f_{w_{i}}$ for each random variable $w_{i}$ is symmetric and unimodal with mode $c_{i}$.

We now address Subproblem 1 for systems of the form (14) under Assumptions 1-3. We decompose our procedure for bounding the transition probability from a state $Q_{1}$ to a state $Q_{2}$ in two steps: first, we compute the rectangular over-approximation of the $\mathcal{F}$-reachable set from state $Q_{1}$ by taking advantage of the mixed monotonicity property. Next, we determine the positions of $f_{w}$ within this rectangular region that respectively minimize and maximize its overlap with $Q_{2}$. In the next section, we exploit the characteristics of $w$ previously evoked to obtain an efficient computational procedure for computing these extremum points.

Proposition 2

Consider system (14) under Assumptions 1–3. Let $Q_{1}=\{x:a^{1}\leq x\leq b^{1}\}$ and $Q_{2}=\{x:a^{2}\leq x\leq b^{2}\}$ be two nonempty rectangular sets with least point $a^{j}$ and greatest point $b^{j}$ for $j=1,2$. Then

[TABLE]

and

[TABLE]

where $g_{i}$ denotes the $i$-th element of $g(x,y)$, the decomposition function of $\mathcal{F}$.

All proofs are found in the appendix. Before generalizing to higher dimensions, we treat a 1-dimensional version of our original problem. In Lemma 1, we prove that for a fixed interval $[a,b]\subset\mathbb{R}$, there exists a unique position for a unimodal and symmetric distribution which maximizes its integral over $[a,b]$.

Lemma 1

Let $\omega\in\Omega\subset\mathbb{R}$ with $\Omega$ an interval be a random variable with symmetric and unimodal probability density function $f_{\omega}:\mathbb{R}\rightarrow\mathbb{R}$ and mode $c\in\mathbb{R}$. For any $a,b\in\mathbb{R}$ satisfying $a\leq b$ and any $r_{1},r_{2}\in\mathbb{R}$ satisfying $r_{1}\leq r_{2}$, let

[TABLE]

and define

[TABLE]

Then

[TABLE]

When $s_{max}\in[r_{1},r_{2}]$ in Lemma 1, the lemma confirms the intuitive idea that the integral of a unimodal, symmetric distribution over some interval $I=[a,b]$ is maximized when the peak of its probability distribution lies at the center of $I$. However, for the type of systems considered in this work, the shift of such distributions will always be restricted to take values within a given rectangular set $[r_{1},r_{2}]$ so that, when $s_{max}\not\in[r_{1},r_{2}]$, the shift $s\in[r_{1},r_{2}]$ maximizing the overlap of the density function over $I$ is the one closest to the global maximizing shift $s_{max}$. Conversely, a shift $s\in[r_{1},r_{2}]$ minimizing this overlap is the one furthest from $s_{max}$.

Theorem 1 combines Lemma 1 and Proposition 2 to provide a procedure for constructing an IMC abstraction for (14) given a rectangular partition of its domain $D$.

Theorem 1

Consider system (14) under Assumptions 1–3 and let $P=\{Q_{j}\}_{j=1}^{m}$ be a rectangular partition of $D$ with each $Q_{j}=\{x:a^{j}\leq x\leq b^{j}\}$ for some $a^{j},b^{j}\in\mathbb{R}^{n}$ satisfying $a^{j}\leq b^{j}$. For all $Q_{j},Q_{\ell}\in P$, let

[TABLE]

and define

[TABLE]

where $F_{w_{i}}$ is the cumulative distribution function for $w_{i}$ and

[TABLE]

Then \mathcal{I}=(P,{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}},\widehat{T}) is an IMC abstraction of (14).

Theorem 1 provides the mathematical foundation for solving Subproblem 1. Given a system of the form $\eqref{eq:4}$ satisfying Assumptions 1 to 3, and a rectangular partition $P$, this theorem shows that an IMC abstraction of (14) can be computed efficiently. Specifically, for any state in $P$, we establish an over-approximation of its one-step reachable set by evaluating the system’s decomposition function at only two points. Finding the maximizing and minimizing shifts inside the reachable sets decouples along each coordinate and involves a number of operations that is linear in the dimension $n$ of the state-space, according to $\eqref{eq:13}$ and $\eqref{eq:14}$. Finally, we see in $\eqref{eq:15}$ and $\eqref{eq:16}$ that $n$ integral evaluations are needed per transition bound. This last step requires two evaluations of $F_{w_{i}}$ per bound for each $i$ and thus amounts to $2n$ function evaluations per bound. Because the computed over-approximations of reachable sets for mixed monotone dynamics were shown to be tight in certain cases [16], our abstraction technique is generally not as conservative as those employing Lipschitz constants [29], while being computationally efficient.

5 Verification of IMCs

In this section, we develop the machinery to address Subproblem 2. Let $\mathcal{I}$ be an IMC abstraction of (1) obtained from, e.g., the abstraction approach in Section IV for systems with specific form (14). For a formula $\phi$ of the type (2), our goal is to sort the initial states of $\mathcal{I}$ into the sets $Q^{yes}_{\phi},Q^{no}_{\phi}$ and $Q^{?}_{\phi}$. To this end, for any initial state $Q_{j}$ of $\mathcal{I}$, we require a lower bound and an upper bound on the probability of satisfying the $\omega$-regular property $\Psi$ for the probabilistic specification $\phi=\mathcal{P}_{\bowtie p_{sat}}[\Psi]$. We thus seek to compute the greatest lower bound {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\displaystyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\textstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=4.7639pt}}}}}\cr\hbox{\scriptstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.40279pt}}}}}\cr\hbox{\scriptscriptstyle\mathcal{P}}}}}}_{\mathcal{I}}(Q_{j}\models\Psi) and least upper bound $\widehat{\mathcal{P}}_{\mathcal{I}}(Q_{j}\models\Psi)$ such that, for any adversary $\nu\in\nu_{\mathcal{I}}$,

[TABLE]

Our approach draws from the verification of regular MCs against $\omega$-regular properties using automata-based methods [1, Section 10.3]. First, we generate a DRA $\mathcal{A}$ that recognizes the language induced by property $\Psi$. Such a DRA always exists. Several algorithms can generate a DRA for a large subset of $\omega$-regular expressions [30] [31]. Then, we construct the product $\mathcal{I}\otimes\mathcal{A}$ as defined below.

Definition 7** (Product Interval-valued Markov Chain)**

Let \mathcal{I}=(Q,{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}},\widehat{T},\Sigma,L) be an Interval-valued Markov Chain and $\mathcal{A}=(S,\Sigma,\delta,s_{0},Acc)$ be a Deterministic Rabin Automaton. The product \mathcal{I}\otimes\mathcal{A}=(Q\times S,{\mathchoice{{\ooalign{\hbox{\raise 7.6111pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.6111pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=8.38887pt\vrule height=0.0pt,width=8.77264pt}}}}}\cr\hbox{\displaystyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 7.6111pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.6111pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=8.38887pt\vrule height=0.0pt,width=8.77264pt}}}}}\cr\hbox{\textstyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 6.77963pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.77963pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=5.89444pt\vrule height=0.0pt,width=6.16284pt}}}}}\cr\hbox{\scriptstyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 6.32407pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.32407pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=4.52777pt\vrule height=0.0pt,width=4.71631pt}}}}}\cr\hbox{\scriptscriptstyle T^{\prime}}}}}},\widehat{T^{\prime}},Acc^{\prime},L^{\prime}) is an Interval-valued Markov Chain where:

• •

$Q\times S$* is a set of states,*

• •

$\{(Q_{j},s_{0}):Q_{j}\in Q\}$* is a finite set of initial states,*

• •

{\mathchoice{{\ooalign{\hbox{\raise 7.6111pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.6111pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=8.38887pt\vrule height=0.0pt,width=8.77264pt}}}}}\cr\hbox{\displaystyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 7.6111pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.6111pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=8.38887pt\vrule height=0.0pt,width=8.77264pt}}}}}\cr\hbox{\textstyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 6.77963pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.77963pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=5.89444pt\vrule height=0.0pt,width=6.16284pt}}}}}\cr\hbox{\scriptstyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 6.32407pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.32407pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=4.52777pt\vrule height=0.0pt,width=4.71631pt}}}}}\cr\hbox{\scriptscriptstyle T^{\prime}}}}}}_{\left<Q_{j},s\right>\rightarrow\left<Q_{\ell},s^{\prime}\right>}=\begin{cases}{\mathchoice{{\ooalign{\hbox{\raise 7.6111pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.6111pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=8.38887pt\vrule height=0.0pt,width=8.77264pt}}}}}\cr\hbox{\displaystyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 7.6111pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.6111pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=8.38887pt\vrule height=0.0pt,width=8.77264pt}}}}}\cr\hbox{\textstyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 6.77963pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.77963pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=5.89444pt\vrule height=0.0pt,width=6.16284pt}}}}}\cr\hbox{\scriptstyle T^{\prime}}}}}{{\ooalign{\hbox{\raise 6.32407pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.32407pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=4.52777pt\vrule height=0.0pt,width=4.71631pt}}}}}\cr\hbox{\scriptscriptstyle T^{\prime}}}}}}_{Q_{j}\rightarrow Q_{\ell}},\;\;\text{if}\;\;s^{\prime}=\delta(s,L(Q_{\ell}))\\ \;\;\;\;\;\;\;\;\;0,\;\;\;\;\;\;\text{otherwise}\end{cases}

• •

$\widehat{T^{\prime}}_{\left<Q_{j},s\right>\rightarrow\left<Q_{\ell},s^{\prime}\right>}=\begin{cases}\widehat{T^{\prime}}_{Q_{j}\rightarrow Q_{\ell}},\;\;\text{if}\;\;s^{\prime}=\delta(s,L(Q_{\ell}))\\ \;\;\;\;\;\;\;\;\;0,\;\;\;\;\;\;\text{otherwise}\end{cases}$

• •

$Acc^{\prime}=\{E_{1},E_{2},\ldots,E_{k},F_{1},F_{2},\ldots,F_{k}\}$* is a set of atomic propositions, where $E_{i}$ and $F_{i}$ are the sets in the Rabin pairs of $Acc$,*

• •

$L^{\prime}:Q\times S\rightarrow 2^{Acc^{\prime}}$* such that $H\in L^{\prime}(\left<Q_{j},s\right>)$ if and only if $s\in H$, for all $H\in Acc^{\prime}$ and for all $j$.*

**

A MC induced by $\mathcal{I}\otimes\mathcal{A}$ is called a product Markov Chain, and we use the notation $\mathcal{M}_{\otimes}^{\mathcal{A}}$ to denote such an induced MC.

The probability of satisfying $\Psi$ from initial state $Q_{j}$ in a discrete-time MC equals that of reaching an accepting Bottom Strongly Connected Component (BSCC) from initial state $\left<Q_{j},s_{0}\right>$ in the product MC with $\mathcal{A}$ [1].

Definition 8** (Bottom Strongly Connected Component)**

Given a Markov Chain $\mathcal{M}$ with states $Q$, a set $B\subseteq Q$ is a Bottom Strongly Connected Component (BSCC) of $\mathcal{M}$ if

• •

$B$* is strongly connected: for each pair of states $(q,t)$ in $B$, there exists a path $q_{0}q_{1}\ldots q_{n}$ such that $T(q_{i},q_{i+1})>0$, $i=0,1,\ldots,n-1$, and $q_{i}\in B$ for $0\leq i\leq n$ with $q_{0}=q,$ $q_{n}=t$,*

• •

no proper superset of $B$ is strongly connected,

• •

$\forall s\in B$, $\Sigma_{t\in B}T(s,t)=1$.

In words, every state in a BSCC $B$ is reachable from any state in $B$, and every state in $B$ only transitions to another state in $B$. Moreover, $B$ is accepting when at least one of its states maps to the accepting set of a Rabin pair, while no state in $B$ maps to the non-accepting set of that same pair.

Definition 9** (Accepting Bottom Strongly Connected Component)**

A Bottom Strongly Connected Component $B$ of a product MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$ is said to be accepting if:

[TABLE]

Definition 10** (Non-Accepting Bottom Strongly Connected Component)**

A Bottom Strongly Connected Component $B$ of a product MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$ is said to be non-accepting if it is not accepting.

We denote by $U^{A}$ and $U^{N}$ the sets of states that respectively belong to an accepting and a non-accepting BSCC in a product MC.

Note that each product MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$ induced by $\mathcal{I}\otimes\mathcal{A}$ simulates the behavior of $\mathcal{I}$ under some adversary $\mathcal{\nu}\in\mathcal{\nu}_{\mathcal{I}}$. Indeed, for any two states $Q_{j}$ and $Q_{\ell}$ in $\mathcal{I}$ and some states $s,s^{\prime},s^{\prime\prime}$ and $s^{\prime\prime\prime}$ in $\mathcal{A}$, we allow $T_{\left<Q_{j},s\right>\rightarrow\left<Q_{\ell},s^{\prime}\right>}$ and $T_{\left<Q_{j},s^{\prime\prime}\right>\rightarrow\left<Q_{\ell},s^{\prime\prime\prime}\right>}$ to assume different values in $\mathcal{M}_{\otimes}^{\mathcal{A}}$, which means that the transition probability between $Q_{j}$ and $Q_{\ell}$ may change depending on the history of the path in $\mathcal{I}$ as encoded in the state of $\mathcal{A}$.

Also, the adversary is history-independent or memoryless in the product automaton, that is, the adversary’s chosen transition probability only depends on the current states of the IMC and the DRA $\mathcal{A}$. For reachability problems in IMCs, it was shown in [32] that memoryless adversaries yield the same bounds as the memory-dependent ones. The following facts establish that, therefore, such memoryless (in the product) adversaries are sufficient for IMC verification.

Fact 2

[1, p. 792, Theorem 10.56]** [32] We denote the set of adversaries of $\mathcal{I}$ that are memoryless in the product IMC $\mathcal{I}\otimes\mathcal{A}$ by $(\mathcal{\nu}_{\mathcal{I}})_{\otimes}^{\mathcal{A}}\subseteq\mathcal{\nu}_{\mathcal{I}}$. It holds that

[TABLE]

Fact 3

For any adversary $\mathcal{\nu}\in(\mathcal{\nu}_{\mathcal{I}})_{\otimes}^{\mathcal{A}}$ in $\mathcal{I}$, it holds that $\mathcal{P}_{\mathcal{I}[\nu]}(Q_{i}\models\Psi)$ = $\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\nu}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A})$, where $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\nu}$ denotes the product MC induced by $\mathcal{I}\otimes\mathcal{A}$ corresponding to adversary $\nu$.

Consequently, computing {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\displaystyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\textstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=4.7639pt}}}}}\cr\hbox{\scriptstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.40279pt}}}}}\cr\hbox{\scriptscriptstyle\mathcal{P}}}}}}_{\mathcal{I}}(Q_{i}\models\Psi) and $\widehat{\mathcal{P}}_{\mathcal{I}}(Q_{i}\models\Psi)$ amounts to finding the product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ that respectively minimize and maximize the probability of reaching an accepting BSCC from $\left<Q_{j},s_{0}\right>$. Such reachability problems in IMCs were solved when the destination states are fixed for all induced MCs [33] [12].

However, in general, the sets $U^{A}$ and $U^{N}$ are not fixed in product IMCs and vary with the assumed values for each transition. Specifically, $U^{A}$ and $U^{N}$ are determined by transitions that are either “on” or “off”, i.e. those whose lower bound is zero and upper bound is non-zero, as seen in the example in Fig. 3: in the product MC $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ induced by $\mathcal{I}\otimes\mathcal{A}$, $U^{A}$ is $\{Q_{0},Q_{1}\}$ while $\{Q_{2}\}$ is non-accepting. In $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$, another product MC induced by $\mathcal{I}\otimes\mathcal{A}$, all states are in $U^{N}$.

The contribution of this paper to the verification of IMCs for $\omega$-regular properties is twofold. First, we show that a product IMC always induces a largest Losing Component and Winning Component. These components contain states that reach a BSCC with probability 1. Upper and lower bounds on $\Psi$ are computed by solving a reachability problem for these sets. We further introduce the notion of Permanent Losing Components and Permanent Winning Components which play a crucial role in the refinement algorithm derived in Section VI. Second, we describe a graph search algorithm to find these components.

5.1 Computation of Satisfiability Bounds in IMCs

Previous works highlighted the crucial role of BSCCs in product MCs [1, Theorem 10.56]. As the probability of reaching an accepting BSCC in a product MC determines the probability of satisfying some property in the original abstraction, we now further introduce the notions of winning and losing components. These components include states that may not belong to a BSCC but from which any path is bound to reach a BSCC.

Definition 11** (Winning/Losing Component)**

[25]** A winning (losing) component $WC\;(LC)$ of a product MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$ is a set of states satisfying $\mathcal{P}_{\mathcal{M}_{\otimes}^{\mathcal{A}}}(WC\models\Diamond U^{A})=1\;(\;\mathcal{P}_{\mathcal{M}_{\otimes}^{\mathcal{A}}}(LC\models\Diamond U^{N})=1\;)$ , where $U^{A}$ ($U^{N}$) is the set of states belonging to an accepting (non-accepting) BSCC in $\mathcal{M}_{\otimes}^{\mathcal{A}}$.

It naturally follows that the probability of eventually reaching a BSCC from some initial state is equal to that of reaching a winning or losing component.

Corollary 1

In any product MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$,

[TABLE]

For any initial state in a product IMC, our goal is thus to find induced product MCs that minimize and maximize the probability of reaching a winning component.

We refer to the technical appendix for all lemmas and proofs leading to the proposed solution. The key observation is that any product IMC induces a largest winning component and a largest losing component. The largest winning component is the set of states of the product IMC belonging to a winning component for at least one induced product MC, while the largest losing component is the analogous set for losing components. Definitions of permanent and potential components follow directly from that of largest components.

Definition 12** (Largest Winning/Losing Components)**

A state $\left<Q_{i},s_{j}\right>\in Q\times S$ of a product IMC $\mathcal{I}\otimes\mathcal{A}$ is a member of the Largest Winning (Losing) Component $(WC)_{L}$ \big{(}\;(LC)_{L}\;\big{)} if there exists a product MC induced by $\mathcal{I}\otimes\mathcal{A}$ such that $\left<Q_{i},s_{j}\right>$ is a winning (losing) component.

Definition 13** (Permanent Winning/Losing Components)**

A state $\left<Q_{i},s_{j}\right>\in Q\times S$ of a product IMC $\mathcal{I}\otimes\mathcal{A}$ is a member of the Permanent Winning (Losing) Component $(WC)_{P}$ \big{(}\;(LC)_{P}\;\big{)} of $\mathcal{I}\otimes\mathcal{A}$ if $\left<Q_{i},s_{j}\right>$ is a winning (losing) component for all product MCs induced by $\mathcal{I}\otimes\mathcal{A}$.

Definition 14** (Potential Winning/Losing Components)**

A state $\left<Q_{i},s_{j}\right>\in Q\times S$ of a product IMC $\mathcal{I}\otimes\mathcal{A}$ is a member of the Potential Winning (Losing) Component $(WC)_{?}$ \big{(}\;(LC)_{?}\;\big{)} of $\mathcal{I}\otimes\mathcal{A}$ if \left<Q_{i},s_{j}\right>\in(WC)_{L}\setminus(WC)_{P}\;\;\big{(}\left<Q_{i},s_{j}\right>\in\;(LC)_{L}\setminus(LC)_{P}\;\big{)}.

Note that the sets $(WC)_{?}$ and $(LC)_{?}$ may intersect, and by extension $(WC)_{L}$ and $(LC)_{L}$, while $(WC)_{P}$ and $(LC)_{P}$ are disjoint. An important result established in this paper is that any product IMC induces a set of product MCs where all members of the largest winning component belong to a winning component simultaneously. A product IMC induces an analogous set of product MCs for the largest losing component. We provide proofs in Lemmas 5-7 of the Appendix.

We now state the main result of this section, which establishes that bounds on the probability of satisfying an $\omega$-regular property in an IMC can be computed by solving a reachability maximization problem on a fixed set of states in a product IMC. These sets are the largest components of the product IMC. Furthermore, solving these problems induce sets of best and worst-case product MCs where the probabilities of reaching a winning component are respectively maximized and minimized for all initial states of the product IMC.

Theorem 2

Let $\mathcal{I}$ be an IMC and $\mathcal{A}$ be a Rabin Automaton corresponding to omega-regular property $\Psi$. Let $(WC)_{L}$ and $(LC)_{L}$ be the largest winning and losing components and $(WC)_{P}$ and $(LC)_{P}$ be the permanent winning and losing components of the product IMC $\mathcal{I}\otimes\mathcal{A}$. Then for any initial state $Q_{i}$ of $\mathcal{I}$,

[TABLE]

Moreover, there exists a set of induced product MCs $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{worst}}$, where, $\forall\mathcal{M}_{i}\in(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{worst}}$, the sets of all losing and winning components of $\mathcal{M}_{i}$ are $(LC)_{L}$ and $(WC)_{P}$ respectively, and, $\forall\left<Q_{i},s_{0}\right>\in(Q\times S)$, $\mathcal{P}_{\mathcal{M}_{i}}(\left<Q_{i},s_{0}\right>\models\Diamond(LC)_{L})=\widehat{\mathcal{P}}_{\mathcal{I}\otimes\mathcal{A}}(\left<Q_{i},s_{0}\right>\models\Diamond(LC)_{L})$ . Likewise, there exists a set of induced product MCs $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{best}}$, where, $\forall\mathcal{M}_{i}\in(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{best}}$, the sets of all losing and winning components of $\mathcal{M}_{i}$ are $(LC)_{P}$ and $(WC)_{L}$ respectively, and, $\forall\left<Q_{i},s_{0}\right>\in(Q\times S)$, $\mathcal{P}_{\mathcal{M}_{i}}(\left<Q_{i},s_{0}\right>\models\Diamond(WC)_{L})=\widehat{\mathcal{P}}_{\mathcal{I}\otimes\mathcal{A}}(\left<Q_{i},s_{0}\right>\models\Diamond(WC)_{L})$.

Proof 5.3**.**

{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\displaystyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=6.80557pt}}}}}\cr\hbox{\textstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=4.7639pt}}}}}\cr\hbox{\scriptstyle\mathcal{P}}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.40279pt}}}}}\cr\hbox{\scriptscriptstyle\mathcal{P}}}}}}_{\mathcal{I}}(Q_{i}\models\Psi)* is equivalent to a lower bound on the probability of reaching an accepting BSCC from $\left<Q_{i},s_{0}\right>$ in $\mathcal{I}\otimes\mathcal{A}$. Equation (70) follows from Lemma 3 and the following reasoning: assume (70) is not true. This implies that there exists an induced product MC where the probability of reaching an non-accepting BSCC from $\left<Q_{i},s_{0}\right>$ is greater than the highest probability of reaching $(LC)_{L}$, which is a contradiction to Lemma 5 and 9. Next, we denote by $\mathcal{D}$ the set of induced product MCs with set of winning components $(WC)_{P}$ and set of losing components $(LC)_{L}$ constructed in Lemma 10. Lemma 8 and Lemma 9 guarantee that the probability of reaching an accepting BSCC from all $\left<Q_{i},s_{0}\right>$ is minimized in induced product MCs with the smallest set of winning components and the largest set of losing components respectively. Therefore, $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{worst}}\subseteq\mathcal{D}$. Equation (71) and the existence of $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{best}}$ are proved identically.*

The equalities highlighted by this theorem are central to the elaboration of our verification procedure. We first solve a qualitative problem, which is to find the largest components of the product IMC. This can be achieved via graph search and will be the focus of the next section. Then, we compute upper and lower bound probabilities of reaching these components from all states in the product IMC using existing algorithms found in the literature [33] [12] . By doing so, we construct a best-case product MC $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}\in(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{best}}$ and a worst-case product MC $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{l}\in(\mathcal{M}_{\otimes}^{\mathcal{A}})_{\text{worst}}$ which respectively maximizes and minimizes the probability of reaching an accepting BSCC from all initial states. Note that the transition values between states inside the components do not affect the reachability probabilities and do not need to be considered.

5.2 Winning and Losing Components Search Algorithm

We present a graph-based algorithm for finding $(WC)_{P}$, $(WC)_{L}$, $(LC)_{P}$ and $(LC)_{L}$ in a product IMC, divided into Algorithm 1 and 2. We define the sets of potential and permanent BSCCs $(U^{A})_{?}$, $(U^{A})_{P}$, $(U^{N})_{?}$ and $(U^{N})_{P}$. Algorithm 1 takes a product IMC as input and returns its potential and permanent BSCCs. Algorithm 2 takes as inputs a product IMC and its permanent and potential BSCCs and outputs $(WC)_{P}$, $(WC)_{?}$, $(LC)_{P}$ and $(LC)_{?}$. The largest components are the union of the potential and permanent components.

We employ the following notations: a digraph $G$ is said to be generated by an induced MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$ with transition matrix $T$ and states $Q\times S$ if $G$ has a representative vertex for all states in $\mathcal{M}_{\otimes}^{\mathcal{A}}$, and an edge exists between two such vertices if $T(Q_{i},Q_{j})>0$, $Q_{i},Q_{j}\in Q\times S$. $Reach(S,G)$ denotes the set of vertices in graph $G$ from which there exists a path to the set of vertices $S$; $At_{?}(S,G)$ denotes the set of vertices in $G$ from which there exists a path to $S$ for all graphs $G^{\prime}$ generated by an induced product MC of $\mathcal{I}\otimes\mathcal{A}$, where $G$ and $G^{\prime}$ share the same set of vertices; and $At_{P}(S,G)$ denotes the set of vertices in $G$ from which there exists a path to $S$ for at least one graph $G^{\prime}$ generated by an induced product MC of $\mathcal{I}\otimes\mathcal{A}$. A detailed description of the algorithms is found below.

Algorithm 1**:**

Line 4: We first assume all transitions with a non-zero upper bound to be “on” and generate a graph $G=(V,E)$ with a vertex for all states and an edge for all transitions in $\mathcal{I}\otimes A$.

Line 5: Next, we find all strongly connected components (SCC) of $G$ and list them in $S$.

Line 6 to 10: For all SCC $S_{k}\in S$, we want to determine if there exists an induced MC where $S_{k}$ is a BSCC. To this end, for all the states $S_{k}^{j}$ in $S_{k}$, we check whether all outgoing transitions to states not in $S_{k}$ can be turned “off” for some induced product MC, that is if the transition lower bounds from $S_{k}^{j}$ to states in $Tr_{i}=V\setminus R_{i}$ are 0 and the sum of the transition upper bounds from $S_{k}^{j}$ to states in $S_{k}$ is greater than 1, which is captured by the use of the function $At_{?}$. Otherwise, $S_{k}^{j}$ is said to be leaky in all induced product MCs and $S_{k}^{j}$ is added to the set $C_{i}$, which contains all leaky states of $S_{k}$ found at iteration $i$. Note that $R_{0}=S_{k}$ and that all leaky states previously found are removed from $S_{k}$ at each iteration via variable $R_{i}$. The loop terminates when all states have been checked and no more leaky states are found, that is $C_{i}=\emptyset$.

Line 11 to 13: If $S_{k}$ contained leaky states that were previously removed, we compute all SCCs formed by the remaining states in $R_{i}$ and add them to the list of SCCs of G. If $S_{k}$ did not contain any leaky state, it is a member of a largest set of BSCCs and the mapping of the states in $S_{k}$ with respect to the Rabin Pairs decides whether $S_{k}$ is accepting and $S_{k}\in(U^{A})_{L}$ or non-accepting and $S_{i}\in(U^{N})_{L}$.

Line 14 to 15: If $S_{k}\in(U^{A})_{L}$, it could still contain potential non-accepting BSCCs, since $(U^{A})_{L}$ and $(U^{N})_{L}$ may comprise intersecting sets. Treat all states causing $S_{k}$ to be accepting as leaky (states mapping to some $F_{i}$ in the Rabin pairs when no states in $S_{k}$ maps to $E_{i}$), remove from $S_{k}$ all states that have a permanent path to the leaky states, compute all SCCs formed by the remaining states and add them to $S$.

Line 16 to 17: If $S_{k}\in(U^{N})_{L}$, potential accepting BSCCs may lie inside $S_{k}$. For all sets $F_{i}$ in the Rabin pairs to which at least one state in $S_{k}$ is mapped, create a “copy” $S_{k}^{\prime}$ of $S_{k}$ where all states causing $S_{k}$ to be non-accepting are considered leaky (the states mapping to $E_{i}$), remove from $S_{k}^{\prime}$ all states that have a permanent path to the leaky states, compute all SCCs formed by the remaining states and add them to S.

Line 19 to 22: We check whether some state in $B$ leaks outside of $B$ for at least one induced MC. If so, the BSCC is not permanent. Otherwise, $B$ is permanent if and only if no BSCC of the opposite acceptance status is found inside of $B$.

Algorithm 2**:**

Inspired by the Classical Algorithm for Buchi MDPs [34], we perform a graph search to find permanent and potential winning and losing components for each BSCC. Permanent components only arise from permanent BSCCs, while potential components stem from both potential and permanent BSCCs.

Line 4: We generate a graph $G=(V,E)$ where transitions with a non-zero upper bound are assumed to be “on”.

Line 5 to 10 For all BSCCs $B$, we find the set $R_{i}$ of all states from which there is a path to $B$ in $G$. Other states in $G$ are “trap states” denoted by $Tr_{i}$. Then, we iteratively remove the set of states $C_{i}$ from $R_{i}$ that “leak” to $Tr_{i}$ for all induced MCs, and compute the new set $R_{i+1}$ of states that have a path to $B$ once the leaky states are discarded. The iteration stops when no more leaky states are found, that is $C_{i}=\emptyset$. The remaining states belong to $(WC)_{L}$ or $(LC)_{L}$ according to $B$.

Line 20-21: If $B$ is a potential BSCC, these states have to belong to one of the potential components — $(WC)_{?}$ or $(LC)_{?}$ — depending on $B$.

Line 11: If $B$ is a permanent BSCC, we want to check whether the above set of states, denoted by $V_{P}$, contains members of the permanent components $(WC)_{P}$ or $(LC)_{P}$.

Line 12: If $B$ is accepting, remove potential non-accepting component from $V_{P}$ and treat them as trap state; for a non-accepting $B$, remove potential accepting components instead.

Line 13-20: Repeat the same procedure as in Algorithm 1, except that leaky states are now those which have a path to the trap states in at least one induced MC. The remaining states are permanent components of the same acceptance status as $B$.

To summarize, it is known that verification against temporal logic specifications in discrete-time MCs can be accomplished by solving a reachability problem on a product MC constructed from a Rabin automaton corresponding to the specification to be verified. The heart of this approach relies on analyzing winning and losing components of the product MC. These ideas do not directly extend to IMCs because BSCCs are not uniquely determined in this case; this is because some transitions can have a lower transition bound equal to 0 but an upper transition bound that is non-zero. Instead, we introduced the concepts of largest winning and losing components. In Theorem 2, we show that upper and lower bounds on the probability of satisfaction are obtained from these components. Algorithms 1 and 2 provide means for computing these components. Note that the proposed algorithm allows to perform verification of IMCs without constructing an exponentially large Markov decision process, as done in [33].

6 State-Space Refinement

Given a partition $P$ of the domain $D$ and a specification $\phi$ as in (2), the verification procedure derived in Section V assigns each discrete state of $P$ to one of the sets $Q_{\phi}^{yes}$, $Q_{\phi}^{no}$ or $Q_{\phi}^{?}$. One aims to find a partition $P$ that yields a low volume of undecided states in $Q_{\phi}^{?}$. To this end, we suggest a specification-guided iterative method. Specifically, we first generate a rough partition $P$ of $D$ and successively refine $P$ into finer partitions by targeting the best candidate states for reducing the uncertainty in the abstraction with respect to $\phi$. These states are chosen after comparing the behavior of the system in the best and worst-case scenarios computed during verification. The procedure stops when a user-defined criterion is reached. Here, we terminate when the fractional volume of uncertain states is less than a threshold $V_{stop}$ $\in[0,1]$.

We seek to analyze the behavior of accepting paths in the best and worst-case product MCs $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{l}$ obtained at the time of verification and illustrated in Fig. 4. In particular, for every undecided state $Q_{j}$ in $Q_{\phi}^{?}$, we look at all paths starting from $\left<Q_{j},s_{0}\right>$ in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}$ and assign a score to the states encountered along them depending on how these states behave in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{l}$. We inspect a path until it reaches a state that belongs to either $(WC)_{L}$ or $(LC)_{L}$, or when its probability of occurrence in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}$ falls below a threshold $p_{stop}$. States with high scores are targeted for refinement.

We introduce some notation: for a finite path $\pi=q_{0}q_{1}\ldots q_{k}$ in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}$, $Last(\pi)$ denotes the last state $q_{k}$ of $\pi$; $\pi_{i}$ denotes the $i$-th state of $\pi$; $\mathcal{P}(\pi)=T(q_{0},q_{1})\cdot T(q_{1},q_{2})\cdot\ldots\cdot T(q_{k-1},q_{k})$, $\mathcal{P}(q_{0})=1$, is the probability of path $\pi$ in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}$; $R(\pi)$ is the set of states that are one-step reachable from $Last(\pi)$ in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{u}$; $Exp(\pi)$ denotes all continuations of $\pi$ from $R(\pi)$ that have been explored and is initialized to the empty set for all $\pi$; $\pi^{-}$ is the path obtained by removing the last state of $\pi$ and $\pi^{+}(q_{i})$ is the path with $q_{i}$ appended to $\pi$. $V_{?}$ is the fractional volume of uncertain states and is equal to the sum of the volume of all states in $Q_{\phi}^{?}$ divided by the volume of the domain $D$. Our procedure is as follows:

Compute a refinement score for all states in $\mathcal{I}$ according to Algorithm 3, which is described below:

Line 6 to 24: This loop terminates when $\pi=\emptyset$, that is, when all paths starting from $\left<Q_{j},s_{0}\right>$ have been explored.

Line 7 to 8: If $\mathcal{P}(\pi)<p_{stop}$ or $Exp(\pi)=R(\pi)$, the probability of the path is below the pre-defined exploration threshold or all continuations of $\pi$ have been explored. Thus, we return to the previous state in the path.

Line 10 to 13: lf $Exp(\pi)\not=\emptyset$, add $q_{i}$ to $Exp(\pi)$, where $q_{i}$ is some unexplored state in $R(\pi)$ and extend the path to $q_{i}$. Else, $\pi$ is a path fragment which has not been explored yet. Add all states in $\pi$ to $Exp(\pi)$ to avoid loops.

Line 14 to 15: If $Last(\pi)\in(WC)_{?}$ or $Last(\pi)\in(LC)_{?}$, the path reached a state in a potential component. We want to target the states which can either confirm or refute that $Last(\pi)$ belongs to such a component. These states are the ones inside the potential BSCCs that $Last(\pi)$ belongs to (or makes a transition to with probability 1) that have outgoing transitions which can be either “on” or “off”, as depicted in Fig. 5. A potential ”certainty gain” is added to the score of all such states and the path is returned to its previous state. If $Last(\pi)$ belongs to both $(WC)_{?}$ and $(LC)_{?}$, then the scoring scheme is applied to all intersecting potential BSCCs related to $Last(\pi)$. This heuristical gain quantifies a potential reduction in the width of the satisfaction interval of $Q_{\ell}$ in the scenario that the refinement of the considered states provides perfect information, i.e., the probability of reaching an accepting BSCC from $Last(\pi)$ becomes a fixed number.

Line 16 to 17: If $Last(\pi)\in(WC)_{P}$ or $Last(\pi)\in(LC)_{P}$, the path reached a region of the state-space that does not require refinement as it belongs to a permanent component. The path returns to its previous state.

Line 18 to 20: Else, $Last(\pi)$ does not belong to a winning or losing component for any refinement of the product IMC. The potential “certainty gain” one can hope for by refining $\left<Q_{j},s_{i}\right>=Last(\pi)$ is added to the score of $Q_{j}$. The path is continued to an unexplored state. 2. 2.

Refine the states in $P_{k}$ with scores above a user-defined threshold to generate $P_{k+1}$. 3. 3.

Generate an IMC abstraction of the system with respect to $P_{k+1}$, perform model-checking and compute $V_{?}$. 4. 4.

If $V_{?}>V_{stop}$, return to step 1. Else, terminate.

It is not difficult to construct examples demonstrating that the volume of uncertain states $V_{?}$ need not decrease monotonically at each step of the refinement algorithm using our abstraction technique. This is because, when a parent state is refined to two children states, the sum of the upper transition bounds for the children states may be greater than the upper transition bound of the original parent state. Nevertheless, when $\mathcal{F}$ is continuous, the size of the reachable sets, and consequently the error in the transitions, approaches zero as the grid size decreases. Thus, in the limit, the volume of uncertain states $V_{?}$ decreases to zero.

A common refinement approach consists in splitting the chosen states in the partition in half along their greatest dimension. As the scoring procedure in Algorithm 3 may select the entire state-space of IMC $\mathcal{I}$ for refinement, the worst-case growth of the size of the product IMC $\mathcal{I}\otimes\mathcal{A}$ is exponential and scales in $\mathcal{O}(|S|\cdot 2^{|Q|})$, where $|S|$ and $|Q|$ are the number of states of automaton $\mathcal{A}$ and IMC $\mathcal{I}$ respectively.

However, because this path-based scoring procedure aims to target states which are most likely to reduce the volume of undecided states in the partition with respect to the specification under consideration, our refinement algorithm tends to focus on specific regions of the state-space, as shown in the next section, with the effect of mitigating state explosion. In particular, we were able to achieve lower volumes $V_{stop}$ before the number of states in the partition became prohibitive compared to our naive refinement method in [13] which systematically refined all uncertain states.

All algorithms discussed in this paper are implemented in a python package available at https://github.com/gtfactslab/TACStochasticVerification.

7 Case Study

We now apply our verification and refinement procedure in a case study. We consider a nonlinear, monotone bistable switch system with additive disturbance and governing equations

[TABLE]

where we assume $w_{1}$ and $w_{2}$ to be independent truncated Gaussian random variables sampled at each time step. $w_{1}\sim\mathcal{N}(\mu=-0.3;\sigma^{2}=0.1)$ and is truncated on $[-0.4,-0.2]$; $w_{2}$ is identical. To keep the system self-contained in $D$, we assume that any time the disturbance would push the trajectory outside of $D$, it is actually maintained on the boundary of $D$. This assumption reflects the behavior of systems with bounded capacity where the state variables are restricted to some intervals. We choose $a=1.3$, $b=0.25$ and $\Delta T=0.05$. The deterministic piece of the system has two stable equilibria at $(0,0)$ and $(2.71,3.52)$ and one unstable equilibrium. We seek to verify (72) on a domain $D$, with initial rectangular partition $P$ depicted in Fig. 6 (Top) and Fig. 7 (Top), against the probabilistic LTL specifications

[TABLE]

Specification $\phi_{1}$ translates in natural language to “trajectories that have more than a 80% chance of remaining in an $A$ state for at least 2 more time steps when entering an $A$ state”. Specification $\phi_{2}$ translates to “trajectories that have less than a 90% chance of reaching a $B$ state if it eventually always remain in $A$, and of always staying outside of $B$ if it reaches a $C$ state”. Their Rabin automaton representations contain 5 and 7 states respectively. We perform verification with stopping criterion $V_{stop}=0.13$ for $\phi_{1}$ and $V_{stop}=0.1$ for $\phi_{2}$. To construct IMC abstractions of this system, we use the technique shown in Section IV. Graph search is based on Section V-B and we compute reachability bounds applying the algorithm in [12]. Upon verification, we select states with an uncertainty score as defined in Section VI that is greater than $10\%$ of the highest score for refinement. Selected states are split into two rectangles along their largest dimension to keep the new partition rectangular. The procedure was conducted on a 3.3 GHz Intel Core i7 with 8 GB of memory using Python.

For $\phi_{1}$, the refinement algorithm produced 3531 states and terminated in 1h56min after 12 refinement steps. For $\phi_{2}$, it generated 4845 states and terminated in 3h15min after 13 steps. The final partitions are shown in Fig. 6 (Bottom) and Fig. 7 (Bottom). Our new method outperforms the algorithm we propose in [13] which refines all undecided states at each refinement step: for instance, for $\phi_{1}$, [13] achieves $V_{?}=0.2137$ in 2 hours 58 min and 11 steps. Our algorithm non-uniformly refined the initial partition across the state-space. In the first example, the boundary between regions which can and cannot reach an $A$ state are heavily targeted, as well as boundaries between regions which could keep the system in an $A$ state for one and two time steps. In the second example, the edges of a region leading to $A$ via $B$ are refined the most, as this region is critical with respect to $\phi_{2}$. Although these two examples share the same dynamics, our algorithm generates very different partitions depending on the specification. Therefore, specification-free gridding approaches are likely to perform conservatively for these examples.

Because this procedure produces different partitions for different temporal objectives, our algorithm is suited for the verification of systems against well-identified specifications which are known a priori, while FAUST2, which provides error guarantees with respect to entire classes of temporal logic formulas, better accommodates situations requiring an analysis against numerous distinct specifications. Furthermore, unlike our work, FAUST2 only permits verification for specifications with bounded-time temporal operators [35].

On the other hand, the toolbox StocHy [35] allows for the verification of certain unbounded-time operators through the use of IMC abstractions. However, because its verification algorithm is based on [12], it solely accommodates specification belonging to a fragment of LTL and not all $\omega$-regular properties. In addition, StocHy employs the IMC abstraction technique presented in [29] which applies only to affine-in-disturbance linear systems, while the abstraction method shown in this work and used in the case study involves the wide class of stochastic mixed monotone dynamics.

Finally, though similar in flavor, the objective of our verification technique is not identical to the one of FAUST2 and StocHy. The latter aim to create partitions engendering a user-defined abstraction error, whereas the goal of this work is to obtain a small volume of uncertain state with respect to a probabilistic $\omega$-regular specification. Note that low-error abstractions can generate a high volume of uncertain states while high-error abstractions can produce a low volume of uncertain states, depending on the threshold $p_{sat}$.

8 Conclusion

In this paper, we described an algorithm for performing verification against $\omega$-regular properties in continuous state stochastic systems. The proposed approach relies on computing a finite state abstraction of the original system in the form of an IMC and can accommodate classes of specifications not previously covered in the literature. We have developed an efficient procedure for computing the IMC of a mixed monotone system with affine disturbance over rectangular partitions. Furthermore, we presented a specification-guided strategy for refining a finite partition of the continuous domain until a precision threshold has been met. Our technique resolves qualitative issues highlighted in the literature for abstraction-based methods by targeting states that are likely to confirm or destroy winning and losing components in a product IMC. We showed the practicality of this approach in two examples.

\appendices

9 Proofs of Section IV

9.1 Proof of Proposition 2

Proof 9.4**.**

By Proposition 1, we observe

[TABLE]

To prove (16), we have

[TABLE]

where (76) follows from (75), (77) follows from the mutual independence of all components of $w$ in Assumption 2, and (78) holds because $g(a^{1},b^{1})\leq z\leq g(b^{1},a^{1})$ if and only if $g_{i}(a^{1},b^{1})\leq z_{i}\leq g_{i}(b^{1},a^{1})$ for all $i=1,\ldots,n$. Then (16) holds since $Pr(z_{i}+w_{i}\in[a^{2}_{i},b^{2}_{i}])=\int_{a_{i}^{2}}^{b_{i}^{2}}f_{w_{i}}(x-z_{i})dx$. By a symmetric argument replacing $\min$ with $\max$, (17) holds.

9.2 Proof Lemma 1

Proof 9.5**.**

For $s\in\mathbb{R}$, define $H(s)=\int_{a}^{b}f_{\omega}(x-s)\;dx$. We claim

[TABLE]

and that, for all $s_{1},s_{2}\in\mathbb{R}$ such that $|s_{max}-s_{1}|\geq|s_{max}-s_{2}|$, it holds that $H(s_{1})\leq H(s_{2})$, that is, $H(s)$ monotonically decreases as $|s_{max}-s|$ increases. Assuming the claim to be true, it follows that $\max_{s\in[r_{1},r_{2}]}H(s)=H(s^{r}_{max})$ and $\min_{s\in[r_{1},r_{2}]}H(s)=H(s^{r}_{min})$, i.e., (21) and (22), completing the proof. To prove the claim, we have, for all $s\in\mathbb{R}$,

[TABLE]

Moreover, because $f_{\omega}$ is symmetric and unimodal with mode $c$, $f_{\omega}(x+\frac{a-b}{2}-c)-f_{\omega}(x+\frac{b-a}{2}-c)$ is an odd function of $x$ and is negative for $x>0$ and positive for $x<0$. Therefore, the integral in (83) is nonnegative and monotonically decreases as $|s_{max}-s|$ increases, thus proving the claim.

9.3 Proof of Theorem 1

Proof 9.6**.**

For all $Q_{j},Q_{\ell}\in P$ and $i=1,\ldots,n$,

[TABLE]

by Lemma 1. Then, by Proposition 2,

[TABLE]

so that (34)–(44) implies (12)–(13). Furthermore, (86)–(87) implies {\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}}(Q_{j},Q_{\ell})\leq\widehat{T}(Q_{j},Q_{\ell}) and (12)–(13) implies (3) so that \mathcal{I}=(P,{\mathchoice{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\displaystyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\displaystyle T}}}}{{\ooalign{\hbox{\raise 7.09259pt\hbox{\scalebox{1.0}[-1.0]{\lower 7.09259pt\hbox{\textstyle\widehat{\vrule width=0.0pt,height=6.83331pt\vrule height=0.0pt,width=7.23265pt}}}}}\cr\hbox{\textstyle T}}}}{{\ooalign{\hbox{\raise 6.40926pt\hbox{\scalebox{1.0}[-1.0]{\lower 6.40926pt\hbox{\scriptstyle\widehat{\vrule width=0.0pt,height=4.78333pt\vrule height=0.0pt,width=5.06285pt}}}}}\cr\hbox{\scriptstyle T}}}}{{\ooalign{\hbox{\raise 5.9537pt\hbox{\scalebox{1.0}[-1.0]{\lower 5.9537pt\hbox{\scriptscriptstyle\widehat{\vrule width=0.0pt,height=3.41666pt\vrule height=0.0pt,width=3.61632pt}}}}}\cr\hbox{\scriptscriptstyle T}}}}},\widehat{T}) is a valid IMC, concluding the proof.

10 Lemmas and Proofs of Section V

Lemma 10.7**.**

[1]** For any infinite sequence of states $\pi=q_{0}q_{1}q_{2}\ldots$ in a Markov Chain, there exists an index $i\geq 0$ such that $q_{i}$ belongs to a BSCC.

Corollary 10.8**.**

For any initial state $\left<Q_{i},s_{0}\right>$ in an induced product MC $\mathcal{M}_{\otimes}^{\mathcal{A}}$,

[TABLE]

Lemma 10.9**.**

For any initial state $\left<Q_{i},s_{0}\right>$ in an induced product Markov Chain $\mathcal{M}_{\otimes}^{\mathcal{A}}$,

[TABLE]

Proof 10.10**.**

This lemma follows from Corollary 2.

Lemma 10.11**.**

Let $\mathcal{I}$ be an IMC and let $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ be two MCs induced by $\mathcal{I}$ where the set $B$ is a BSCC for both. If $C_{1}$ and $C_{2}$ are the sets of states such that $\mathcal{P}_{\mathcal{M}_{1}}(C_{1}\models\Diamond B)=1$ and $\mathcal{P}_{\mathcal{M}_{2}}(C_{2}\models\Diamond B)=1$, then there exists a MC $\mathcal{M}_{3}$ induced by $\mathcal{I}$ such that $\mathcal{P}_{\mathcal{M}_{3}}((C_{1}\cup C_{2})\models\Diamond B)=1$.

Proof 10.12**.**

Let $T_{1}$ and $T_{2}$ denote the transition matrices of $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ respectively, and $Q$ denote the set of states in $\mathcal{I}$. Consider an induced MC $\mathcal{M}_{3}$ where $T_{3}(Q_{i},Q_{j})=T_{1}(Q_{i},Q_{j})\;\forall Q_{i}\in C_{1}$ and $\forall\;Q_{j}\in Q$, and $T_{3}(Q_{i},Q_{j})=T_{2}(Q_{i},Q_{j})\;\forall Q_{i}\in C_{2}\setminus(C_{1}\cap C_{2})$ and $\forall\;Q_{j}\in Q$. By assumption, any state in $C_{1}$ reaches $B$ with probability 1, while all states in $C_{2}\setminus(C_{1}\cap C_{2})$ reach $B\cup(C_{1}\cap C_{2})$ with probability 1. Since $\mathcal{P}_{\mathcal{M}_{3}}((C_{1}\cap C_{2})\models\Diamond B)=1$ by construction, we have $\mathcal{P}_{\mathcal{M}_{3}}((C_{1}\cup C_{2})\models\Diamond B)=1$.

Lemma 10.13**.**

Let $\mathcal{I}\otimes\mathcal{A}$ be a product IMC and $(LC)_{i}$ be the losing components of any product MC $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}$ induced by $\mathcal{I}\otimes\mathcal{A}$. There exists a set of product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ with losing components $(LC)_{L}$ and such that $(LC)_{i}\subseteq(LC)_{L}$.

Proof 10.14**.**

We proved in [26] that any product IMC induces a set of MCs with a largest set of non-accepting BSCCs. Lemma 5 is deduced from this fact and Lemma 4.

Lemma 10.15**.**

Let $\mathcal{I}\otimes\mathcal{A}$ be a product IMC. Let $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$ be two product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ with sets of accepting BSCC $U^{A}_{1}$ and $U^{A}_{2}$ respectively. There exists a set of product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ with winning components $(WC)_{3}$ and such that $(U^{A}_{1}\cup U^{A}_{2})\subseteq(WC)_{3}$.

Proof 10.16**.**

Let $T_{1}$ and $T_{2}$ denote the transition matrices of $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$ respectively, and $Q$ denote the set of states in $\mathcal{I}\otimes\mathcal{A}$. Assume $U^{A}_{1}\cap U^{A}_{2}=\emptyset$. There exists a set of product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ such that $U^{A}_{1}\cup U^{A}_{2}$ are accepting BSCCs (see [26]), and thus winning components. If $U^{A}_{1}\cap U^{A}_{2}\not=\emptyset$, consider the set of all product MCs $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}$ induced by $\mathcal{I}\otimes\mathcal{A}$ such that, for all transition matrices $T_{i}$ of the product MCs in this set, $T_{i}(Q_{i},Q_{j})=T_{1}(Q_{i},Q_{j})\;\forall Q_{i}\in U^{A}_{1}$ and $\forall\;Q_{j}\in Q$, and $T_{i}(Q_{i},Q_{j})=T_{2}(Q_{i},Q_{j})\;\forall Q_{i}\in U^{A}_{2}\setminus(U^{A}_{1}\cap U^{A}_{2})$ and $\forall\;Q_{j}\in Q$. Clearly, $U^{A}_{1}$ is an accepting BSCC in all $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}$. For all $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}$, it holds that $\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}}((U^{A}_{2}\setminus(U^{A}_{1}\cap U^{A}_{2}))\models\Diamond(U^{A}_{1}\cap U^{A}_{2}))=1$, since $U^{A}_{2}$ is a BSCC for the same probability assignments in $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$. Thus, $U^{A}_{1}\cup U^{A}_{2}$ are winning components with respect to all $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}$.

Lemma 10.17**.**

Let $\mathcal{I}\otimes\mathcal{A}$ be a product IMC and $(WC)_{i}$ be the winning components of any product MC $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{i}$ induced by $\mathcal{I}\otimes\mathcal{A}$. There exists a set of product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ with winning component $(WC)_{L}$ and such that $(WC)_{i}\subseteq(WC)_{L}$.

Proof 10.18**.**

This lemma follows from Lemmas 4 and 6.

Lemma 10.19**.**

Let $\mathcal{I}\otimes\mathcal{A}$ be a product IMC. Let $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$ be two product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ with winning components $(WC)_{1}$ and $(WC)_{2}$ respectively, and such that $(WC)_{2}\subseteq(WC)_{1}$. Also, their losing components $(LC)_{1}$ and $(LC)_{2}$ are such that $(LC)_{1}=(LC)_{2}=LC$ and their respective transition matrices $T_{1}$ and $T_{2}$ satisfy $T_{1}(Q_{i},Q_{j})=T_{2}(Q_{i},Q_{j})\;\forall Q_{i}\in(Q\times S)\setminus((WC)_{1}\cup LC)$ and $\forall Q_{j}\in(Q\times S)$. The sets of accepting BSCCs of $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$ are denoted by $U^{A}_{1}$ and $U^{A}_{2}$ respectively. For any initial state $\left<Q_{i},s_{0}\right>$, it holds that

[TABLE]

Proof 10.20**.**

For any initial state $\left<Q_{i},s_{0}\right>\in LC$, it holds that $\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A}_{1})=\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A}_{2})=0$. For any initial state $\left<Q_{i},s_{0}\right>\in((WC)_{1}\cap(WC)_{2})$, it holds that $\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A}_{1})=\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A}_{2})=1$. For any initial state $\left<Q_{i},s_{0}\right>\in((WC)_{1}\setminus(WC)_{2})$, it holds that $\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A}_{1})=1\geq\mathcal{P}_{(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}}(\left<Q_{i},s_{0}\right>\models\Diamond U^{A}_{2})$. For any initial state $\left<Q_{i},s_{0}\right>\in(Q\times S)\setminus((WC)_{1}\cup LC)$ (denoted by $H$ for clarity), we have

[TABLE]

based on the transition matrices assumptions.

Lemma 10.21**.**

Let $\mathcal{I}\otimes\mathcal{A}$ be a product IMC. Let $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$ be two product MCs induced by $\mathcal{I}\otimes\mathcal{A}$ with losing components $(LC)_{1}$ and $(LC)_{2}$ respectively, and such that $(LC)_{2}\subseteq(LC)_{1}$. Also, their winning components $(WC)_{1}$ and $(WC)_{2}$ are such that $(WC)_{1}=(WC)_{2}=WC$ and their respective transition matrices $T_{1}$ and $T_{2}$ satisfy $T_{1}(Q_{i},Q_{j})=T_{2}(Q_{i},Q_{j})\;\forall Q_{i}\in(Q\times S)\setminus((LC)_{1}\cup WC)$ and $\forall Q_{j}\in(Q\times S)$. The sets of non-accepting BSCCs of $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{1}$ and $(\mathcal{M}_{\otimes}^{\mathcal{A}})_{2}$ are denoted by $U^{N}_{1}$ and $U^{N}_{2}$ respectively. For any initial state $\left<Q_{i},s_{0}\right>$, it holds that

[TABLE]

Proof 10.22**.**

The proof is identical to the one of Lemma 8

Lemma 10.23**.**

Let $\mathcal{I}\otimes\mathcal{A}$ be a product IMC with permanent and largest sets $(WC)_{P}$, $(LC)_{P}$, $(WC)_{L}$ and $(LC)_{L}$ as previously defined. There exists a set of induced MCs of $\mathcal{I}\otimes\mathcal{A}$ whose sets of winning and losing components are $(WC)_{P}$ and $(LC)_{L}$, and a set of induced MCs whose sets of losing and winning components are $(LC)_{P}$ and $(WC)_{L}$.

Proof 10.24**.**

Consider the set $\mathcal{C}$ of all induced MCs of $\mathcal{I}\otimes\mathcal{A}$ whose set of losing components is $(LC)_{L}$. For any $\left<Q_{i},s_{0}\right>\in((WC)_{?}\setminus(LC)_{L})$, consider an induced product MC $\mathcal{M}\in\mathcal{C}$ with transition matrix $T$ such that $\left<Q_{i},s_{0}\right>$ is not a winning component of $\mathcal{M}$. Such an induced product MC always exists by the definition of $(WC)_{?}$ and Lemma 8. Denote by $(WC)_{?}^{\mathcal{M}}$ the winning components of $\mathcal{M}$ which also belong to $(WC)_{?}$. There exists an induced product MC $\mathcal{M^{\prime}}$ with transition matrix $T^{\prime}$ such that, for all $q_{i}\in(WC)_{?}^{\mathcal{M}}$, $\mathcal{P}_{\mathcal{M^{\prime}}}(q_{i}\models\Diamond\neg((WC)_{?}^{\mathcal{M}}\cup(WC)_{P}))>0$, otherwise $q_{i}\in(WC)_{P}$, which is a contradiction. Consider the induced product MC $\mathcal{M^{\prime\prime}}\in\mathcal{C}$ with transition matrix $T^{\prime\prime}$ such that $T^{\prime\prime}(q_{i},q_{j})=T^{\prime}(q_{i},q_{j})$ for all $q_{i}\in(WC)_{?}^{\mathcal{M}}$ and $q_{j}\in(Q\times S)$, and $T^{\prime\prime}=T$ for all other transitions. The sets of winning and losing components of $\mathcal{M^{\prime\prime}}$ are $(WC)_{P}$ and $(LC)_{L}$, proving the claim. The proof with respect to $(LC)_{P}$ and $(WC)_{L}$ is identical.