Omega-Regular Verification and Control for Distributional Specifications in MDPs

In addition to the work already mentioned, we discuss a (non-exhaustive list of) few others. Our distributional certificates draw insights from classical certificates for program verification and template-based synthesis algorithms for their computation. Notable examples include ranking functions for proving termination in programs [22, 13] and invariants for proving safety in programs [21, 14]. Our distributional certificates draw insights from Büchi ranking functions of [17] for proving LTL properties in programs. However, there are several important differences. First, we leverage and lift the idea of Büchi ranking to the setting of probability distributions over MDP states. Second, our distributional certificates and algorithms for their computation also need to reason about strategies in MDPs. This is reflected in the following key difference. Our certificates provide soundness and completeness guarantees for all distributional $\omega$-regular specifications and distributionally memoryless strategies, and proving this requires reasoning about reachability under a strategy (see the proof of Theorem 9). The certificate of [17], on the other hand, is complete only for specifications that can be represented via deterministic Büchi automata, if the specification needs to be satisfied from a set of initial states (see Corollary 2 in [17]).

In the distributional setting, the probabilistic logics defined in [10, 11, 2] are all orthogonal to the classical semantics, and the model checking techniques developed are not template-based. To the best of our knowledge, none of these works have been automated. The works [4, 5] propose certificates for distributional reachability, safety and reach-avoidance and design template-based synthesis algorithms for their computation. Our paper follows this line of work and introduces distributional certificates and template-based algorithms for distributional $\omega$-regular specifications, hence significantly generalizing the class of distributional properties that we can automatically reason about.

Certificates were also used for reasoning about infinite-state probabilistic models such as probabilistic programs under the state-based view. In particular, supermartingale certificates were proposed for qualitative reachability [12, 15], quantitative reachability, safety and reach-avoidance [33, 19, 34, 18, 35], and most recently for qualitative $\omega$-regular specifications [1]. However, these certificates are not, a priori, applicable to the distributional setting.

A Markov decision process (MDP) is a tuple $ℳ=(S,\mathrm{𝐴𝑐𝑡},P)$. We use $S$ to denote a finite set of states and $\mathrm{𝐴𝑐𝑡}$ to denote a finite set of actions. Slightly overloading the notation, for each state $s\in S$, we write $\mathrm{𝐴𝑐𝑡}(s)\subseteq \mathrm{𝐴𝑐𝑡}$ to denote the set of available actions at $s$. Finally, $P:S\times \mathrm{𝐴𝑐𝑡}\to \mathrm{\Delta }(S)$ is a transition function, assigning to each state $s$ and available action $a\in \mathrm{𝐴𝑐𝑡}(s)$ a probability distribution over the succcessor states. When $|\mathrm{𝐴𝑐𝑡}(s)|=1$ for each state $s$, we say that $ℳ$ is a Markov chain.

An infinite path in an MDP is a sequence $\rho =s_1,a_1,s_2,a_2,\mathrm{\cdots }\in {(S\times \mathrm{𝐴𝑐𝑡})}^{\omega }$, such that $a_i\in \mathrm{𝐴𝑐𝑡}(s_i)$ and $P(s_i,a_i)(s_{i+1})>0$ for all $i\in \mathbb{N}$. A finite path $\varrho$ in an MDP is a finite prefix of an infinite path that ends in a state. We use ${\rho }_i$ and ${\varrho }_i$ to denote the $i$-th state along an (in)finite path. We use ${\mathrm{𝖨𝖯𝖺𝗍𝗁𝗌}}_{ℳ}$ and ${\mathrm{𝖥𝖯𝖺𝗍𝗁𝗌}}_{ℳ}$ to denote the sets of all infinite and finite paths in the MDP $ℳ$, respectively.

The semantics of MDPs are formalized in terms of strategies. A strategy (or policy) in an MDP $ℳ$ is a function $\pi :{\mathrm{𝖥𝖯𝖺𝗍𝗁𝗌}}_{ℳ}\to \mathrm{\Delta }(\mathrm{𝐴𝑐𝑡})$ which to each finite path (called a history) assigns a probability distribution over the action to be taken next. We require that, if a finite path $\varrho \in {\mathrm{𝖥𝖯𝖺𝗍𝗁𝗌}}_{ℳ}$ ends in a state $s$, then $\mathrm{supp}(\pi (\varrho ))\subseteq \mathrm{𝐴𝑐𝑡}(s)$. A strategy is said to be memoryless if the probability distribution over actions depends only on the last state of the finite path and not on the whole history, i.e. if $\pi (\varrho )=\pi ({\varrho }^{\prime })$ whenever $\varrho$ and ${\varrho }^{\prime }$ end in the same state. For every initial state distribution ${\mu }_0\in \mathrm{\Delta }(S)$, an MDP $ℳ$ and a strategy $\pi$ together give rise to a probability space over the set of all infinite paths in the MDP [8]. We denote by ${\mathbb{P}}_{{\mu }_0}^{\pi }$ the probability measure and by ${𝔼}_{{\mu }_0}^{\pi }$ the expectation operators in this probability space, omitting the MDP $ℳ$ from the notation when clear from the context.

MDPs are typically regarded as random generators of infinite paths, giving rise to a probability space over the set of all infinite paths in the MDP. Classical probabilistic model checking problems then explore the expected behaviour of these randomly generated infinite paths, giving rise to path properties [8]. However, one can also view MDPs as (deterministic) transformers of distributions.

Consider an MDP $ℳ$, a strategy $\pi$, and an initial state distribution ${\mu }_0\in \mathrm{\Delta }(S)$. For each $i\in \mathbb{N}$ and state $s$, define ${\mu }_i(s)={\mathbb{P}}_{{\mu }_0}^{\pi }[\rho \in {\mathrm{𝖨𝖯𝖺𝗍𝗁𝗌}}_{ℳ}\mid {\rho }_i=s]$, i.e. the probability that the $i$-th state of a randomly generated infinite path is $s$. We write ${\mu }_i={ℳ}^{\pi }({\mu }_0,i)$ for the induced probability distribution of the $i$-th state of a randomly generated infinite path. Hence, the MDP $ℳ$, a strategy $\pi$, and an initial state distribution ${\mu }_0\in \mathrm{\Delta }(S)$ together give rise to a sequence of probability distributions over the MDP states

One can then study properties of this sequence of distributions. Some examples are distributional reachability and distributional safety, which ask if the induced sequence of distributions contains or does not contain an element of some specified set of distributions [4, 5].

In this work we will consider $\omega$-regular specifications, which subsume a broad class of specifications such as those belonging to linear temporal logic (LTL) or computation tree logic (CTL) [8]. An $\omega$-regular specification over a finite set $\mathrm{𝖠𝖯}$ of atomic propositions is defined by a non-deterministic Büchi automaton (NBA) $N=(Q,\mathrm{\Sigma },\delta ,q_0,F)$, where $Q$ is a finite set of states, $\mathrm{\Sigma }=2^{\mathrm{𝖠𝖯}}$ is a finite set of letters, $\delta :Q\times \mathrm{\Sigma }\to 2^Q$ is a (non-deterministic) transition function, $q_0\in Q$ is the initial state and $F\subseteq Q$ are accepting states. An infinite word of letters ${\sigma }_1,{\sigma }_2,\mathrm{\cdots }\in {\mathrm{\Sigma }}^{\omega }$ is said to be accepting, if it gives rise to at least one accepting run in $N$, i.e. if there exists a run $q_0,q_1,q_2,\mathrm{\dots }$ such that $q_{i+1}\in \delta (q_i,{\sigma }_i)$ for each $i$ and such that $q_i\in F$ for infinitely many $i$. Note that given an LTL formula $\phi$, it can be converted to an equivalent NBA $N^{\phi }$ in exponential time (see e.g., [8]). In what follows, we will often write examples and benchmarks in LTL as it will be easier and often more intuitive. But for our analysis, we will convert them to their equivalent NBA and reason only about these NBA as the $\omega$-regular specification.

In order to reason about the synchronous evolution of a sequence of distributions over the MDP states and a run in the NBA, we will later introduce the notion of product distributional transition systems in Section 4. Hence, we here recall the notion of transition systems, which are commonly used to model imperative numerical programs.

An (infinite-state) transition system is a tuple $𝒯=(L,V,l_{\text{init}},{\theta }_{\text{init}},\mapsto )$, where

• $\mathrm{■}$

  $L$ is a finite set of locations,

• $\mathrm{■}$

  $V$ is a finite set of real-valued variables,

• $\mathrm{■}$

  $l_{\text{init}}\in L$ is the initial location,

• $\mathrm{■}$

  ${\theta }_{\text{init}}\subseteq {ℝ}^{|V|}$ is the set of initial variable valuations, and

• $\mathrm{■}$

  $\mapsto$ is a finite set of transitions of the form $\tau =(l_{\tau },l_{\tau }^{\prime },G_{\tau },U_{\tau })$ with $l_{\tau }$ a source location, $l_{\tau }^{\prime }$ a target location, $G_{\tau }$ a guard which is a boolean predicate over the variables in $V$, and $U_{\tau }:{ℝ}^n\to {ℝ}^n$ an update function.

A state in the transition system is a tuple $(l,x)\in L\times {ℝ}^{|V|}$ consisting of a location in $L$ and a valuation of variables in $V$. A transition $\tau =(l_{\tau },l_{\tau }^{\prime },G_{\tau },U_{\tau })$ is said to be enabled at a state $(l,x)$ if $l=l_{\tau }$ and $x\vDash G_{\tau }$. An infinite path (or a run) in the transition system is a sequence of states $(l_0,x_0),(l_1,x_1),\mathrm{\dots }$ with $l_0=l_{\text{init}}$, $x_0\in \mathrm{𝖨𝗇𝗂𝗍}$, and where for each $i\in {\mathbb{N}}_0$ there exists a transition ${\tau }_i=(l_i,l_{i+1},G_{\tau },U_{\tau })$ enabled at $(l_i,x_i)$ such that $x_{i+1}=U_{\tau }(x_i)$. A state $(l,x)$ is said to be reachable, if there exists an infinite path that contains $(l,x)$.

Similarly to the classical $\omega$-regular specification setting, we first need to specify a finite set of atomic propositions $\mathrm{𝖠𝖯}$. We are interested in reasoning about a sequence of distributions induced by an MDP under a strategy. Hence, we let the set $\mathrm{𝖠𝖯}$ consist of finitely many logical formulas of the form $\mathrm{𝖾𝗑𝗉}(\mu (s_1),\mathrm{\dots },\mu (s_{|S|}))\ge 0$. Here, $\mathrm{𝖾𝗑𝗉}:{ℝ}^{|S|}\to ℝ$ is an arithmetic expression over the probabilities $\mu (s_1),\mathrm{\dots },\mu (s_{|S|})$ of being in each state of the MDP, where $s_1,\mathrm{\dots },s_{|S|}$ is an arbitrary (but throughout fixed) enumeration of MDP states. In practice, we let $\mathrm{𝖠𝖯}$ contain exactly those atomic propositions that appear in the property that we want to reason about. A distributional $\omega$-regular specification $\phi$ is then defined by an NBA $N^{\phi }=(Q,\mathrm{\Sigma },\delta ,q_0,F)$ with $\mathrm{\Sigma }=2^{\mathrm{𝖠𝖯}}$.

We now define the semantics of distributional $\omega$-regular specifications. Consider a finite set of atomic propositions $\mathrm{𝖠𝖯}$, a distributional $\omega$-regular specification $\phi$, a strategy $\pi$ and an initial distribution ${\mu }_0\in \mathrm{\Delta }(S)$ in the MDP $ℳ$. The MDP $ℳ$ under strategy $\pi$ from the initial distribution ${\mu }_0$ induces an infinite word ${\sigma }_0,{\sigma }_1,{\sigma }_2,\mathrm{\dots }$ in the language $2^{\mathrm{𝖠𝖯}}$ as follows. As defined in Section 2, an MDP $ℳ$ under strategy $\pi$ from the initial distribution ${\mu }_0$ induces a sequence ${\mu }_0,{\mu }_1,{\mu }_2,\mathrm{\dots }$ of distributions over MDP states. Then, for each $i\in {\mathbb{N}}_0$, we define the letter ${\sigma }_i$ as the set of all atomic propositions in $\mathrm{𝖠𝖯}$ that are satisfied at the distribution ${\mu }_i$, i.e. ${\sigma }_i=\{p\in \mathrm{𝖠𝖯}\mid {\mu }_i\vDash p\}$, where we use $\vDash$ to denote proposition satisfaction. We say that the MDP $ℳ$ satisfies distributional $\omega$-regular specification $\phi$ under strategy $\pi$ from initial distribution ${\mu }_0\in \mathrm{\Delta }(S)$, if this infinite word ${\sigma }_0,{\sigma }_1,{\sigma }_2,\mathrm{\dots }$ is accepted by the NBA $N^{\phi }$.

We restrict our attention to a class of strategies called distributionally memoryless strategies. A strategy $\pi :{\mathrm{𝖥𝖯𝖺𝗍𝗁𝗌}}_{ℳ}\to \mathrm{\Delta }(\mathrm{𝐴𝑐𝑡})$ is said to be distributionally memoryless if the probability distribution over actions prescribed by the strategy depends only on the current distribution over the MDP states and not on the whole history. Formally, we require that for any initial distribution ${\mu }_0\in \mathrm{𝖨𝗇𝗂𝗍}$ and for any two finite runs $\rho =s_0,a_0,s_1,a_1,\mathrm{\dots },s_n$ and ${\rho }^{\prime }=s_0^{\prime },a_0^{\prime },s_1^{\prime },a_1^{\prime },\mathrm{\dots },s_n^{\prime }$ that induce the sequences of probability distributions ${\mu }_0,{\mu }_1,\mathrm{\dots },{\mu }_n$ and ${\mu }_0^{\prime },{\mu }_1^{\prime },\mathrm{\dots },{\mu }_n^{\prime }$ with ${\mu }_n={\mu }_n^{\prime }$, we have $\pi (\rho )=\pi ({\rho }^{\prime })$. When the strategy $\pi$ is distributionally memoryless, we write ${ℳ}^{\pi }(\mu )={ℳ}^{\pi }(\mu ,1)$ to denote an application of a single-step distribution transformer operator.

It was shown in [4, 5] that distributionally memoryless strategies are sufficient for reasoning about distributional reachability, safety and reach-avoid specifications. That is, for each of these distributional specifications, there exists a strategy in the MDP under which the specification is satisfied if and only if there exists a distributionally memoryless strategy in the MDP under which the specification is satisfied. While this result need not necessarily hold for distributional $\omega$-regular specifications, the restriction will be needed for enabling automated verification and synthesis as they can be represented in a more compact form.

We are now ready to define our strategy verification and synthesis problems. Consider an MDP $ℳ$, a set of initial distributions $\mathrm{𝖨𝗇𝗂𝗍}\subseteq \mathrm{\Delta }(S)$, and a distributional $\omega$-regular specification $\phi$:

1. 1.

   Strategy verification problem. Given a distributionally memoryless strategy $\pi$, verify that the MDP $ℳ$ satisfies $\phi$ under $\pi$ from every initial distribution ${\mu }_0\in \mathrm{𝖨𝗇𝗂𝗍}$.

2. 2.

   Strategy synthesis problem. Compute a distributionally memoryless strategy $\pi$, such that the MDP $ℳ$ satisfies $\phi$ under $\pi$ from every initial distribution ${\mu }_0\in \mathrm{𝖨𝗇𝗂𝗍}$.

We first formalize the notions of affine distributional certificates and distributionally memoryless strategies:

• $\mathrm{■}$

  Affine distributional certificates. A distributional certificate $(𝒞,I)$ is said to be affine if both the distributional Büchi ranking function $𝒞$ and the distributional invariant $I$ can be expressed in terms of affine expressions and inequalities over the space $\mathrm{\Delta }(S)$ of probability distributions over MDP states. We require $𝒞$ to be of the form

  $$𝒞(q,\mu )=\sum _{i=1}^{|S|}{a}_i^q\cdot \mu (s_i)+b^q,$$

  (3)

  where $a_1^q,\mathrm{\dots },a_{|S|}^q,b^q$ are some real valued coefficients for each NBA state $q\in Q$. That is, for each NBA state $q$, the function $𝒞(q,\cdot )$ is an affine function over the probabilities of being in each MDP state, with $\mu (s_1),\mathrm{\dots },\mu (s_{|V|})$ being the variables that capture probabilities of being in each MDP state and $a_1^q,\mathrm{\dots },a_{|S|}^q,b^q$ being the coefficients of the affine function. Similarly, we require $I$ to be a set defined by a conjunction of $N_I$ affine inequalities over the probabilities of being in each MDP state, i.e. to be of the form

  $$I=\{(\mu ,q)\in \mathrm{\Delta }(S)\times Q\mid {\wedge }_{k=1}^{N_I}{I}^k(q,\mu )\ge 0\},$$

  (4)

  where each $I^k(q,\mu )={\sum }_{i=1}^{|S|}{c}_i^{k,q}\cdot \mu (s_i)+d^{k,q}\ge 0$ and $c_1^{k,q},\mathrm{\dots },c_{|S|}^{k,q},d^{k,q}$ are some real valued coefficients for each NBA state $q\in Q$ and each $k\in \{1,\mathrm{\dots },N_I\}$. The number $N_I$ is referred to as the size of the invariant and will be an algorithm parameter.

• $\mathrm{■}$

  Affine distributionally memoryless strategies. A distributionally memoryless strategy $\pi :\mathrm{\Delta }(S)\to \mathrm{\Delta }(Act)$ is said to be affine, if for each state $s\in S$, action $a\in \mathrm{𝐴𝑐𝑡}$ and state distribution $\mu \in \mathrm{\Delta }(S)$, the probability of taking action $a$ in state $s$ given the current distribution over states $\mu$ is of the form

  $$\pi (s,a)(\mu )=\frac{{\sum }_{i=1}^{|S|}{e}_{i,s,a}^{\pi }\cdot \mu (s_i)+f_{s,a}^{\pi }}{{\sum }_{i=1}^{|S|}{g}_{i,s}^{\pi }\cdot \mu (s_i)+h_s^{\pi }},$$

  (5)

  where $e_{1,s,a}^{\pi },\mathrm{\dots },e_{|S|,s,a}^{\pi },f_{s,a}^{\pi }$ and $g_{1,s}^{\pi },\mathrm{\dots },g_{|S|,s}^{\pi },h_s^{\pi }$ are real valued constants. The denominator is used in order to normalize the probabilities such that the sum of probabilities of all actions being taken at a state $s$ is $1$.

Both our verification and synthesis algorithms take as input an MDP $ℳ=(S,\mathrm{𝐴𝑐𝑡},P)$, a set of initial distributions $\mathrm{𝖨𝗇𝗂𝗍}$, and a distributional $\omega$-regular specification $\phi$ defined over atomic propositions $\mathrm{𝖠𝖯}$. We assume that the distributional $\omega$-regular specification is provided via an NBA $N^{\phi }=(Q,\mathrm{\Sigma },\delta ,q_0,F)$ with letters $\mathrm{\Sigma }=2^{\mathrm{𝖠𝖯}}$, which accepts the same set of infinite words over $2^{\mathrm{𝖠𝖯}}$ as $\phi$. Finally, the algorithms also take as input the size of the invariant $N_I$ that needs to be synthesized. The verification algorithm in addition takes as input an affine distributionally memoryless strategy $\pi$.

Both verification and synthesis algorithms follow a template-based synthesis approach and proceed in four steps. In the first step, the PDTS of the input MDP and the distributional specification is constructed. In the second step, the algorithms fix a symbolic template for the affine distributional certificate, i.e. symbolic variables for each real valued coefficient in affine expressions that define the certificate. The synthesis algorithm also fixes a symbolic template for the affine distributionally memoryless strategy. In the third step, the algorithms collect a system of constraints over the symbolic template variables, that together encode all defining conditions of distributional certificates in Definition 8 as well as conditions for the strategy template to define a valid distributionally memoryless strategy (the latter for the synthesis algorithm). Finally, in the fourth step, the collected system of constraints is solved by using an SMT-solver, to get a concrete valuation of the symbolic template variables which in turn gives rise to a distributional certificate and a distributionally memoryless strategy. In what follows, we detail each of these four steps.

In this step, the PDTS ${𝒯}^{\times }=(L^{\times },V^{\times },l_{\text{init}}^{\times },{\theta }_{\text{init}}^{\times },{\mapsto }^{\times })$ is constructed from the given MDP $ℳ$ and the NBA $N^{\phi }$, as explained in Section 4.1.

The algorithms fix a template for the affine distributional certificate $(𝒞,I)$, while the synthesis algorithm also fixes a template for the affine distributionally memoryless strategy $\pi$. The novelty, compared to prior work on verification and synthesis for distributional reachability and safety specifications [4, 5], lies in a more complex template design for the distributional certificate, which is now defined with respect to the PDTS:

• $\mathrm{■}$

  Template for $𝒞$. Recall that an affine distributional Büchi ranking function is of the form $𝒞(q,\mu )={\sum }_{i=1}^{|S|}{a}_i^q\cdot \mu (s_i)+b^q$ as in eq. (3). Hence, the template for $𝒞$ is defined by introducing a set of symbolic template variables $a_1^q,\mathrm{\dots },a_{|S|}^q,b^q$ for each NBA state $q\in Q$.

• $\mathrm{■}$

  Template for $I$. Similarly, the template for an affine distributional invariant $I$ is of the form as in eq. (4). Hence, the template for $I$ is defined by introducing a set of symbolic template variables $c_1^{k,q},\mathrm{\dots },c_{|S|}^{k,q},d^{k,q}$ for each NBA state $q\in Q$ and each $k\in \{1,\mathrm{\dots },N_I\}$, where $N_I$ is the algorithm parameter that specifies the size of the invariant.

• $\mathrm{■}$

  Template for $\pi$ (synthesis algorithm). The template for an affine distributionally memoryless strategy $\pi$ is of the form as in eq. (5), hence it is defined by introducing symbolic template variables $e_{1,s,a}^{\pi },\mathrm{\dots },e_{|S|,s,a}^{\pi },f_{s,a}^{\pi }$ and $g_{1,s}^{\pi },\mathrm{\dots },g_{|S|,s}^{\pi },h_s^{\pi }$ for each state $s\in S$ and action $a\in \mathrm{𝐴𝑐𝑡}$. Note that, in the special case when we are interested in synthesizing memoryless strategies instead of distributionally memoryless strategies, the strategy template becomes simpler. Instead of the template as in eq. (5), we introduce a single symbolic template variable $p_{s,a}^{\pi }$ for each state-action pair $s\in S$ and $a\in \mathrm{𝐴𝑐𝑡}$, to encode the probability of taking action $a$ in state $s$.

In this step, the algorithms collect a system of constraints over the symbolic template variables that together encode that $𝒞$ and $ℐ$ indeed define a valid distributional certificate. For the synthesis algorithm, we also collect a system of constraints that encode that $\pi$ defines a valid distributionally memoryless strategy. In each of the following constraints, each appearance of $𝒞$, $ℐ$ and $\pi$ is replaced by the symbolic template introduced in Step 2, in the form as in eq. (3), (4) and (5). Moreover, we write $\mu \in \mathrm{\Delta }(S)$ for the conjunction of affine inequalities ${\wedge }_{i=1}^{|S|}({\mu }_i\ge 0)\wedge ({\mu }_1+\mathrm{\cdots }+{\mu }_{|S|}=1)$.

• $\mathrm{■}$

  Initial condition. We define

  $${\mathrm{\Phi }}_{\text{init}}\equiv \forall \mu \in {ℝ}^{|S|}.\mu \in \mathrm{\Delta }(S)\wedge \mu \in \mathrm{𝖨𝗇𝗂𝗍}⟹𝒞(q_0,\mu )\ge 0\wedge \underset{k=1}{\overset{N_I}{\bigwedge }}{I}^k(q_0,\mu )\ge 0.$$

• $\mathrm{■}$

  Büchi ranking condition for accepting states. For each accepting state $q\in F$ and letter $\sigma \in 2^{\mathrm{𝖠𝖯}}$ in the NBA, we define

• $\mathrm{■}$

  Büchi ranking condition for nonaccepting states. For each non-accepting state $q\in Q\backslash F$ and letter $\sigma \in 2^{\mathrm{𝖠𝖯}}$ in the NBA in the NBA, we define

• $\mathrm{■}$

  Strategy conditions (synthesis algorithm). For the strategy template to indeed define a valid affine distributionally memoryless strategy, we require that:

  $${\mathrm{\Phi }}_{\pi }\equiv \underset{s\in S}{\bigwedge }\left(\sum _{a\in Act}\pi (s,a)(\mu )=1\wedge \underset{a\in Act}{\bigwedge }(\pi (s,a)(\mu )\ge 0)\right).$$

In the above definitions, note that ${ℳ}^{\pi }(\mu )$ is the one-step successor from distribution $\mu$ when policy $\pi$ is applied in the MDP, computed as: ${\sum }_{s\in S,a\in Act(s)}\pi (s,a)(\mu )\cdot P(s,a)$.

The strategy condition constraint ${\mathrm{\Phi }}_{\pi }$ is a purely existentially quantified Boolean combination of affine inequalities over the symbolic template variables. However, constraints ${\mathrm{\Phi }}_{\text{init}}$ and are all of the form

where $t$ is the vector of all symbolic template variables, ${\text{aff-expr}}_{i,j}(t,\mu )$’s are some affine functions and ${\text{poly-expr}}_k$’s are some polynomial functions over the vectors of variables $t$ and $\mu$. Polynomial expressions on the right hand side arise due to the quotients of affine expressions that define affine distributionally memoryless strategies, see eq. (5). Hence, multiplying both sides of the inequality by the affine expressions appearing in denominators results in polynomial expressions over variables in $t$ and $\mu$.

The problem of synthesizing affine distributional certificates and affine distributionally memoryless strategies then reduces to solving a system of constraints that contain quantifier alternation $\exists t.\forall \mu$. Such quantifier alternation over real-valued variables is generally hard to handle directly and can lead to inefficiency in solvers. In order to allow for a more efficient constraint solving, before passing our system of constraints to an SMT-solver, we first apply Handelman’s theorem [27] to translate ${\mathrm{\Phi }}_{\text{init}}$ and into a purely existentially quantified system of polynomial constraints over the symbolic template variables in $t$ and auxiliary variables introduced by the translation, whose satisfiability implies satisfiability of the original constraints. This translation is common in template-based program analysis, see [7] for details. This step allows for more efficient constraint solving as well as better bound on the algorithm complexity. Finally, the resulting purely existentially quantified system of polynomial constraints over real-valued variables is solved via an SMT solver.

In the special case when we are interested in synthesizing memoryless strategies rather than distributionally memoryless strategies, we may use Farkas’ lemma [25] rather than Handelman’s theorem. This yields a sound and complete translation into an equisatisfiable purely existentially satisfied system of constraints.

Soundness of our algorithms follows from the soundness of all four steps above, including soundness of the transformations via Handelman’s theorem and Farkas’ lemma [7]. Since the Farkas’ lemma transformation leads to an equisatisfiable system of constraints, it also follows that our algorithm is relatively complete – it is guaranteed to synthesize an affine distributional certificate and memoryless strategy whenever they exist. Finally, our algorithms provide a PSPACE complexity upper bound as they reduce the synthesis and verification problems to solving a sentence in the existential first-order theory of the reals. The following theorem summarizes these results.

We evaluated our method on several examples collected from the literature:

• $\mathrm{■}$

  GridWorld (synthesis). Motivated by [5], these benchmarks model robot swarms in gridworld environments. Initially, all robots are placed in the top-left corner of the gridworld environment. Some of the cells are covered by walls whereas some are slippery and with certain probability may lead to moving in an undesired direction. Hence, each environment induces an MDP. As shown in [5], the evolution of a robot swarm can be analyzed by taking the distribution transformer view of MDPs and considering how the robots are distributed across the gridworld cells at each time step. In Table 1, we consider $5$ gridworld benchmarks of varying sizes and consider two distributional specifications: (1) at least 90% of robots should be in some slippery target cell infinitely often, and (2) in addition, at most 50% of robots should occupy some narrow passage at any point in time.

• $\mathrm{■}$

  PageRank (verification). We consider a Markov chain representation of the PageRank algorithm taken from [2]. Given the context, we consider various verification tasks, which are of the form: always if the probability mass at some vertex/page is above a threshold, then eventually, it must be above a threhold in another page.

• $\mathrm{■}$

  Pharamakocinetics (verification) We also consider a 6 state Markov chain from  [2] which is adapted from a Pharmacokinetics example in [11]. We use the two queries that were listed in [2] as the motivating examples to obtain our specifications.

• $\mathrm{■}$

  Benchmarks from [4] (verification and synthesis). Finally, we collect $3$ pairs of verification and synthesis tasks from [4]. In the verification task a strategy is fixed, whereas in the synthesis task one also needs to compute the strategy. While [4] considered distributional safety specifications, we design more complex $\omega$-regular specifications.

Our experimental results are shown in Table 1. Our results demonstrate that our prototype is able to solve a number of challenging verification and synthesis tasks for distributional $\omega$-regular specifications in MDPs, that were beyond the reach of all existing methods. This is achieved at runtimes that are comparable or even lower than those reported by earlier methods for distributional reachability and safety specifications in [4, 5] on benchmarks of similar size. Hence, even though we consider a significantly more general class of distributional $\omega$-regular specifications, our algorithms do not lead to a significant computational overhead. Moreover, for all our strategy synthesis tasks, our prototype was able to compute memoryless strategies that lead to distributional specification satisfaction. This demonstrates the generality of relative completeness guarantees provided by our algorithms.

We also make some observations. First, as can be seen from runtimes reported in Table 1, the final SMT-solving step is computationally the most expensive step of our algorithms. Constraint generation took at most a few seconds in all cases. Second, we observe that strategy synthesis tasks are generally computationally more expensive, which is expected given that they require synthesizing both the strategy and the distributional certificate. However, in some cases the synthesis problems can also be solved more efficiently. This is demonstrated by the last $6$ experiments (CAV’23 in Table 1), where synthesis is achieved at lower runtimes due to our prototype being able to compute a simple memoryless strategy that was easier to verify, compared to the strategy considered in the verification task.

Finally, regarding the invariant size parameter, we used $N_I=1$ because it was sufficient for all our benchmarks. We also ran our prototype tool with $N_I=2$ on $12$ of the benchmarks and $8$ of them were solved within the timeout of 5 minutes. The timeouts are likely due to the larger size of the final system of constraints. Indeed, given more time, we expect our method can be effectively applied with larger template sizes as well.