Compositional Reasoning for Parametric Probabilistic Automata

Mertens, Hannah; Quatmann, Tim; Katoen, Joost-Pieter

doi:10.4230/LIPIcs.CONCUR.2025.31

Compositional Reasoning for Parametric Probabilistic Automata

Hannah Mertens¹¹1Corresponding author

RWTH Aachen University, Germany Tim Quatmann

RWTH Aachen University, Germany Joost-Pieter Katoen

RWTH Aachen University, Germany

Abstract

We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) – an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.

Keywords and phrases:

Verification, Probabilistic systems, Assume-guarantee reasoning, Parametric Probabilistic Automata, Parameter synthesis

Funding:

Tim Quatmann: This research was funded by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic

Editors:

Patricia Bouyer and Jaco van de Pol

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Probabilistic Model Checking [21, 31] studies the automated verification of Markov models for systems with random behavior. Applications include network and security protocols, biochemical processes, and planning under uncertainty [40, 33, 20]. Common properties such as reachability probabilities in Markov decision processes (MDPs) can often be verified efficiently in PTIME [3].

When the probabilities with which the system evolves are not known exactly, verification results must be robust towards slight perturbations. Parametric Markov models [14, 28] allow representing uncertain model quantities – for example the bias of a coin-flip or the probability of a sensor misreading – using parameters. Feasibility is a fundamental verification problem for parametric systems and asks whether there is an instantiation of the parameters under which a given specification holds. Deciding feasibility for reachability probability specifications in parametric MDPs is ETR-complete, i.e., at least NP-hard and within PSPACE [29]. The dual verification problem that asks if the specification holds under all instantiations is co-ETR complete. Checking parametric Markov models is therefore significantly more complex compared to Markov models without parameters.

The number of system states grows exponentially with the number of system components. The resulting state-space explosion is an omnipresent challenge when model checking complex systems, often rendering analysis computationally infeasible. Compositional verification techniques such as assume-guarantee (AG) reasoning [26, 44] address this problem by decomposing the verification task into smaller sub-tasks that consider individual components in isolation. This modular verification approach has been successfully applied in various domains, including service-based workflow verification [6], large-scale IT systems [7], and autonomous systems incorporating deep neural networks [42, 43]. Recent advancements include circular AG reasoning [16] and verification-repair techniques [22]. Extensions to probabilistic systems have further expanded the scope of AG reasoning, as demonstrated in works such as [35], where AG reasoning was applied to Segala’s probabilistic automata (PA) [47] – a compositional extension of Markov decision processes. Automated approaches to AG reasoning for probabilistic systems have also been explored [19, 36], enabling more scalable verification. Other works have considered parametric, but non-probabilistic timed automata [2] as well as parameterized programs [4, 48, 39] – where the concurrent system is parameterized by the number of processes or threads in a configured instance.

This work introduces a framework for compositional reasoning about parametric probabilistic automata (pPA). The case studies presented by Kwiatkowska et al. [35] demonstrate the practical applicability of AG reasoning within a non-parametric setting. These findings provide strong motivation for extending this approach to the parametric domain. In this work, we develop the theoretical foundations of an AG reasoning framework for pPAs, leveraging results from (non-parametric) PAs [35]. Due to the aforementioned ETR-hardness, compositional reasoning has a large potential and can be crucial to verify complex parameterized systems that are too large to handle monolithically.

Example 1.

Consider a communication system, where a sender $\mathcal{S}$ broadcasts messages to a receiver $\mathcal{R}$ through a broadcast channel $\mathcal{B}$ . The system is modeled by the parallel composition $\mathcal{S}\parallel\mathcal{B}\parallel\mathcal{R}$ . The components are faulty: $\mathcal{S}$ might face a collision, broadcasting in $\mathcal{B}$ might fail due to message loss, and $\mathcal{R}$ might miss broadcasts. The reliability of $\mathcal{S}$ , $\mathcal{B}$ , and $\mathcal{R}$ is influenced by parameters and the precise values of these parameters vary depending on network conditions, interference, or other factors. Our goal is to verify that under all parameter instantiations in a given parameter space $R$ , the message is successfully received with at least probability $0.7$ , formally denoted by

(\mathcal{S}\parallel\mathcal{B}\parallel\mathcal{R}),R\leavevmode\nobreak\ % \models{}\!\leavevmode\nobreak\ \mathbb{P}_{\geq 0.7}\!(\mathit{received}).

AG reasoning allows to verify the specification without explicitly considering the (potentially large) composition $\mathcal{S}\parallel\mathcal{B}\parallel\mathcal{R}$ . To this end, assume that we have established the following statements:

$\blacksquare$

$\mathcal{S},R\models{}\!\mathbb{P}_{<0.1}\!(\mathit{collision})$ – the probability that $\mathcal{S}$ faces a collision is below $0.1$
$\blacksquare$

${\mathcal{B},R}\models{}\!{\mathbb{P}_{<0.1}\!(\mathit{collision})}{% \rightarrow}{\mathbb{P}_{\geq 0.8}\!(\mathit{broadcast})}$ – if $\mathcal{B}$ observes a collision with probability below $0.1$ , the message is broadcast with probability at least $0.8$
$\blacksquare$

${\mathcal{R},R}\models{}\!{\mathbb{P}_{\geq 0.8}\!(\mathit{broadcast})}{% \rightarrow}{\mathbb{P}_{\geq 0.7}\!(\mathit{received})}$ – If the message is broadcast with probability at least $0.8$ , then $\mathcal{R}$ receives the message with probability at least $0.7$

We reason about the composed system using the AG rule stated in Theorem 33 in Section 5:

(\mathcal{S}\parallel\mathcal{B}),R\models{}\!\mathbb{P}_{\geq 0.8}\!(\mathit{% broadcast}){\mathcal{B},R}\models{}\!{\mathbb{P}_{<0.1}\!(\mathit{collision})}% {\rightarrow}{\mathbb{P}_{\geq 0.8}\!(\mathit{broadcast})}\mathcal{S},R\models% {}\!\mathbb{P}_{<0.1}\!(\mathit{collision})\qquad(\mathcal{S}\parallel\mathcal% {B}\parallel\mathcal{R}),R\models{}\!\mathbb{P}_{\geq 0.7}\!(\mathit{received}% ){\mathcal{R},R}\models{}\!{\mathbb{P}_{\geq 0.8}\!(\mathit{broadcast})}{% \rightarrow}{\mathbb{P}_{\geq 0.7}\!(\mathit{received})}(\mathcal{S}\parallel% \mathcal{B}),R\models{}\!\mathbb{P}_{\geq 0.8}\!(\mathit{broadcast})

Contributions.

To the best of our knowledge, we provide the first framework for compositional reasoning of parametric Markov models. Our main contributions are as follows.

$\blacksquare$

We introduce and formalize pPAs, i.e., compositional probabilistic automata with parametric transitions.
$\blacksquare$

We provide a conservative extension of strategy projections [46, 35] to pPAs, including a more natural definition based on conditional probabilities. Strategy projections are essential for correctness of compositional reasoning as they allow to link measures of a composed model to measures of its constituting components.
$\blacksquare$

We present rules for assume-guarantee reasoning, generalizing an established framework by Kwiatkowska et al. [35] to the parametric setting – which requires some technically intricate proofs. The framework applies to $\omega$ -regular and expected total reward properties as well as multi-objective combinations thereof.
$\blacksquare$

We provide a new rule for compositional reasoning about monotonicity in pPAs. Knowing that a measure of interest – either the probability to satisfy an $\omega$ -regular specification or an expected total reward – is monotone in one or more parameters can significantly speed up verification [28, 50]. Our rule allows to derive monotonicity w.r.t. a composed pPA by only determining monotonicity for its components.

We introduce pPAs in Section 2 and discuss strategy projections in Section 3. Section 4 outlines properties of interest and Section 5 presents our AG rules. We outline results for monotonicity in Section 6 and related work in Section 7. Section 8 concludes the paper. Proofs omitted in the main part of the paper are given in the extended version [38].

2 Preliminaries

For sets $X$ and $Y$ , let $f\colon X\hookrightarrow Y$ denote a partial function from $X$ to $Y$ with domain $\mathit{dom}(f)\subseteq X$ . The projection of $f$ to a set $Z$ is written as ${f{\upharpoonright}_{\!Z}}\colon(X\cap Z)\to Y$ . Iverson brackets $\llbracket\,\varphi\,\rrbracket\in\{0,1\}$ map a Boolean condition $\varphi$ to $1$ if $\varphi$ holds and $0$ otherwise.

$\mathbb{Q}[V]$ denotes the set of (multivariate) polynomials over a finite set of real-valued parameters $V=\{p_{1},\dots,p_{n}\}$ . A (parameter) valuation for $V$ is a function $\mathpzc{v}\colon V\to\mathbb{R}$ . Evaluating a polynomial $f\in\mathbb{Q}[V]$ at $\mathpzc{v}$ yields $f[\mathpzc{v}]\in\mathbb{R}$ . A region ${R}$ for $V$ is a set of valuations. For $p\in V$ , we define the valuation $\mathpzc{e}_{p}$ with $\mathpzc{e}_{p}(q)=\llbracket\,p{=}q\,\rrbracket$ for $q\in V$ .

A parametric distribution²²2We use the term parametric distribution – rather than parametric function – to emphasize that we are typically interested in functions $\mu$ where $\mu[\mathpzc{v}]$ is a (sub)probability distribution. for $V$ over a finite set $S$ is a function $\mu\colon S\to(\mathbb{Q}[V]\cup\mathbb{R})$ . Applying valuation $\mathpzc{v}$ to $\mu$ yields $\mu[\mathpzc{v}]\colon S\to\mathbb{R}$ with $\mu[\mathpzc{v}](s)=\mu(s)[\mathpzc{v}]$ for all $s\in S$ . We call $\mu\colon S\to[0,1]$ a subdistribution if $\sum_{s\in S}\mu(s)\leq 1$ and a distribution if $\sum_{s\in S}\mu(s)=1$ . The sets of parametric distributions, subdistributions, and distributions over $S$ are denoted by $\mathit{Dist}_{V}(S)$ , $\mathit{SubDist}(S)$ , and $\mathit{Dist}(S)$ , respectively. For $s\in S$ , $\mathbbm{1}_{s}\in\mathit{Dist}(S)$ is the Dirac distribution with $\mathbbm{1}_{s}(s^{\prime})=\llbracket\,s^{\prime}{=}s\,\rrbracket$ . For sets $S_{1},S_{2}$ , the product of $\mu_{1}\in\mathit{Dist}_{V}(S_{1})$ and $\mu_{2}\in\mathit{Dist}_{V}(S_{2})$ is the distribution $\mu_{1}{\times}\mu_{2}\in\mathit{Dist}_{V}(S_{1}\times S_{2})$ with $(\mu_{1}{\times}\mu_{2})(s_{1},s_{2})=\mu_{1}(s_{1})\cdot\mu_{2}(s_{2})$ .

2.1 Parametric Probabilistic Automata

We combine probabilistic automata (PA) [47, 52] with parametric Markov models [28].

Definition 2.

A parametric probabilistic automaton (pPA) over a finite alphabet $\Sigma$ is a tuple $\mathcal{M}=\left(S,{s^{\mathit{init}}},V,\mathit{Act},\mathbf{P},L\right)$ , where $S$ , $V$ , and $\mathit{Act}$ are finite sets of states, parameters, and actions, respectively, ${s^{\mathit{init}}}\in S$ is an initial state, $\mathbf{P}\colon(S\times\mathit{Act})\hookrightarrow\mathit{Dist}_{V}(S)$ is a parametric transition function, and $L\colon\mathit{dom}(\mathbf{P})\to\Sigma$ is a labeling function.

Let $\mathcal{M}=\left(S,{s^{\mathit{init}}},V,\mathit{Act},\mathbf{P},L\right)$ be a pPA. For $s\in S$ , $\mathit{Act}\left(s\right)=\{\alpha\in\mathit{Act}\mid(s,\alpha)\in\mathit{dom% }(\mathbf{P})\}$ denotes the set of enabled actions in $s$ and $\mathcal{M}_{s}$ is the pPA where the initial state is set to $s$ . We set $\mathbf{P}(s,\alpha,s^{\prime})=\mathbf{P}(s,\alpha)(s^{\prime})$ if $(s,\alpha)\in\mathit{dom}(\mathbf{P})$ and otherwise $\mathbf{P}(s,\alpha,s^{\prime})=0$ . $\mathcal{M}$ is a (non-parametric) PA if $\mathbf{P}(s,\alpha)\in\mathit{Dist}(S)$ for all $(s,\alpha)\in\mathit{dom}(\mathbf{P})$ . In this case, $\mathbf{P}(s,\alpha,s^{\prime})$ is the probability to transition to successor state $s^{\prime}$ when action $\alpha$ is selected at state $s$ .

The instantiation of $\mathcal{M}$ at valuation $\mathpzc{v}$ for $V$ is the pPA $\mathcal{M}[\mathpzc{v}]=\left(S,{s^{\mathit{init}}},\emptyset,\mathit{Act},% \mathbf{P}[\mathpzc{v}],L\right)$ , where $\mathit{dom}(\mathbf{P}[\mathpzc{v}])=\mathit{dom}(\mathbf{P})$ and $\mathbf{P}[\mathpzc{v}](s,\alpha)=\mathbf{P}(s,\alpha)[\mathpzc{v}]$ . If $\mathcal{M}[\mathpzc{v}]$ is a non-parametric PA, we say $\mathpzc{v}$ is well-defined for $\mathcal{M}$ . A valuation $\mathpzc{v}$ is graph-preserving for $\mathcal{M}$ if it is well-defined and for all $s,s^{\prime}\in S$ and $\alpha\in\mathit{Act}_{\mathcal{M}}$ : $\mathbf{P}(s,\alpha,s^{\prime})[\mathpzc{v}]=0$ iff $\mathbf{P}(s,\alpha,s^{\prime})=0$ . A region ${R}$ is well-defined (graph-preserving) if all its valuations $\mathpzc{v}\in{R}$ are well-defined (graph-preserving).

(a) pPA

\mathcal{M}_{1}

.

(b) pPA

\mathcal{M}_{2}

.

Figure 1: Example pPAs

\mathcal{M}_{1}

and

\mathcal{M}_{2}

.

Example 3 (pPA).

Consider the pPA $\mathcal{M}_{1}$ in Figure 1(a) and $\mathcal{M}_{2}$ in Figure 1(b). $\mathcal{M}_{1}=\left(S_{1},{s^{\mathit{init}}_{1}},V_{1},\mathit{Act}_{1},% \mathbf{P}_{1},L_{1}\right)$ , where $S_{1}=\{s_{0},s_{1}\}$ , ${s^{\mathit{init}}_{1}}=s_{0}$ and $V_{1}=\{p\}$ . Actions $\mathit{Act}_{1}=\{\mathsf{a},\mathsf{b},\mathsf{c}\}$ and alphabet $\Sigma_{1}=\{\mathsf{a},\mathsf{b},\mathsf{c}\}$ . In this example, the alphabet coincides with actions as these uniquely define the transitions. Similarly, $\mathcal{M}_{2}=\left(S_{2},{s^{\mathit{init}}_{2}},V_{2},\mathit{Act}_{2},% \mathbf{P}_{2},L_{2}\right)$ , where $S_{2}=\{t_{0},\dots,t_{4}\}$ , ${s^{\mathit{init}}_{2}}=t_{0}$ , and $V_{2}=\{p,q\}$ . Again, $\mathit{Act}_{2}=\Sigma_{2}=\{\mathsf{a},\mathsf{c},\frownie\}$ .

An infinite path of $\mathcal{M}$ is an alternating sequence $\pi=s_{0},\alpha_{0},s_{1},\alpha_{1},\dots$ of states $s_{i}\in S$ and actions $\alpha_{i}\in\mathit{Act}$ such that $(s_{i},\alpha_{i})\in\mathit{dom}(\mathbf{P})$ for all $i\geq 0$ . A finite path of length $n\in\mathbb{N}$ is a prefix $\widehat{\pi}=s_{0},\alpha_{0},\dots,s_{n}$ of an infinite path, ending in a state $\mathit{last}(\widehat{\pi})=s_{n}\in S$ . $Paths_{\mathcal{M}}^{inf}{}$ and $Paths_{\mathcal{M}}^{fin}{}{}$ are the sets of infinite and finite paths of $\mathcal{M}$ , respectively. For a (finite or infinite) path $\pi\in Paths_{\mathcal{M}}^{inf}{}\cup Paths_{\mathcal{M}}^{fin}{}$ , we write $|\pi|\in\mathbb{N}\cup\{\infty\}$ for its length and $\pi[0,j]$ for its prefix of length $j\leq|\pi|$ . We deliberately allow paths that take transitions with probability 0. As a consequence, a path of a pPA M is always also a path of any of its instantiations $\mathcal{M}[\mathpzc{v}]$ – even if $\mathpzc{v}$ is not graph-preserving.

Strategies – also known as schedulers or adversaries – resolve nondeterminism by assigning (sub-)distributions over enabled actions based on the history – i.e., a finite path – observed so far. We allow for partial strategies that, intuitively, can choose none of the enabled actions to reflect the case that no further transition is executed.

Definition 4.

A (partial) strategy for $\mathcal{M}$ is a function $\sigma\colon Paths_{\mathcal{M}}^{fin}{}\to\mathit{SubDist}(\mathit{Act})$ such that $\sigma(\widehat{\pi})(\alpha)>0$ implies $(\mathit{last}(\widehat{\pi}),\alpha)\in\mathit{dom}(\mathbf{P})$ . A strategy $\sigma\colon Paths_{\mathcal{M}}^{fin}\to\mathit{Dist}(\mathit{Act}_{\mathcal{% M}})$ is called complete. The set of all partial and complete strategies on $\mathcal{M}$ are denoted by $Str_{\!\mathcal{M}}^{\!\star}$ , where $\star\in\{\mathit{prt},\mathit{cmp}\}$ , respectively. A memoryless strategy only depends on the last state of $\widehat{\pi}$ . The set of memoryless strategies on $\mathcal{M}$ is denoted by $Str_{\!\mathcal{M}}^{\!\mathit{mless},\star}$ .

For a strategy $\sigma$ for $\mathcal{M}$ , we may write $\sigma(\widehat{\pi},\alpha)$ instead of $\sigma(\widehat{\pi})(\alpha)$ . If $\sigma$ is memoryless, we write $\sigma(s_{n},\alpha)$ instead of $\sigma(\widehat{\pi},\alpha)$ , where $s_{n}=\mathit{last}(\widehat{\pi})$ .

A well-defined instantiation $\mathpzc{v}$ and a strategy $\sigma$ for $\mathcal{M}$ yield a purely probabilistic process described by the (sub)probability measure $Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}$ on the measurable subsets of $Paths_{\mathcal{M}}^{inf}{}$ , which is obtained by a standard cylinder set construction [3]:

\textsf{Cyl}(\widehat{\pi})=\{\pi\in Paths_{\mathcal{M}}^{inf}{}\mid\widehat{% \pi}\text{ is a prefix of }\pi\}

is the cylinder set of a finite path $\widehat{\pi}=s_{0},\alpha_{0},\dots,s_{n}$ of $\mathcal{M}$ and we set

Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\textsf{Cyl}(\widehat{\pi})\right% )\leavevmode\nobreak\ =\leavevmode\nobreak\ \llbracket\,s_{0}={s^{\mathit{init% }}}\,\rrbracket\cdot\prod_{i=0}^{n-1}\sigma(\widehat{\pi}[0,i],\alpha_{i})% \cdot\mathbf{P}(s_{i},\alpha_{i},s_{i+1})[\mathpzc{v}].

This definition extends uniquely to a probability measure on all measurable sets of infinite paths. We further lift $Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}$ to (sets of) finite paths and write, e.g., $Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\widehat{\pi}\right)$ for $\widehat{\pi}\in Paths_{\mathcal{M}}^{fin}$ or $Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\Pi\right)$ for $\Pi\subseteq Paths_{\mathcal{M}}^{fin}$ – implicitly referring to (unions of) cylinder sets. If $\mathcal{M}$ is a (non-parametric) PA, we may omit $\mathpzc{v}$ and write $Pr_{\mathcal{M}}^{\sigma}$ . Well-defined $\mathpzc{v}$ yields $Pr_{\mathcal{M}[\mathpzc{v}]}^{\sigma}=Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}$ .

Example 5.

For the pPA $\mathcal{M}_{2}$ from Figure 1(b) and a well-defined valuation $\mathpzc{v}$ , the probability to reach the state $t_{3}$ under valuation $\mathpzc{v}$ is $(1-\mathpzc{v}(p))\cdot\mathpzc{v}(q)+\mathpzc{v}(p)\cdot\frac{1}{10}$ .

$\blacktriangleright$ Remark 6.

Our definition of PA slightly deviates from related work [47, 35, 32, 36], which commonly define a transition relation $\delta\subseteq S\times\Sigma\times\mathit{Dist}(S)$ instead of functions $\mathbf{P}$ and $L$ . In our setting, a pair $(s,\alpha)\in\mathit{dom}(\mathbf{P})$ uniquely identifies both, a label $L(s,\alpha)\in\Sigma$ , and a distribution over successor states $\mathbf{P}(s,\alpha)\in\mathit{Dist}(S)$ , which significantly simplifies formalizations related to pPAs. In particular, any strategy for $\mathcal{M}$ immediately also applies to instantiations of $\mathcal{M}$ and vice versa, i.e., we have $Str_{\!\mathcal{M}}^{\!}=Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!}$ for any valuation $v$ . On the other hand, our variant does not affect expressiveness of non-parametric PA as one can convert between the two formalisms.

We lift parallel composition of PA [47] to pPAs. Composed pPAs synchronize on common transition labels while behaving autonomously on non-common labels. For simplicity, we assume that composed pPAs consider a common set of parameters $V$ .³³3If two pPAs have different parameter sets $V_{1}\neq V_{2}$ , the assumption can be established by considering $V=V_{1}\cup V_{2}$ instead, potentially adding (unused) parameters to the individual pPAs.

Definition 7 (Parallel Composition).

For $i=1,2$ , let $\mathcal{M}_{i}=(S_{i},{s^{\mathit{init}}_{i}},V,\mathit{Act}_{i},\mathbf{P}_{% i},L_{i})$ be two pPAs over alphabets $\Sigma_{i}$ with $\mathit{Act}_{i}\cap(\Sigma_{1}\cup\Sigma_{2})=\emptyset$ . The parallel composition of $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ is given by the pPA $\mathcal{M}_{1}\parallel\mathcal{M}_{2}=\big{(}S_{1}\times S_{2},({s^{\mathit{% init}}_{1}},{s^{\mathit{init}}_{2}}),V,\mathit{Act}_{\parallel},\mathbf{P}_{% \parallel},L_{\parallel}\big{)}$ over $\Sigma_{1}\cup\Sigma_{2}$ , where

$\blacksquare$

$\mathit{Act}_{\parallel}=(\mathit{Act}_{1}\times\mathit{Act}_{2})\mathbin{% \mathaccent 0{\cdot}\cup}(\mathit{Act}_{1}\times\Sigma_{1}\setminus\Sigma_{2})% \mathbin{\mathaccent 0{\cdot}\cup}(\Sigma_{2}\setminus\Sigma_{1}\times\mathit{% Act}_{2})$ ,
$\blacksquare$

for each $(s_{1},\alpha_{1})\in\mathit{dom}(\mathbf{P}_{1})$ , $(s_{2},\alpha_{2})\in\mathit{dom}(\mathbf{P}_{2})$ with $L_{1}(s_{1},\alpha_{1})=L_{2}(s_{2},\alpha_{2})\in\Sigma_{1}\cap\Sigma_{2}$ :

$\mathbf{P}_{\parallel}((s_{1},s_{2}),(\alpha_{1},\alpha_{2}))=\mathbf{P}_{1}(s% _{1},\alpha_{1})\times\mathbf{P}_{2}(s_{2},\alpha_{2})\quad\text{and}\quad L_{% \parallel}((s_{1},s_{2}),(\alpha_{1},\alpha_{2}))=L_{1}(s_{1},\alpha_{1}),$
$\blacksquare$

for each $(s_{1},\alpha_{1})\in\mathit{dom}(\mathbf{P}_{1})$ , $s_{2}\in S_{2}$ with $L_{1}(s_{1},\alpha_{1})=\mathsf{a}_{1}\in\Sigma_{1}\setminus\Sigma_{2}$ :

$\mathbf{P}_{\parallel}((s_{1},s_{2}),(\alpha_{1},\mathsf{a}_{1}))=\mathbf{P}_{% 1}(s_{1},\alpha_{1})\times\mathbbm{1}_{s_{2}}\quad\text{and}\quad L_{\parallel% }((s_{1},s_{2}),(\alpha_{1},\mathsf{a}_{1}))=\mathsf{a}_{1}=L_{1}(s_{1},\alpha% _{1}),$
$\blacksquare$

for each $s_{1}\in S_{1}$ , $(s_{2},\alpha_{2})\in\mathit{dom}(\mathbf{P}_{2})$ with $L_{2}(s_{2},\alpha_{2})=\mathsf{a}_{2}\in\Sigma_{2}\setminus\Sigma_{1}$ :

$\mathbf{P}_{\parallel}((s_{1},s_{2}),(\mathsf{a}_{2},\alpha_{2}))=\mathbbm{1}_% {s_{1}}\times\mathbf{P}_{2}(s_{2},\alpha_{2})\quad\text{and}\quad L_{\parallel% }((s_{1},s_{2}),(\mathsf{a}_{2},\alpha_{2}))=\mathsf{a}_{2}=L_{2}(s_{2},\alpha% _{2}).$

The parallel composition of parametric probabilistic automata (pPAs) is associative, meaning that $(\mathcal{M}_{1}\parallel\mathcal{M}_{2})\parallel\mathcal{M}_{3}$ and $\mathcal{M}_{1}\parallel(\mathcal{M}_{2}\parallel\mathcal{M}_{3})$ are equivalent up to state renaming. Therefore, we denote this composition as $\mathcal{M}_{1}\parallel\mathcal{M}_{2}\parallel\mathcal{M}_{3}$ .

Figure 2: Parallel composition of pPAs

\mathcal{M}_{1}

and

\mathcal{M}_{2}

from Figure 1.

Example 8 (Parallel Composition).

Figure 2 shows the composition of pPAs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ from Figure 1. Actions with labels $\mathsf{a}$ or $\mathsf{c}$ are synchronized while $\mathsf{b}$ and $\frownie$ are asynchronous.

Similar to [35, Section 3.5], we sometimes assume fairness of strategies, meaning that specific sets of labels $\Sigma_{i}\subseteq\Sigma$ are visited infinitely often.

Definition 9 (Fair Strategy).

Let $\mathcal{C}\subseteq 2^{\Sigma}$ and $\mathpzc{v}$ be a well-defined valuation for $\mathcal{M}$ over $\Sigma$ . A complete strategy $\sigma\in Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!\mathit{cmp}}$ is fair w.r.t. $\mathcal{C}$ (denoted ${{\mathit{fair}}_{\mathcal{C}\ }}\!\!$ ) if

Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\big{\{}s_{0},\alpha_{0},s_{1},% \alpha_{1},\dots\in Paths_{\mathcal{M}}^{inf}{}\mathbin{\big{|}}\forall\Sigma_% {i}\in\mathcal{C}\colon\,\forall j\in\mathbb{N}\colon\,\exists k\geq j\colon\,% L(s_{k},\alpha_{k})\in\Sigma_{i}\big{\}}\right)=1.

The set of all ${{\mathit{fair}}_{\mathcal{C}\ }}\!\!$ strategies of $\mathcal{M}[\mathpzc{v}]$ is denoted $Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}$ .

Almost-sure repeated reachability in PA only depends on the graph structure, which yields:

Proposition 10.

For any graph-preserving valuations $\mathpzc{v},\mathpzc{v}^{\prime}$ for $\mathcal{M}$ we have $Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}=Str% _{\!\mathcal{M}[\mathpzc{v}^{\prime}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}$ , i.e., a strategy is ${{\mathit{fair}}_{\mathcal{C}\ }}\!\!$ for $\mathcal{M}[\mathpzc{v}]$ iff it is ${{\mathit{fair}}_{\mathcal{C}\ }}\!\!$ for $\mathcal{M}[\mathpzc{v}^{\prime}]$ .

3 Strategy Projections

In this section, we define the projection of a strategy of a composite pPA $\mathcal{M}=\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ onto a single component $\mathcal{M}_{i}$ for $i=1,2$ . Projections for PA are defined in [35, Definition 6] and originate from [46, page 65, Definition of Projection]. They are intuitively used to relate probability measures for $\mathcal{M}$ and $\mathcal{M}_{i}$ .

The projection of a finite path $\pi\in Paths_{\mathcal{M}}^{fin}$ onto component $\mathcal{M}_{i}$ is the finite path ${\pi{\upharpoonright}_{\!i}}\in Paths_{\mathcal{M}_{i}}^{fin}$ obtained by restricting $\pi$ to the steps performed by $\mathcal{M}_{i}$ . Formally, ${({s^{\mathit{init}}_{1}},{s^{\mathit{init}}_{2}}){\upharpoonright}_{\!i}}={s^% {\mathit{init}}_{i}}$ and for $\pi=\pi^{\prime},(\alpha_{1},\alpha_{2}),(s_{1},s_{2})$ :

{\pi{\upharpoonright}_{\!i}}=\begin{cases}{\pi^{\prime}{\upharpoonright}_{\!i}% },\alpha_{i},s_{i}&\text{if }\alpha_{i}\in\mathit{Act}_{i}\\ {\pi^{\prime}{\upharpoonright}_{\!i}}&\text{otherwise.}\end{cases}

Path projections are neither injective nor surjective, i.e., we might have ${\pi{\upharpoonright}_{\!i}}={\pi^{\prime}{\upharpoonright}_{\!i}}$ for two distinct paths $\pi\neq\pi^{\prime}$ of $\mathcal{M}$ , and for some $\pi_{i}\in Paths_{\mathcal{M}_{i}}^{fin}$ there might not be any $\pi\in Paths_{\mathcal{M}}^{fin}$ with $\pi_{i}={\pi{\upharpoonright}_{\!i}}$ . We define the set of paths of $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ that are projected to $\pi_{i}\in Paths_{\mathcal{M}_{i}}^{fin}$ as

\pi_{i}\otimes\mathcal{M}_{3-i}=\big{\{}\pi\in Paths_{\mathcal{M}}^{fin}\mid% \pi_{i}={\pi{\upharpoonright}_{\!i}}\big{\}}.

We first focus on strategy projections for non-parametric PA. Then, we lift our notions to the parametric setting.

3.1 Projections for non-parametric PAs

We fix the parallel composition $\mathcal{N}=\mathcal{N}_{1}\parallel\mathcal{N}_{2}=\left(S_{\parallel},{s^{% \mathit{init}}_{\parallel}},\mathit{Act}_{\parallel},\mathbf{P}_{\parallel},L_% {\parallel}\right)$ of (non-parametric) PAs $\mathcal{N}_{1}$ and $\mathcal{N}_{2}$ with $\mathcal{N}_{i}=\left(S_{i},{s^{\mathit{init}}_{i}},\mathit{Act}_{i},\mathbf{P% }_{i},L_{i}\right)$ and alphabets $\Sigma_{i}$ for $i=1,2$ .

Definition 11 (Strategy Projection for PA).

The projection of a strategy $\sigma\in Str_{\!\mathcal{N}}^{\!\mathit{prt}}$ to $\mathcal{N}_{i}$ is the strategy ${{{\sigma{\upharpoonright}_{\!i}^{\mathcal{N}}}}}\in Str_{\!\mathcal{N}_{i}}^{% \!\mathit{prt}}$ , where for $\pi_{i}\in Paths_{\mathcal{M}_{i}}^{fin}$ and $\alpha_{i}\in\mathit{Act}_{i}$ :

\displaystyle{{{\sigma{\upharpoonright}_{\!i}^{\mathcal{N}}}}}(\pi_{i},\alpha_% {i})=\begin{cases}\displaystyle\frac{\sum_{s_{i}\in S_{i}}Pr_{\mathcal{N}}^{% \sigma}\!\left((\pi_{i},\alpha_{i},s_{i})\otimes\mathcal{N}_{3-i}\right)}{Pr_{% \mathcal{N}}^{\sigma}\!\left(\pi_{i}\otimes\mathcal{N}_{3-i}\right)}&\text{if % }Pr_{\mathcal{N}}^{\sigma}\!\left(\pi_{i}\otimes\mathcal{N}_{3-i}\right)>0\\ 0&\text{otherwise.}\end{cases}

If $\mathcal{N}$ is clear, we simply write ${{\sigma{\upharpoonright}_{\!i}}}$ instead of ${{{\sigma{\upharpoonright}_{\!i}^{\mathcal{N}}}}}$ . Lemmas 12 and 13 below yield that Definition 11 is equivalent to the projection defined in [35, Def. 6]. We argue that our variant is more intuitive since the numerator and denominator of the fraction consider the same probability measure $Pr_{\mathcal{N}}^{\sigma}$ . Intuitively, ${{\sigma{\upharpoonright}_{\!i}}}(\pi_{i},\alpha_{i})$ coincides with the conditional probability that – under $Pr_{\mathcal{N}}^{\sigma}$ and given that a path $\pi$ with projection ${\pi{\upharpoonright}_{\!i}}=\pi_{i}$ is observed – the next action of component $\mathcal{N}_{i}$ is $\alpha_{i}$ . We now provide an alternative characterization for the numerator given in Definition 11.

Lemma 12.

For $\sigma\in Str_{\!\mathcal{N}}^{\!\mathit{prt}}$ , $\pi_{i}\in Paths_{\mathcal{N}_{i}}^{fin}$ , and $\alpha_{i}\in\mathit{Act}_{i}$ :

\sum_{s_{i}\in S_{i}}Pr_{\mathcal{N}}^{\sigma}\!\left((\pi_{i},\alpha_{i},s_{i% })\otimes\mathcal{N}_{3-i}\right)\leavevmode\nobreak\ =\leavevmode\nobreak\ % \sum_{\pi\in(\pi_{i}\otimes\mathcal{N}_{3-i})}\leavevmode\nobreak\ \sum_{% \begin{subarray}{c}(\hat{\alpha}_{1},\hat{\alpha}_{2})\in\mathit{Act}_{% \parallel},\,\hat{\alpha}_{i}=\alpha_{i}\end{subarray}}Pr_{\mathcal{N}}^{% \sigma}\!\left(\pi\right)\cdot\sigma(\pi,(\hat{\alpha}_{1},\hat{\alpha}_{2})).

The next lemma is the key observation for strategy projections as it connects the probability measure $Pr_{\mathcal{N}}^{\sigma}$ for $\mathcal{N}$ and $Pr_{\mathcal{N}_{i}}^{{{\sigma{\upharpoonright}_{\!i}}}}$ for each component $\mathcal{N}_{i}$ .

Lemma 13.

For $\sigma\in Str_{\!\mathcal{N}}^{\!\mathit{prt}}$ and $\pi_{i}\in Paths_{\mathcal{N}_{i}}^{fin}$ : $Pr_{\mathcal{N}_{i}}^{{{\sigma{\upharpoonright}_{\!i}}}}\!\left(\pi_{i}\right)% =Pr_{\mathcal{N}}^{\sigma}\!\left(\pi_{i}\otimes\mathcal{N}_{3-i}\right)$ .

The following result lifts [35, Lemma 2] to our setting and states that fair (and therefore also complete) strategies have fair and complete projections.

Lemma 14.

Let $\mathcal{C}_{1}\subseteq 2^{\Sigma_{1}}$ and $\mathcal{C}_{2}\subseteq 2^{\Sigma_{2}}$ . If $\sigma\in Str_{\!\mathcal{N}}^{\!{{\mathit{fair}}_{\mathcal{C}_{1}\cup\mathcal% {C}_{2}\ }}\!\!}$ , then ${{\sigma{\upharpoonright}_{\!i}}}\in Str_{\!\mathcal{N}_{i}}^{\!{{\mathit{fair% }}_{\mathcal{C}_{i}\ }}\!\!}$ .

The converse of Lemma 14 does not hold: The projection ${\sigma{\upharpoonright}_{\!i}}$ might not be a complete strategy for $\mathcal{N}_{i}$ , even though $\sigma$ is complete for $\mathcal{N}$ . Furthermore, ${\sigma{\upharpoonright}_{\!i}}$ might not be memoryless, even if $\sigma$ is memoryless. The following example shows both cases.

Example 15 (Strategy Projection for pPA).

Consider the pPA $\mathcal{M}=\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ from Figure 2, using $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ depicted in Figure 1. We fix the valuation $\mathpzc{v}$ with $\mathpzc{v}(p)=\mathpzc{v}(q)=0.1$ and set $\mathcal{N}=\mathcal{M}[\mathpzc{v}]$ and $\mathcal{N}_{i}=\mathcal{M}_{i}[\mathpzc{v}]$ for $i=1,2$ . Let $\sigma\in Str_{\!\mathcal{N}_{1}\parallel\mathcal{N}_{2}}^{\!\mathit{mless},% \mathit{cmp}}$ that always selects the actions with label $\mathsf{a}$ , $\mathsf{c}$ , or $\frownie$ with probability 1 when available; otherwise, it chooses $\mathsf{b}$ .

We compute the projection ${{{\sigma{\upharpoonright}_{\!2}}}}$ to the PA $\mathcal{M}_{2}[\mathpzc{v}]$ :

$\blacksquare$

${{{\sigma{\upharpoonright}_{\!2}}}}(t_{0},\mathsf{a})=1$
$\blacksquare$

${{{\sigma{\upharpoonright}_{\!2}}}}((t_{0},\mathsf{a},t_{2}),\mathsf{c})=\frac% {(\mathpzc{v}(p))^{2}}{\mathpzc{v}(p)}=\mathpzc{v}(p)=0.1$
$\blacksquare$

${{{\sigma{\upharpoonright}_{\!2}}}}((t_{0},\mathsf{a},t_{2},\mathsf{c},t_{3}),% \frownie)=\frac{(\mathpzc{v}(p))^{2}\cdot\frac{1}{10}}{\mathpzc{v}(p)\cdot% \frac{1}{10}}=\mathpzc{v}(p)=0.1$

Similarly, ${{{\sigma{\upharpoonright}_{\!2}}}}((t_{0},\mathsf{a},t_{1}),\mathsf{a})=% \mathpzc{v}(p)=0.1$ and ${{{\sigma{\upharpoonright}_{\!2}}}}((t_{0},\mathsf{a},t_{1},\mathsf{a},t_{3}),% \frownie)=\mathpzc{v}(p)=0.1$ . We observe that the projection is not a complete strategy as $\frownie$ is the only available action in $t_{3}$ for $\mathcal{M}_{2}$ . Moreover, the projection is not memoryless, because, for example, ${{{\sigma{\upharpoonright}_{\!2}}}}((t_{0},\mathsf{a},t_{2},\mathsf{c},t_{4}),% \mathsf{c})=\mathpzc{v}(p)=0.1$ is not equal to ${{{\sigma{\upharpoonright}_{\!2}}}}((t_{0},\mathsf{a},t_{1},\mathsf{a},t_{4}),% \mathsf{c})=1.$

3.2 Projections for Parametric PAs

We now lift strategy projections to the parametric case. We fix the parallel composition $\mathcal{M}=\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ of two pPAs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ with a common set of parameters $V$ . Let $i=1,2$ and let $\mathpzc{v}_{i}\colon V\to\mathbb{R}$ be a well-defined valuation for $\mathcal{M}_{i}$ . We define strategy projections for pPAs in terms of the instantiated PAs.

Definition 16 (Strategy Projection for pPA).

The projection of a strategy $\sigma\in Str_{\!\mathcal{M}}^{\!\mathit{prt}}$ to pPA $\mathcal{M}_{i}$ w.r.t. $\mathpzc{v}_{1},\mathpzc{v}_{2}$ is the strategy ${{{\sigma{\upharpoonright}_{\!i}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}\in Str_{% \!\mathcal{M}_{i}}^{\!\mathit{prt}}$ , defined by ${{{\sigma{\upharpoonright}_{\!i}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}={{{% \sigma{\upharpoonright}_{\!i}^{\mathcal{M}_{1}[\mathpzc{v}_{1}]\parallel% \mathcal{M}_{2}[\mathpzc{v}_{2}]}}}}$ .

If the valuations coincide, i.e., $\mathpzc{v}_{1}=\mathpzc{v}_{2}=\mathpzc{v}$ , we write ${{{\sigma{\upharpoonright}_{\!i}^{\mathpzc{v}}}}}$ instead of ${{{\sigma{\upharpoonright}_{\!i}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}$ . Strategy projections depend on the parameter instantiations as the following example illustrates. Such strategies are also referred to as (parameter) dependent strategies [49, Def. 2.6].

Example 17 (Strategy Projection for pPA).

Consider $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ from Figure 2 and the strategy $\sigma$ as in Example 15. Let $\mathpzc{v}_{1}$ and $\mathpzc{v}_{2}$ be the valuations used for $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ , respectively, with $\mathpzc{v}_{1}(p)=\mathpzc{v}_{1}(q)=0.1$ , and $\mathpzc{v}_{2}(p)=\mathpzc{v}_{2}(q)=0.9$ . For the projection ${{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}$ to $\mathcal{M}_{2}$ , the following values are obtained:

$\blacksquare$

${{{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}}(t_{0},% \mathsf{a})=1$
$\blacksquare$

${{{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}}((t_{0}% ,\mathsf{a},t_{2}),\mathsf{c})=\frac{\mathpzc{v}_{1}(p)\cdot\mathpzc{v}_{2}(p)% }{\mathpzc{v}_{2}(p)}=\mathpzc{v}_{1}(p)=0.1$
$\blacksquare$

${{{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}}((t_{0}% ,\mathsf{a},t_{2},\mathsf{c},t_{3}),\frownie)=\frac{\mathpzc{v}_{1}(p)\cdot% \mathpzc{v}_{2}(p)\cdot\frac{1}{10}}{\mathpzc{v}_{2}(p)\cdot\frac{1}{10}}=% \mathpzc{v}_{1}(p)=0.1$ ,
$\blacksquare$

${{{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}}((t_{0}% ,\mathsf{a},t_{1}),\mathsf{a})=\mathpzc{v}_{1}(p)=0.1$ , and
$\blacksquare$

${{{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}}((t_{0}% ,\mathsf{a},t_{1},\mathsf{a},t_{3}),\frownie)=\mathpzc{v}_{1}(p)=0.1$ .

Note that the resulting projection coincides with the one computed in Example 15, where both components were instantiated using $\mathpzc{v}_{1}$ , i.e., ${{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}={{{% \sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1}}}}}={{{\sigma{\upharpoonright}_% {\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{1}}}}}$ .

The next lemma states that – when restricting to valuations that yield the same non-zero transitions – the strategy projection to $\mathcal{M}_{i}$ only depends on the parameter instantiation applied to $\mathcal{M}_{3-i}$ . This observation is the key insight for the correctness of the proof rule in Theorem 41, which enables compositional reasoning about monotonicity.

Lemma 18.

For $i=1,2$ , and well-defined valuations $\mathpzc{v}_{i},\mathpzc{v}_{i}^{\prime}\colon V\to\mathbb{R}$ for $\mathcal{M}_{i}$ such that $\mathbf{P}_{i}(s_{i},\alpha_{i},s_{i}^{\prime})[\mathpzc{v}_{i}]=0$ iff $\mathbf{P}_{i}(s_{i},\alpha_{i},s_{i}^{\prime})[\mathpzc{v}_{i}^{\prime}]=0$ we have: ${{{\sigma{\upharpoonright}_{\!1}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}={{{% \sigma{\upharpoonright}_{\!1}^{\mathpzc{v}_{1}^{\prime},\mathpzc{v}_{2}}}}}$ and ${{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}}}}}={{{% \sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{1},\mathpzc{v}_{2}^{\prime}}}}}$ .

4 Verification Objectives for pPAs

We define properties of interest for pPA verification. Let $\Sigma$ be a finite alphabet. $\Sigma^{\infty}=\Sigma^{*}\cup\Sigma^{\omega}$ denotes the set of all finite and infinite words over $\Sigma$ . For a word $\rho=\mathsf{a}_{0},\mathsf{a}_{1},\dots\in\Sigma^{\infty}$ and another alphabet $\widehat{\Sigma}$ , let ${\rho{\upharpoonright}_{\!\widehat{\Sigma}}}\in\widehat{\Sigma}^{\infty}$ denote the projection of $\rho$ onto $\widehat{\Sigma}$ – obtained by dropping all $\mathsf{a}_{i}\in\Sigma\setminus\widehat{\Sigma}$ from $\rho$ . The restriction ${\rho{\upharpoonright}_{\!\widehat{\Sigma}}}$ can be finite, even if $\rho$ is infinite.

We fix a pPA $\mathcal{M}=\left(S,{s^{\mathit{init}}},V,\mathit{Act},\mathbf{P},L\right)$ . The trace of $\pi=s_{0},\alpha_{0},s_{1},\alpha_{1},\dots\in Paths_{\mathcal{M}}^{inf}$ is the sequence $\mathit{tr}({\pi})=L(s_{0},\alpha_{0}),L(s_{1},\alpha_{1}),\dots$ of transition labels. The probability of a language $\mathcal{L}\subseteq\Sigma^{\infty}$ at a well-defined valuation $\mathpzc{v}$ under strategy $\sigma$ of $\mathcal{M}$ is given by

Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\mathcal{L}\right)=Pr_{\mathcal{M% }}^{\mathpzc{v},\sigma}\!\left(\{\pi\in Paths_{\mathcal{M}}^{inf}{}\mid{% \mathit{tr}({\pi}){\upharpoonright}_{\!\Sigma}}\in\mathcal{L}\}\right).

We also consider (parametric) expected total reward properties. Let $V$ be a set of parameters. A reward function $\mathcal{R}\colon\Sigma\to\mathbb{Q}[{V}]\cup\mathbb{R}_{\geq 0}$ over $\Sigma$ assigns a (potentially parametric) reward to each symbol $\mathsf{a}\in\Sigma$ . Instantiation of $\mathcal{R}$ at a valuation $\mathpzc{v}\colon V\to\mathbb{R}$ yields $\mathcal{R}[\mathpzc{v}]$ with $\mathcal{R}[\mathpzc{v}](\mathsf{a})=\mathcal{R}(\mathsf{a})[\mathpzc{v}]$ for all $\mathsf{a}\in\Sigma$ . Valuation $\mathpzc{v}$ is well-defined for $\mathcal{R}$ if $\mathcal{R}[\mathpzc{v}]\colon\Sigma\to\mathbb{R}_{\geq 0}$ . In this case, the accumulated reward for a word $\rho=\mathsf{a}_{0},\mathsf{a}_{1},\dots\in\Sigma^{\infty}$ is given by $\mathcal{R}[\mathpzc{v}](\rho)=\sum_{i=0}^{|\rho|}\mathcal{R}[\mathpzc{v}](% \mathsf{a}_{i})\in\mathbb{R}_{\geq 0}\cup\{\infty\}$ .

When applied to a pPA $\mathcal{M}$ , a reward function $\mathcal{R}$ assigns the reward $\mathcal{R}(L(s,\alpha))$ to the enabled state-action-pairs $(s,\alpha)\in\mathit{dom}(\mathbf{P})$ with $L(s,\alpha)\in\Sigma$ . For a well-defined valuation $\mathpzc{v}$ for $\mathcal{M}$ and $\mathcal{R}$ , we define the expected total reward under strategy $\sigma$ as

Ex_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\mathcal{R}\right)=\textstyle\int% _{\pi\in Paths_{\mathcal{M}}^{inf}{}}\mathcal{R}[\mathpzc{v}]\big{(}{\mathit{% tr}({\pi}){\upharpoonright}_{\!\Sigma}}\big{)}\,dPr_{\mathcal{M}}^{\mathpzc{v}% ,\sigma}\!\left(\pi\right).

We consider probabilistic and reward-based objectives as well as their multi-objective combinations.

Definition 19 (Objectives).

For ${\sim}\in\{>,\geq,<,\leq\}$ , $p\in[0,1]$ , and $r\in\mathbb{R}_{\geq 0}$ , we denote

$\blacksquare$

a probabilistic objective over $\mathcal{L}\subseteq\Sigma^{\infty}$ by $\mathbb{P}_{\sim p}\!(\mathcal{L})$ and
$\blacksquare$

a reward objective over $\mathcal{R}\colon\Sigma\to\mathbb{Q}[{V}]\cup\mathbb{R}_{\geq 0}$ by $\mathbb{E}_{\sim r}\!(\mathcal{R})$ .

Their satisfaction for a well-defined valuation $\mathpzc{v}$ and strategy $\sigma$ is defined by

\mathcal{M},\mathpzc{v},\sigma\models{}\!\mathbb{P}_{\sim p}\!(\mathcal{L})\ % \Leftrightarrow\ Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\mathcal{L}% \right)\sim p\quad\text{ and}\quad\mathcal{M},\mathpzc{v},\sigma\models{}\!% \mathbb{E}_{\sim r}\!(\mathcal{R})\ \Leftrightarrow\ Ex_{\mathcal{M}}^{% \mathpzc{v},\sigma}\!\left(\mathcal{R}\right)\sim r.

Let $\varphi{}\in\{\mathbb{P}_{\sim p}\!(\mathcal{L}),\mathbb{E}_{\sim r}\!(% \mathcal{R})\}$ refer to a (probabilistic or reward) objective. If neither $\mathcal{M}$ nor $\varphi{}$ consider any parameters, we may drop the valuation from the notation and just write $\mathcal{M},\sigma\models{}\!\varphi{}$ . We lift the satisfaction relation $\models{}\!$ to regions, i.e., sets of valuations.

Definition 20 (Region Satisfaction Relation).

Let $\star\in\{\mathit{prt},\mathit{cmp}\}\cup\{{{\mathit{fair}}_{\mathcal{C}\ }}\!% \!\mid\mathcal{C}\subseteq 2^{\Sigma_{\mathcal{M}}}\}$ . For objective $\varphi$ and well-defined region ${R}$ for $\mathcal{M}$ – and $\mathcal{R}$ if $\varphi{}=\mathbb{E}_{\sim r}\!(\mathcal{R})$ – the region satisfaction relation $\models^{\star}$ is given by:

\mathcal{M},{R}\models^{\star}\varphi{}\quad\Leftrightarrow\quad\forall% \mathpzc{v}\in{R}:\forall\sigma\in Str_{\!\mathcal{M}}^{\!\star}:\mathcal{M},% \mathpzc{v},\sigma\models{}\!\varphi{}.

Satisfaction under memoryless strategies – denoted by $\models^{\mathit{mless},\star}$ – is defined similarly.

$\blacktriangleright$ Remark 21.

For $\star\in\{\mathit{prt},\mathit{cmp}\}$ and any well-defined valuation $\mathpzc{v}$ we have $Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!\star}=Str_{\!\mathcal{M}}^{\!\star}$ . Thus, for well-defined ${R}$ , we can swap the quantifiers in Definition 20:

\mathcal{M},{R}\models^{\star}\varphi{}\quad\Leftrightarrow\quad\forall\sigma% \in Str_{\!\mathcal{M}}^{\!\star}:\forall\mathpzc{v}\in{R}:\mathcal{M},% \mathpzc{v},\sigma\models{}\!\varphi{}.

However, this is not the case for fair strategies and regions that are not graph-preserving: A strategy that is not ${{\mathit{fair}}_{\mathcal{C}\ }}\!\!$ for $\mathcal{M}$ (under graph-preserving instantiations) might be ${{\mathit{fair}}_{\mathcal{C}\ }}\!\!$ for $\mathcal{M}[\mathpzc{v}]$ if $\mathpzc{v}$ is not graph-preserving, because states that violate the fairness condition might not be reachable in $\mathcal{M}[\mathpzc{v}]$ . For a graph-preserving region ${R}$ and all $\mathpzc{v}\in{R}$ , we have $Str_{\!\mathcal{M}}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}=Str_{\!\mathcal{% M}[\mathpzc{v}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}$ . Thus, we can swap quantifiers as above.

Our framework also handles conjunctions of multiple objectives.

Definition 22 (MO-Query).

A multi-objective query (mo-query) is a set $\textsf{X}=\{\varphi{}_{1},\dots,\varphi{}_{n}\}$ of $n$ probabilistic or reward objectives with $\mathcal{M},\mathpzc{v},\sigma\models{}\!\textsf{X}\ \Leftrightarrow\ \mathcal% {M},\mathpzc{v},\sigma\models{}\!\varphi{}_{i}$ for all $\varphi{}_{i}\in\textsf{X}$ .

The conjunction of two mo-queries is a union of sets: $\textsf{X}_{1}\land\textsf{X}_{2}=\textsf{X}_{1}\cup\textsf{X}_{2}$ . We lift objective satisfaction for regions (Definition 20) to mo-queries in a straightforward way.

$\blacktriangleright$ Remark 23.

In [38] it is shown that model checking under partial strategies in $\mathcal{M}$ for probabilistic properties, rewards, and multi-objective queries reduces to model checking under complete strategies in a modified pPA, denoted $\mathcal{M}_{\tau}$ . This result extends [35, Proposition 2] to pPA while preserving memorylessness of the strategies.

We consider safety objectives as a special type of probabilistic objectives.

Definition 24 (Safety Objective).

$\mathbb{P}_{\geq p}\!(\mathcal{L})$ is a safety objective⁴⁴4Note that safety objectives contain all finite prefixes of words in $\mathcal{L}$ , i.e., they are prefix-closed. This is different in [35], where only infinite words are considered, leading to technical problems. See [38]. if $\mathcal{L}$ can be characterized by a DFA $\mathcal{A}^{bad}_{\mathcal{L}}$ accepting a language of finite words (bad prefixes):

\mathcal{L}=\{w\in\Sigma^{\infty}\mid\text{no prefix of $w$ is accepted by }% \mathcal{A}^{bad}_{\mathcal{L}}\}.

A mo-query is called safe, denoted $\textsf{X}^{\mathit{safe}}$ , if each $\varphi{}_{i}$ is a probabilistic safety objective.

For PA, computing the probability for a safety objective reduces to maximal reachability properties in the PA-DFA product [35, Lemma 1]. This result can be lifted to pPA in a straightforward manner; see [38]. For reachability and safety objectives, it is equivalent to quantify over complete or partial strategies. Lemma 25 lifts [35, Proposition 1] to pPA.

Lemma 25.

Let $\mathcal{M}$ be a pPA, let ${R}$ be a well-defined region and let $\mathbb{P}_{\geq p}\!(\mathcal{L})$ be a safety objective for $\mathcal{M}$ . It holds that: $\mathcal{M},{R}\models^{\mathit{cmp}}\mathbb{P}_{\geq p}\!(\mathcal{L})% \Leftrightarrow\mathcal{M},{R}\models^{\mathit{prt}}\mathbb{P}_{\geq p}\!(% \mathcal{L})$ . Same for $\models^{\mathit{mless},\star}$ .

4.1 Preservation Under Projection

We generalize the result from [35, Lemma 3] – originally stated in [46, Lemma 7.2.6] – to the parametric setting. In particular, we show that probabilistic and reward properties in a composed pPA $\mathcal{M}=\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ under a strategy $\sigma$ are preserved when projecting to either component $\mathcal{M}_{i}$ over $\Sigma_{i}$ , assuming a well-defined valuation $\mathpzc{v}$ .

Theorem 26.

For $i=1,2$ , let $\mathcal{L}$ be a language over $\Sigma_{i}$ and $\mathcal{R}$ be a reward function over $\Sigma_{i}$ . Then, for a well-defined valuation $\mathpzc{v}$ :

\displaystyle Pr_{{{\mathcal{M}_{i}}}}^{\mathpzc{v},{{{{\sigma{\upharpoonright% }_{\!i}^{\mathpzc{v}}}}}}}\!\left(\mathcal{L}\right)=Pr_{{{{\mathcal{M}_{1}}}% \parallel\mathcal{M}_{2}}}^{\mathpzc{v},\sigma}\!\left(\mathcal{L}\right)\quad% \text{ and }\quad Ex_{{\mathcal{M}_{i}}}^{\mathpzc{v},{{{{\sigma{% \upharpoonright}_{\!i}^{\mathpzc{v}}}}}}}\!\left(\mathcal{R}\right)=Ex_{{% \mathcal{M}_{1}}\parallel{\mathcal{M}_{2}}}^{\mathpzc{v},\sigma}\!\left(% \mathcal{R}\right)

Example 27.

Let $\mathcal{L}=\{w\in\{\mathsf{a},\mathsf{c},\frownie\}^{\infty}\mid\exists i\in% \mathbb{N}:w_{i}=\frownie\}$ be the language of words in which $\frownie$ occurs. Reconsider the strategy $\sigma$ of $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ from Example 17 and the projection ${{{{\sigma{\upharpoonright}_{\!{2}}^{\mathpzc{v}}}}}}$ to $\mathcal{M}_{2}$ . We have $Pr_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}^{\mathpzc{v},\sigma}\!\left(% \mathcal{L}\right)=Pr_{\mathcal{M}_{2}}^{\mathpzc{v},{{{{\sigma{% \upharpoonright}_{\!2}^{\mathpzc{v}}}}}}}\!\left(\mathcal{L}\right)=(\mathpzc{% v}(p))^{2}\cdot\frac{1}{10}+\mathpzc{v}(p)\cdot(1-\mathpzc{v}(p))\cdot\mathpzc% {v}(q))$ .

Theorem 26 assumes that the property only involves action labels from a single component $\mathcal{M}_{i}$ . To allow objectives over arbitrary alphabets $\Sigma$ , we can add a self-loop labeled $\mathsf{a}$ at every state, for each label $\mathsf{a}\notin\Sigma_{i}$ .

Definition 28 (Alphabet Extension).

Let $\mathcal{M}=\left(S,{s^{\mathit{init}}},V,\mathit{Act},\mathbf{P},L\right)$ be a pPA over $\Sigma_{\mathcal{M}}$ and let $\Sigma$ be an alphabet with $\mathit{Act}\cap(\Sigma\setminus\Sigma_{\mathcal{M}})=\emptyset$ . The alphabet extension of $\mathcal{M}$ with respect to $\Sigma$ is the pPA $\mathcal{M}{\langle\Sigma\rangle}=(S,{s^{\mathit{init}}},V,\mathit{Act}% \mathbin{\mathaccent 0{\cdot}\cup}(\Sigma\setminus\Sigma_{\mathcal{M}}),% \mathbf{P}_{\Sigma},L_{\Sigma})$ over alphabet $\Sigma_{\mathcal{M}}\cup\Sigma$ , where

$\blacksquare$

$\mathbf{P}_{\Sigma}(s,\alpha)=\mathbf{P}(s,\alpha)$ and $L_{\Sigma}(s,\alpha)=L(s,\alpha)$ for all $(s,\alpha)\in\mathit{dom}(\mathbf{P})$ and
$\blacksquare$

$\mathbf{P}_{\Sigma}(s,\mathsf{a})=\mathbbm{1}_{s}$ and $L_{\Sigma}(s,\mathsf{a})=\mathsf{a}$ for all $s\in S$ and $\mathsf{a}\in\Sigma\setminus\Sigma_{\mathcal{M}}$ .

Figure 3: Alphabet extension

\mathcal{M}_{2}{\langle\{\mathsf{a},\mathsf{b}\}\rangle}

of the pPA

\mathcal{M}_{2}

from Figure 1(b) to the alphabet

\{\mathsf{a},\mathsf{b}\}

.

Example 29 (Alphabet Extension).

Figure 3 shows $\mathcal{M}_{2}{\langle\{\mathsf{a},\mathsf{b}\}\rangle}$ for pPA $\mathcal{M}_{2}$ over $\Sigma_{2}=\{\mathsf{a},\mathsf{c},\frownie\}$ from Figure 1(b). Transitions with label $\mathsf{a}$ remain unchanged as $\mathsf{a}\in\Sigma_{2}$ , but an additional self-loop with action $\mathsf{b}\not\in\Sigma_{2}$ is added to every state.

We now lift [35, Lemma 3] to the parametric setting, covering properties and mo-queries over an alphabet that is not necessarily shared by $\mathcal{M}_{i}$ :

Theorem 30.

Let $\Sigma\subseteq\Sigma_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}$ , and $\sigma$ be a strategy for ${{\mathcal{M}_{1}{\langle\Sigma\rangle}}\parallel{\mathcal{M}_{2}{\langle% \Sigma\rangle}}}$ . Let $\mathcal{L}$ be a language over $\Sigma$ and $\mathcal{R}$ be a reward function over $\Sigma$ . Then, for well-defined valuation $\mathpzc{v}$ :

\displaystyle Pr_{{\mathcal{M}_{i}{\langle\Sigma\rangle}}}^{\mathpzc{v},{{{{% \sigma{\upharpoonright}_{\!i}^{\mathpzc{v}}}}}}}\!\left(\mathcal{L}\right)=Pr_% {{{\mathcal{M}_{1}{\langle\Sigma\rangle}}\parallel{\mathcal{M}_{2}{\langle% \Sigma\rangle}}}}^{\mathpzc{v},\sigma}\!\left(\mathcal{L}\right)\quad\text{ % and }\quad Ex_{{\mathcal{M}_{i}{\langle\Sigma\rangle}}}^{\mathpzc{v},{{{{% \sigma{\upharpoonright}_{\!i}^{\mathpzc{v}}}}}}}\!\left(\mathcal{R}\right)=Ex_% {{{\mathcal{M}_{1}{\langle\Sigma\rangle}}\parallel{\mathcal{M}_{2}{\langle% \Sigma\rangle}}}}^{\mathpzc{v},\sigma}\!\left(\mathcal{R}\right)

Let X be a mo-query over $\Sigma$ . Then, for any well-defined valuation $\mathpzc{v}$ :

\displaystyle{\mathcal{M}_{i}{\langle\Sigma\rangle}},\mathpzc{v},{{{{{\sigma{% \upharpoonright}_{\!i}^{\mathpzc{v}}}}}}}\models{}\!\textsf{X}\quad{% \Leftrightarrow}\quad({{\mathcal{M}_{1}{\langle\Sigma\rangle}}\parallel{% \mathcal{M}_{2}{\langle\Sigma\rangle}}}),\mathpzc{v},{\sigma}\models{}\!% \textsf{X}

$\blacktriangleright$ Remark 31.

Since alphabet extensions add self-loop transitions for new labels, and thus do not change the system’s state, the pPAs ${{\mathcal{M}_{1}{\langle\Sigma\rangle}}\parallel{\mathcal{M}_{2}{\langle% \Sigma\rangle}}}$ and $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ satisfy the same properties and mo-queries over the alphabet $\Sigma\subseteq\Sigma_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}$ .

Theorems 26 and 30 play a key role in the proof of the AG framework for reasoning about mo-queries and monotonicity, which will be established in Sections 5 and 6.

5 Assume-Guarantee Reasoning for pPA

Kwiatkowska et al. [35] introduced assume-guarantee (AG) reasoning proof rules for PA. This section extends their proof rules to the parametric setting. We first generalize the concept of AG triples to pPAs in Section 5.1. Then, we extend the asymmetric and circular proof rule in Section 5.2. Additional proof rules from [35] are presented in [38].

5.1 Assume-Guarantee Triples for pPA

We extend compositional reasoning to the parametric setting by generalizing assume-guarantee (AG) triples. Intuitively, an AG triple states that if a component satisfies an assumption, it also satisfies the guarantee under the same strategy and valuation.

Definition 32 (AG Triple).

The assume-guarantee triple for $\mathcal{M}$ , (parametric) mo-queries A (assumption) and G (guarantee), well-defined region ${R}$ , and $\star\in\{\mathit{cmp},\mathit{prt},{{\mathit{fair}}_{\mathcal{C}\ }}\!\!\}$ is

\displaystyle{\mathcal{M},{R}}\models^{\star}{\textsf{A}}{\rightarrow}{\textsf% {G}}\quad

\displaystyle\Leftrightarrow\quad\left(\forall\mathpzc{v}\in{R}:\forall\sigma% \in Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!\star}:\quad\mathcal{M},\mathpzc{v},{% \sigma}\models\textsf{A}\quad\rightarrow\quad\mathcal{M},\mathpzc{v},{\sigma}% \models\textsf{G}\right)

5.2 Assume-Guarantee Rules for pPA

We present AG proof rules for the compositional verification of parametric probabilistic automata (pPAs). In the remainder of this section, we fix two pPAs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ with alphabets $\Sigma_{1}$ , and $\Sigma_{2}$ , respectively. Further, let ${R}_{i}$ be a well-defined region for $\mathcal{M}_{i}$ .

First, we establish the asymmetric proof rule for safety and mo-queries – based on [35, Theorem 1 and 2], respectively – for pPA.

Theorem 33 (Asymmetric Rule).

Let A and G be mo-queries over $\Sigma_{\textsf{A}}\subseteq\Sigma_{1}$ and $\Sigma_{\textsf{G}}\subseteq\Sigma_{2}\cup\Sigma_{\textsf{A}}$ , respectively. Let $\mathcal{C}_{1}\subseteq 2^{\Sigma_{1}}$ and $\mathcal{C}_{2}\subseteq 2^{\Sigma_{2}\cup\Sigma_{\textsf{A}}}$ . Then, the two proof rules holds:

\mathcal{M}_{1}\parallel\mathcal{M}_{2},{{{R}_{1}}\!\cap{}\!{{R}_{2}}}\models^% {\mathit{cmp}}\textsf{G}^{\mathit{safe}}{\mathcal{M}_{2}{\langle\Sigma_{% \textsf{A}^{\mathit{safe}}}\rangle},{R}_{2}}\models^{\mathit{prt}}{\textsf{A}^% {\mathit{safe}}}{\rightarrow}{\textsf{G}^{\mathit{safe}}}\mathcal{M}_{1},{R}_{% 1}\models^{\mathit{cmp}}\textsf{A}^{\mathit{safe}}

\mathcal{M}_{1}\parallel\mathcal{M}_{2},{{{R}_{1}}\!\cap{}\!{{R}_{2}}}\models^% {{{\mathit{fair}}_{\mathcal{C}_{1}\cup\mathcal{C}_{2}\ }}\!\!}\textsf{G}{% \mathcal{M}_{2}{\langle\Sigma_{\textsf{A}}\rangle},{R}_{2}}\models^{{{\mathit{% fair}}_{\mathcal{C}_{2}\ }}\!\!}{\textsf{A}}{\rightarrow}{\textsf{G}}\mathcal{% M}_{1},{R}_{1}\models^{{{\mathit{fair}}_{\mathcal{C}_{1}\ }}\!\!}\textsf{A}

Proof sketch.

Let $\mathpzc{v}\in{{{R}_{1}}\!\cap{}\!{{R}_{2}}}$ , and $\sigma$ be a strategy for the composed pPA $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ . To prove validity of the rule, we need to show that $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ instantiated with $\mathpzc{v}$ satisfies $\textsf{G}^{\mathit{safe}}$ .

1.

Since $\mathpzc{v}\in{R}_{1}$ , the first premise implies $\mathcal{M}_{1},\mathpzc{v}\models^{\mathit{cmp}}\textsf{A}^{\mathit{safe}}$ , which is equivalent to $\mathcal{M}_{1},\mathpzc{v}\models^{\mathit{prt}}\textsf{A}^{\mathit{safe}}$ by Lemma 25. This implies that $\mathcal{M}_{1}$ under the partial strategy ${{{\sigma{\upharpoonright}_{\!\mathcal{M}_{1}}^{\mathpzc{v}}}}}$ also satisfies $\textsf{A}^{\mathit{safe}}$ . Since strategies and their projections satisfy the same properties (as shown in Theorem 30), we conclude that $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ instantiated at $\mathpzc{v}$ under the strategy $\sigma$ satisfies $\textsf{A}^{\mathit{safe}}$ .
2.

As $\mathpzc{v}\in{R}_{2}$ , the second premise implies that $\mathcal{M}_{2}[\mathpzc{v}]$ under the strategy ${{{\sigma{\upharpoonright}_{\!\mathcal{M}_{2}}^{\mathpzc{v}}}}}$ satisfies $\textsf{G}^{\mathit{safe}}$ . Again, Theorem 30 implies that $(\mathcal{M}_{1}\parallel\mathcal{M}_{2})[\mathpzc{v}]$ under the strategy $\sigma$ satisfies $\textsf{G}^{\mathit{safe}}$ .

Thus, we conclude that $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ instantiated at $\mathpzc{v}$ under $\sigma$ satisfies $\textsf{G}^{\mathit{safe}}$ . The rule on the right holds by a similar reasoning, where, in addition, Lemma 14 is used to establish that projections of fair strategies remain fair. $\hfill\blacktriangleleft$

Example 34 (Asymmetric Rule).

We illustrate the left proof rule from Theorem 33 for the pPA $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ in Figure 2 – composed of the pPAs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ depicted in Figure 1 – and w.r.t. $\textsf{G}=\mathbb{P}_{\geq 0.8}\!(\mathcal{L}_{G})$ , where $\mathcal{L}_{G}=\{w\in\{\mathsf{a},\mathsf{b},\mathsf{c},\frownie\}^{\infty}% \mid|w|_{\frownie}=0\}$ . Let $\textsf{A}=\{\mathbb{P}_{\geq 0.9}\!(\mathcal{L}_{A})\}$ , where $\mathcal{L}_{A}=\{w\in\{\mathsf{a},\mathsf{b}\}^{\infty}\mid|w|_{\mathsf{a}}% \leq 1\}$ . The pPA $\mathcal{M}_{2}{\langle\{\mathsf{a},\mathsf{b}\}\rangle}$ is depicted in Figure 3. For the premises of the proof rule, we obtain that the (largest) region ${R}$ for which $\mathcal{M}_{1},{R}_{1}\models^{\mathit{cmp}}\mathbb{P}_{\geq 0.9}\!(\mathcal{% L}_{A})$ is ${R}_{1}=\{\mathpzc{v}\colon\{p,q\}\to\mathbb{R}\mid\mathpzc{v}(p)\in[0,0.1]\}$ and the (largest) region ${R}_{2}$ for which ${\mathcal{M}_{2}{\langle\{\mathsf{a},\mathsf{b}\}\rangle},{R}_{2}}\models^{% \mathit{prt}}{\textsf{A}}{\rightarrow}{\textsf{G}}$ holds, is ${R}=\{\mathpzc{v}\colon\{p,q\}\to\mathbb{R}\mid(\mathpzc{v}(p)\in[0,0.5],% \mathpzc{v}(q)\in[0,1])\lor(\mathpzc{v}(p)\in(0.5,1),\mathpzc{v}(q)\in[0,2-2% \cdot p])\}$ . The intersection ${{{R}_{1}}\!\cap{}\!{{R}_{2}}}$ – for which $\mathcal{M}_{1}\parallel\mathcal{M}_{2},{{{R}_{1}}\!\cap{}\!{{R}_{2}}}\models^% {\mathit{prt}}\textsf{G}$ holds by [38, Theorem 52] – contains all valuations with $\mathpzc{v}(p)\in[0,0.1],\mathpzc{v}(q)\in[0,1]$ . The (largest) region ${R}$ for which $\mathcal{M}_{1}\parallel\mathcal{M}_{2},{R}\models^{\mathit{prt}}\textsf{G}$ is ${R}=\{\mathpzc{v}\colon{p,q}\to\mathbb{R}\mid(\mathpzc{v}(p)\in([0,\frac{1}{4}% ]\cup\{1\}),\mathpzc{v}(q)\in[0,1])\lor(\mathpzc{v}(p)\in(\frac{1}{4},1),% \mathpzc{v}(q)\in[0,\frac{p+1}{5\cdot p}])\}$ . This satisfies $({{{R}_{1}}\!\cap{}\!{{R}_{2}}})\subset{R}$ .

The proof rules in Theorem 33 can be extended to systems with more than two components, as detailed in [38, Theorem 52]. Next, we lift the circular proof rule given in [35, Theorem 5] to pPAs:

Theorem 35 (Circular Rule).

Let $\textsf{A}_{1}$ , $\textsf{A}_{2}$ and G be (parametric) mo-queries over $\Sigma_{\textsf{A}_{1}}\subseteq\Sigma_{2}$ , $\Sigma_{\textsf{A}_{2}}\subseteq\Sigma_{1}\cup\Sigma_{\textsf{A}_{1}}$ and $\Sigma_{\textsf{G}}\subseteq\Sigma_{2}\cup\Sigma_{\textsf{A}_{2}}$ , respectively. Let $\mathcal{C}_{i}\in 2^{\Sigma_{i}\cup\Sigma_{\textsf{A}_{i}}}$ for $i\in\{1,2\}$ , and $\mathcal{C}_{3}\in 2^{\Sigma_{2}}$ . Then:

\mathcal{M}_{1}\parallel\mathcal{M}_{2},{{{R}_{1}\!\cap{}{R}_{2}\!\cap{}{R}_{3% }}}\models^{\mathit{cmp}}\textsf{G}^{\mathit{safe}}\mathcal{M}_{2},{R}_{3}% \models^{\mathit{cmp}}\textsf{A}^{\mathit{safe}}_{1}{\mathcal{M}_{2}{\langle% \Sigma_{\textsf{A}^{\mathit{safe}}_{2}}\rangle},{R}_{2}}\models^{\mathit{prt}}% {\textsf{A}^{\mathit{safe}}_{2}}{\rightarrow}{\textsf{G}^{\mathit{safe}}}{% \mathcal{M}_{1}{\langle\Sigma_{\textsf{A}^{\mathit{safe}}_{1}}\rangle},{R}_{1}% }\models^{\mathit{prt}}{\textsf{A}^{\mathit{safe}}_{1}}{\rightarrow}{\textsf{A% }^{\mathit{safe}}_{2}}

\mathcal{M}_{1}\parallel\mathcal{M}_{2},{{{R}_{1}\!\cap{}{R}_{2}\!\cap{}{R}_{3% }}}\models^{{{\mathit{fair}}_{\mathcal{C}_{1}\cup\mathcal{C}_{2}\cup\mathcal{C% }_{3}\ }}\!\!}\textsf{G}\mathcal{M}_{2},{R}_{3}\models^{{{\mathit{fair}}_{% \mathcal{C}_{3}\ }}\!\!}\textsf{A}_{1}{\mathcal{M}_{2}{\langle\Sigma_{\textsf{% A}_{2}}\rangle},{R}_{2}}\models^{{{\mathit{fair}}_{\mathcal{C}_{2}\ }}\!\!}{% \textsf{A}_{2}}{\rightarrow}{\textsf{G}}{\mathcal{M}_{1}{\langle\Sigma_{% \textsf{A}_{1}}\rangle},{R}_{1}}\models^{{{\mathit{fair}}_{\mathcal{C}_{1}\ }}% \!\!}{\textsf{A}_{1}}{\rightarrow}{\textsf{A}_{2}}

Proof sketch.

Similar to Theorem 33, the proof of the circular rules makes use of Theorem 30, which establishes that the composition under a strategy satisfies the same properties as the individual components under their corresponding projections. For safety, Lemma 25 allows us to verify the condition for complete strategies rather than partial strategies in the third premise. For fairness, Lemma 14 ensures that strategy projections remain fair. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 36.

The inclusion of fairness in the premises of the right rules in Theorem 33 and Theorem 35 enables recursive application and thus supports the compositional verification of systems with more than two components. In the case of a single application of one of the rules, it is sufficient to verify with respect to complete strategies, which, while a stronger condition, simplifies the verification process.

6 Compositional Reasoning about Monotonicity

Exploiting monotonicity can significantly enhance the efficiency of parameter synthesis [51]. However, determining monotonicity is computationally hard⁵⁵5For deterministic pPA (Markov chains) determining monotonicity is coETR-hard [49, Sec. 3.4]. and it would be beneficial to determine monotonicity in a compositional way. Additionally, monotonicity in composed pPA is challenging due to the complexities introduced by parameter dependencies and interactions among components. While we focus on global monotonicity, the following results can be extended to local monotonicity, which considers only the first transition from a given state. See [49, Definitions 4.4 and 4.5].

The probability of a language or the expected total reward for a pPA $\mathcal{M}$ can be viewed as a function – called solution function – that maps a well-defined parameter valuation to the corresponding probability or expected total reward, respectively [27, Definition 4.7].

Definition 37 (Solution Function).

Let $\mathcal{M}$ be a pPA over $\Sigma$ , let $\sigma\in Str_{\!\mathcal{M}}^{\!}$ and let ${R}$ be a well-defined region. The solution function for $\mathcal{M}$ and language $\mathcal{L}\subseteq\Sigma^{\infty}$ is $\textsf{sol}_{\mathcal{M},\sigma}^{Pr\!\left(\mathcal{L}\right)}\colon{R}\to[0% ,1]$ , where $\textsf{sol}_{\mathcal{M},\sigma}^{Pr\!\left(\mathcal{L}\right)}(\mathpzc{v})=% Pr_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\mathcal{L}\right)$ . The solution function for $\mathcal{M}$ and a reward function $\mathcal{R}$ over $\Sigma$ is $\textsf{sol}_{\mathcal{M},\sigma}^{Ex\!\left(\mathcal{R}\right)}\colon{R}\to% \mathbb{R}_{\geq 0}$ , where $\textsf{sol}_{\mathcal{M},\sigma}^{Ex\!\left(\mathcal{R}\right)}(\mathpzc{v})=% Ex_{\mathcal{M}}^{\mathpzc{v},\sigma}\!\left(\mathcal{R}\right)$ .

When referring to a solution function without specifying whether it pertains to probabilities or expected rewards, we simply write $\textsf{sol}_{\mathcal{M},\sigma}$ .

Example 38 (Solution Function).

Consider the pPA $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ in Figure 2 and the region ${R}=\{\mathpzc{v}\colon\{p,q\}\to[0,1]\}$ which is well-defined for $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ . Let $\mathcal{L}=\{w\in\{\mathsf{a},\mathsf{c},\frownie\}^{\infty}\mid|w|_{\frownie% }=0\}$ be the language of words over $\{\mathsf{a},\mathsf{b},\mathsf{c},\frownie\}$ that do not contain $\frownie$ . Let $\sigma$ be the complete strategy of $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ from Example 17, which always selects action $\mathsf{a},\mathsf{c}$ or $\frownie$ with probability 1 whenever any of them is enabled; otherwise, it chooses $\mathsf{b}$ with probability 1. The solution function $\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2},\sigma}^{Pr\!\left(% \mathcal{L}\right)}\colon{R}\to[0,1]$ is defined by $\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2},\sigma}^{Pr\!\left(% \mathcal{L}\right)}(p,q)=1-\left(p^{2}\cdot\frac{1}{10}+p\cdot(1-p)\cdot(p% \cdot q+(1-p)\cdot q)\right)=1-\left(p^{2}\cdot\frac{1}{10}+(p-p^{2})\cdot q\right)$ .

We extend the standard notion of monotonicity [49] by differentiating between different strategy classes, including complete, partial, and fair strategies.

Definition 39 (Monotonicity).

Let $\sigma$ be a strategy of $\mathcal{M}$ . A solution function $\textsf{sol}_{\mathcal{M},\sigma}$ is monotonic increasing in $p\in V$ on region ${R}$ – denoted ${\textsf{sol}_{\mathcal{M},{\sigma}}}{\!\big{\uparrow}}_{{{p},{{R}}}}$ – if for all $\mathpzc{v},\mathpzc{v}_{+}\in{R}$ with $\mathpzc{v}_{+}(q)=\mathpzc{v}(q)+x\cdot\llbracket\,p{=}q\,\rrbracket$ for $q\in V$ and some $x\geq 0$ , we have: ${\textsf{sol}_{{\mathcal{M}},{\sigma}}}{}(\mathpzc{v})\leq{\textsf{sol}_{{% \mathcal{M}},{\sigma}}}{}(\mathpzc{v}_{+}).$

For $\star\in\{\mathit{prt},\mathit{cmp}\}$ , we write ${\textsf{sol}_{\mathcal{M}}}{\!\big{\uparrow}}_{{{p},{{R}}}}^{\star}$ if ${\textsf{sol}_{\mathcal{M},{\sigma}}}{\!\big{\uparrow}}_{{{p},{{R}}}}$ for all $\sigma\in Str_{\!\mathcal{M}}^{\!\star}$ . If ${R}$ is graph-preserving, we write ${\textsf{sol}_{\mathcal{M}}}{\!\big{\uparrow}}_{{{p},{{R}}}}^{{{\mathit{fair}}% _{\mathcal{C}\ }}\!\!}$ if ${\textsf{sol}_{\mathcal{M},{\sigma}}}{\!\big{\uparrow}}_{{{p},{{R}}}}$ holds for all fair strategies $\sigma\in Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }% }\!\!}$ , $\mathpzc{v}\in{R}$ .
Notations ${\textsf{sol}_{\mathcal{M},{\sigma}}}{\!\big{\downarrow}}_{{{p},{{R}}}}$ and ${\textsf{sol}_{\mathcal{M}}}{\!\big{\downarrow}}_{{{p},{{R}}}}^{\star}$ for monotonic decreasing $\textsf{sol}_{\mathcal{M},\sigma}$ are defined analogously.

We require the region to be graph-preserving when defining monotonicity w.r.t. fair strategies. This ensures that for any two valuations, $\mathpzc{v},\mathpzc{v}_{+}$ , we have $Str_{\!\mathcal{M}[\mathpzc{v}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}=Str% _{\!\mathcal{M}[\mathpzc{v}_{+}]}^{\!{{\mathit{fair}}_{\mathcal{C}\ }}\!\!}$ ; see Proposition 10.

$\blacktriangleright$ Remark 40.

Monotonicity for partial strategies w.r.t. general properties is equivalent to monotonicity for complete strategies in a modified pPA; see [38].

The following theorem states that monotonicity of a composed system can be verified by analyzing its individual components.

Theorem 41 (Monotonicity).

Let $\mathcal{M}_{1}$ , $\mathcal{M}_{2}$ be pPAs with alphabets $\Sigma_{1}$ and $\Sigma_{2}$ and ${R}_{i}$ be a graph-preserving region for $\mathcal{M}_{i}$ . Let $\textsf{sol}\in\{\textsf{sol}^{Pr\!\left(\mathcal{L}\right)},\textsf{sol}^{Ex% \!\left(\mathcal{R}\right)}\}$ be a solution function w.r.t. the language $\mathcal{L}$ or reward function $\mathcal{R}$ over $\Sigma\subseteq(\Sigma_{1}\cup\Sigma_{2})$ and let $\big{\updownarrow}\in\{\big{\uparrow},\big{\downarrow}\}$ . Let $\mathcal{C}_{i}\subseteq 2^{\Sigma_{1}\cup{\Sigma}}$ . Then the following two proof rules hold:

{\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}}{\!\big{\updownarrow}}% _{{{p},{{{{R}_{1}}\!\cap{}\!{{R}_{2}}}}}}^{\mathit{prt}}{\textsf{sol}_{% \mathcal{M}_{2}{\langle\Sigma\rangle}}}{\!\big{\updownarrow}}_{{{p},{{R}_{2}}}% }^{\mathit{prt}}{\textsf{sol}_{\mathcal{M}_{1}{\langle\Sigma\rangle}}}{\!\big{% \updownarrow}}_{{{p},{{R}_{1}}}}^{\mathit{prt}}

{\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}}{\!\big{\updownarrow}}% _{{{p},{{{{R}_{1}}\!\cap{}\!{{R}_{2}}}}}}^{{{\mathit{fair}}_{\mathcal{C}_{1}% \cup\mathcal{C}_{2}\ }}\!\!}{\textsf{sol}_{\mathcal{M}_{2}{\langle\Sigma% \rangle}}}{\!\big{\updownarrow}}_{{{p},{{R}_{2}}}}^{{{\mathit{fair}}_{\mathcal% {C}_{2}\ }}\!\!}{\textsf{sol}_{\mathcal{M}_{1}{\langle\Sigma\rangle}}}{\!\big{% \updownarrow}}_{{{p},{{R}_{1}}}}^{{{\mathit{fair}}_{\mathcal{C}_{1}\ }}\!\!}

Proof.

We show the premises imply ${\textsf{sol}_{\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}{% \langle\Sigma\rangle}}}{\!\big{\updownarrow}}_{{{p},{{{{R}_{1}}\!\cap{}\!{{R}_% {2}}}}}}^{\star}$ for $\star\in\{\mathit{prt},{{\mathit{fair}}_{\mathcal{C}_{1}\cup\mathcal{C}_{2}\ }% }\!\!\}$ , which directly implies that ${\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}}{\!\big{\updownarrow}}% _{{{p},{{{{R}_{1}}\!\cap{}\!{{R}_{2}}}}}}^{\star}$ holds, see Remark 31. We focus on the left rule, i.e., $\star=\mathit{prt}$ .

$\blacktriangleright$ Remark 42.

The proof for $\star={{\mathit{fair}}_{\mathcal{C}_{1}\cup\mathcal{C}_{2}\ }}\!\!$ is similar but additionally requires Lemma 14 in [38, Appendix A.4].

We further consider $\big{\updownarrow}=\big{\uparrow}$ . The case $\big{\updownarrow}=\big{\downarrow}$ follows analogously. Our proof is by contradiction. Assume that the premises hold but ${\textsf{sol}_{\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}{% \langle\Sigma\rangle}}}{\!\big{\uparrow}}_{{{p},{{R}_{1}\cap{R}_{2}}}}^{\star}$ does not hold. Thus, there is a strategy $\sigma\in Str_{\!(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2% }{\langle\Sigma\rangle})}^{\!\star}$ and valuations $\mathpzc{v},\mathpzc{v}_{+}\in{R}_{1}\cap{R}_{2}$ with $\mathpzc{v}_{+}(q)=\mathpzc{v}(q)+x\cdot\llbracket\,p{=}q\,\rrbracket$ for $q\in V$ and some $x\geq 0$ and

\displaystyle{\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel% \mathcal{M}_{2}{\langle\Sigma\rangle})},{\sigma}}}{}(\mathpzc{v})>{\textsf{sol% }_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}{\langle% \Sigma\rangle})},{\sigma}}}{}(\mathpzc{v}_{+}).

(1)

Theorem 30 yields ${\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}% {\langle\Sigma\rangle})},{\sigma}}}{}(\mathpzc{v})={\textsf{sol}_{{\mathcal{M}% _{1}{\langle\Sigma\rangle}},{{{{{\sigma{\upharpoonright}_{\!1}^{\mathpzc{v},% \mathpzc{v}}}}}}}}}{}(\mathpzc{v})$ . We have $\mathbf{P}_{\mathcal{M}_{1}{\langle\Sigma\rangle}}(s,\alpha,s^{\prime})[% \mathpzc{v}]=0$ iff $\mathbf{P}_{\mathcal{M}_{1}{\langle\Sigma\rangle}}(s,\alpha,s^{\prime})[% \mathpzc{v}_{+}]=0$ as $\mathpzc{v}$ and $\mathpzc{v}_{+}$ are graph preserving for $\mathcal{M}_{1}$ . Thus, we can apply Lemma 18 and obtain

$\displaystyle{\textsf{sol}_{{\mathcal{M}_{1}{\langle\Sigma\rangle}},{{{{{% \sigma{\upharpoonright}_{\!1}^{\mathpzc{v},\mathpzc{v}}}}}}}}}{}(\mathpzc{v})$	$\displaystyle={\textsf{sol}_{{\mathcal{M}_{1}{\langle\Sigma\rangle}},{{{{{% \sigma{\upharpoonright}_{\!1}^{\mathpzc{v}_{+},\mathpzc{v}}}}}}}}}{}(\mathpzc{% v})$	(by Lemma 18)
	$\displaystyle\leq{\textsf{sol}_{{\mathcal{M}_{1}{\langle\Sigma\rangle}},{{{{{% \sigma{\upharpoonright}_{\!1}^{\mathpzc{v}_{+},\mathpzc{v}}}}}}}}}{}(\mathpzc{% v}_{+})$	( ${{{{\sigma{\upharpoonright}_{\!1}^{\mathpzc{v}_{+},\mathpzc{v}}}}}}\in Str_{\!% \mathcal{M}_{1}{\langle\Sigma\rangle}}^{\!\mathit{prt}}$ , ${\textsf{sol}_{\mathcal{M}_{1}{\langle\Sigma\rangle}}}{\!\big{\uparrow}}_{{{p}% ,{{R}_{1}}}}^{\mathit{prt}}$ )
	$\displaystyle={\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel% \mathcal{M}_{2}{\langle\Sigma\rangle}[\mathpzc{v}])},{\sigma}}}{}(\mathpzc{v}_% {+})$	(by Theorem 30)

We observe that

\big{(}\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}{\langle% \Sigma\rangle}[\mathpzc{v}]\big{)}[\mathpzc{v}_{+}]\leavevmode\nobreak\ =% \leavevmode\nobreak\ \big{(}\mathcal{M}_{1}{\langle\Sigma\rangle}[\mathpzc{v}_% {+}]\parallel\mathcal{M}_{2}{\langle\Sigma\rangle}[\mathpzc{v}]\big{)}% \leavevmode\nobreak\ =\leavevmode\nobreak\ \big{(}\mathcal{M}_{1}{\langle% \Sigma\rangle}[\mathpzc{v}_{+}]\parallel\mathcal{M}_{2}{\langle\Sigma\rangle}% \big{)}[\mathpzc{v}].

Consequently, ${\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}% {\langle\Sigma\rangle}[\mathpzc{v}])},{\sigma}}}{}(\mathpzc{v}_{+})={\textsf{% sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}[\mathpzc{v}_{+}]\parallel% \mathcal{M}_{2}{\langle\Sigma\rangle}},{\sigma}}}{}(\mathpzc{v})$ . By a similar reasoning as above, we obtain

$\displaystyle{\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}[\mathpzc{v% }_{+}]\parallel\mathcal{M}_{2}{\langle\Sigma\rangle})},{\sigma}}}{}(\mathpzc{v})$	$\displaystyle={\textsf{sol}_{{\mathcal{M}_{2}{\langle\Sigma\rangle}},{{{{{% \sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{+},\mathpzc{v}}}}}}}}}{}(\mathpzc{% v})$	(by Theorem 30)
	$\displaystyle\leq{\textsf{sol}_{{\mathcal{M}_{2}{\langle\Sigma\rangle}},{{{{{% \sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{+},\mathpzc{v}}}}}}}}}{}(\mathpzc{% v}_{+})$	( ${{{{\sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{+},\mathpzc{v}}}}}}\in Str_{\!% \mathcal{M}_{2}{\langle\Sigma\rangle}}^{\!\mathit{prt}}$ , ${\textsf{sol}_{\mathcal{M}_{2}{\langle\Sigma\rangle}}}{\!\big{\uparrow}}_{{{p}% ,{{R}_{2}}}}^{\mathit{prt}}$ )
	$\displaystyle={\textsf{sol}_{{\mathcal{M}_{2}{\langle\Sigma\rangle}},{{{{{% \sigma{\upharpoonright}_{\!2}^{\mathpzc{v}_{+},\mathpzc{v}_{+}}}}}}}}}{}(% \mathpzc{v}_{+})$	(by Lemma 18 )
	$\displaystyle={\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel% \mathcal{M}_{2}{\langle\Sigma\rangle})},{\sigma}}}{}(\mathpzc{v}_{+})$	(by Theorem 30)

Thus, ${\textsf{sol}_{{(\mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}% {\langle\Sigma\rangle})},{\sigma}}}{}(\mathpzc{v})\leq{\textsf{sol}_{{(% \mathcal{M}_{1}{\langle\Sigma\rangle}\parallel\mathcal{M}_{2}{\langle\Sigma% \rangle})},{\sigma}}}{}(\mathpzc{v}_{+})$ , violating Equation 1. $\hfill\blacktriangleleft$

Example 43.

Reconsider the pPA $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ in Figure 2, the region ${R}=\{\mathpzc{v}\colon\{p,q\}\to[0,1]\}$ , and the language $\mathcal{L}=\{w\in\{a,c,\frownie\}^{\infty}\mid|w|_{\frownie}=0\}$ from Example 38. The pPA $\mathcal{M}_{1}\parallel\mathcal{M}_{2}$ is composed of the pPAs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ shown in Figure 1. The region ${R}$ is well-defined for $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ . We check whether $\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}^{Pr\!\left(\mathcal{L}% \right)}$ is monotonic in $q$ on ${R}$ via Theorem 41. Since the premises ${\textsf{sol}_{\mathcal{M}_{i}{\langle\Sigma_{\mathcal{L}}\rangle}}^{Pr\!\left% (\mathcal{L}\right)}}{\!\big{\downarrow}}_{{{q},{{R}}}}^{\mathit{prt}}$ for $i\in\{1,2\}$ are satisfied, we conclude ${\textsf{sol}_{\mathcal{M}_{1}\parallel\mathcal{M}_{2}}^{Pr\!\left(\mathcal{L}% \right)}}{\!\big{\downarrow}}_{{{q},{{R}}}}^{\mathit{prt}}$ .

7 Related Work

Compositional verification has been widely studied in both probabilistic and non-probabilistic systems. We summarize key contributions related to our work.

Jones’ rely-guarantee method [26] and Pnueli’s compositional proof system [44] for temporal logic laid the foundation for AG reasoning. Subsequent work focused on AG rules for systems using CTL^∗ [12] and developed AG reasoning for reactive modules [25, 1]. Automated AG reasoning techniques – developed by Pasareanu et al. [13, 41] – include learning-based assumption generation. More recent work has focused on circular AG reasoning [16] and verification-repair approaches [22].

AG reasoning has been lifted to probabilistic settings. Initial work by de Alfaro et al. [15] introduced AG rules for a probabilistic extension of reactive modules [25, 1]. Their model is similar to PA [47, 46], but limited to synchronous composition.

Kwiatkowska et al. [34, 21] generalized AG verification for PA, allowing more flexible parallel compositions and extending AG reasoning to probabilistic safety properties. Their approach reduces AG verification to multi-objective model checking, as proposed by Etessami et al. [17]. This was further refined in [35], enabling AG reasoning over a broader class of quantitative properties, including conjunctions over probabilistic liveness and expected rewards. Algorithmic learning-based assumption generation techniques [13, 23] were later adapted for AG reasoning in probabilistic settings [18, 19, 36]. Other assumption generation approaches include abstraction-refinement methods [32, 10], based on the CEGAR paradigm [11], and symbolic learning-based methods [24, 5]. AG reasoning has been applied to various real-world domains, including service-based workflow verification [6], large-scale IT systems [7], and autonomous systems with deep neural networks [42, 43].

AG reasoning has also been extended to systems with uncertainty, for example, [55] introduced an AG framework for verifying systems with components modeled by MDPs and partially observable MDPs (POMDPs). In contrast, our work considers a different type of uncertainty; We extend AG reasoning to parametric probabilistic automata (PA), leveraging research on parametric MDPs [27, 45, 28] and previous AG verification techniques [35]. Our framework allows to reason about monotonicity [49, 50, 51] in a compositional manner. To the best of our knowledge, this the first AG-based compositional verification framework for parametric PA. Existing modular proof systems have focused on parametric timed automata [2] or non-probabilistic parameterized systems [4, 48, 39], where concurrent programs are parameterized by the number of processes or threads in a configured instance.

Another recent line of research focuses on the sequential composition of MDPs rather than parallel decomposition: Junges and Spaan [30] introduced an abstraction-refinement approach for hierarchical probabilistic models, leveraging parametric MDPs to represent sets of similar subroutines. Recent work by Watanabe et al. [53] on mean-payoff games, applies category-theoretic string diagrams to the verification of sequentially composed MDPs.

8 Conclusion

We presented an assume-guarantee framework for compositional verification of parametric probabilistic automata, building on the proof rules for Segala’s PA by Kwiatkowska et al. [35]. In addition, we introduced new compositional proof rules to reason about monotonicity in composed systems. These contributions lay the theoretical foundations for modular verification of pPA. To the best of our knowledge, these are the first AG proof rules for probabilistic models with parametric transition probabilities.

Future work involves implementing the framework and demonstrating its effectiveness through case studies. Another direction is to deduce additional assume-guarantee rules – for example, reasoning about robust valuations or strategies, i.e, properties of the form: $\exists\mathpzc{v}\in{R}:\forall\sigma\in Str_{\!\mathcal{M}}^{\!\star}:% \mathcal{M}[\mathpzc{v}],{\sigma}\models{}\!\textsf{X}$ . Additionally, interesting directions include the modular verification of other properties, such as long-run average rewards or expected visiting times [37]. Other areas include extending verification to logics such as parametric LTL [9] and probabilistic CTL. Further research could also explore Markov automata with parameters, building on preliminary work in modular reasoning for continuous-time and continuous-space models [8]. Another interesting direction is adapting assume-guarantee reasoning for stochastic games [54] to a parametric setting.

References

[1] Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods Syst. Des., 15(1):7–48, 1999. doi:10.1023/A:1008739929481.
[2] Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, and Harald Ruess. Compositional parameter synthesis. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 60–68, 2016. doi:10.1007/978-3-319-48989-6_4.
[3] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[4] Samik Basu and C. R. Ramakrishnan. Compositional analysis for verification of parameterized systems. Theor. Comput. Sci., 354(2):211–229, 2006. doi:10.1016/J.TCS.2005.11.016.
[5] Redouane Bouchekir and Mohand Cherif Boukala. Toward implicit learning for the compositional verification of Markov decision processes. In Mohamed Faouzi Atig, Saddek Bensalem, Simon Bliudze, and Bruno Monsuez, editors, Verification and Evaluation of Computer and Communication Systems - 12th International Conference, VECoS 2018, Grenoble, France, September 26-28, 2018, Proceedings, volume 11181 of Lecture Notes in Computer Science, pages 200–217. Springer, 2018. doi:10.1007/978-3-030-00359-3_13.
[6] Redouane Bouchekir, Saïda Boukhedouma, and Mohand Cherif Boukala. Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes. In Yuri Merkuryev, Tuncer I. Ören, and Mohammad S. Obaidat, editors, Proceedings of the 6th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2016), Lisbon, Portugal, July 29-31, 2016, pages 244–253. SciTePress, 2016. doi:10.5220/0005978602440253.
[7] Radu Calinescu, Shinji Kikuchi, and Kenneth Johnson. Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In Radu Calinescu and David Garlan, editors, Large-Scale Complex IT Systems. Development, Operation and Management - 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012, Revised Selected Papers, volume 7539 of Lecture Notes in Computer Science, pages 303–329. Springer, 2012. doi:10.1007/978-3-642-34059-8_16.
[8] Luca Cardelli, Kim G. Larsen, and Radu Mardare. Modular Markovian logic. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 380–391. Springer, 2011. doi:10.1007/978-3-642-22012-8_30.
[9] Souymodip Chakraborty and Joost-Pieter Katoen. Parametric LTL on Markov chains. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 207–221. Springer, 2014. doi:10.1007/978-3-662-44602-7_17.
[10] Krishnendu Chatterjee, Martin Chmelik, and Przemyslaw Daca. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods Syst. Des., 47(2):230–264, 2015. doi:10.1007/S10703-015-0235-2.
[11] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer, 2000. doi:10.1007/10722167_15.
[12] Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989, pages 353–362. IEEE Computer Society, 1989. doi:10.1109/LICS.1989.39190.
[13] Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. Learning assumptions for compositional verification. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 331–346. Springer, 2003. doi:10.1007/3-540-36577-X_24.
[14] Conrado Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of Lecture Notes in Computer Science, pages 280–294. Springer, 2004. doi:10.1007/978-3-540-31862-0_21.
[15] Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science, pages 351–365. Springer, 2001. doi:10.1007/3-540-44685-0_24.
[16] Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. Automated circular assume-guarantee reasoning. Formal Aspects Comput., 30(5):571–595, 2018. doi:10.1007/S00165-017-0436-0.
[17] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci., 4(4), 2008. doi:10.2168/LMCS-4(4:8)2008.
[18] Lu Feng, Marta Z. Kwiatkowska, and David Parker. Compositional verification of probabilistic systems using learning. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pages 133–142. IEEE Computer Society, 2010. doi:10.1109/QEST.2010.24.
[19] Lu Feng, Marta Z. Kwiatkowska, and David Parker. Automated learning of probabilistic assumptions for compositional reasoning. In Dimitra Giannakopoulou and Fernando Orejas, editors, Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6603 of Lecture Notes in Computer Science, pages 2–17. Springer, 2011. doi:10.1007/978-3-642-19811-3_2.
[20] Lu Feng, Clemens Wiltsche, Laura R. Humphrey, and Ufuk Topcu. Controller synthesis for autonomous systems interacting with human operators. In ICCPS, pages 70–79. ACM, 2015. doi:10.1145/2735960.2735973.
[21] Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Automated verification techniques for probabilistic systems. In Marco Bernardo and Valérie Issarny, editors, Formal Methods for Eternal Networked Software Systems - 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011. Advanced Lectures, volume 6659 of Lecture Notes in Computer Science, pages 53–113. Springer, 2011. doi:10.1007/978-3-642-21455-4_3.
[22] Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, and Sarai Sheinvald. Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf., 24(5):667–689, 2022. doi:10.1007/S10009-022-00669-9.
[23] Anubhav Gupta, Kenneth L. McMillan, and Zhaohui Fu. Automated assumption generation for compositional verification. Formal Methods Syst. Des., 32(3):285–301, 2008. doi:10.1007/S10703-008-0050-0.
[24] Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and Lijun Zhang. Learning weighted assumptions for compositional verification of Markov decision processes. ACM Trans. Softw. Eng. Methodol., 25(3):21:1–21:39, 2016. doi:10.1145/2907943.
[25] Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. You assume, we guarantee: Methodology and case studies. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV ’98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 440–451. Springer, 1998. doi:10.1007/BFB0028765.
[26] Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596–619, 1983. doi:10.1145/69575.69577.
[27] Sebastian Junges. Parameter synthesis in Markov models. PhD thesis, RWTH Aachen University, Germany, 2020. URL: https://publications.rwth-aachen.de/record/783179.
[28] Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des., 62(1):181–259, 2024. doi:10.1007/S10703-023-00442-X.
[29] Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, and Tobias Winkler. The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci., 119:183–210, 2021. doi:10.1016/J.JCSS.2021.02.006.
[30] Sebastian Junges and Matthijs T. J. Spaan. Abstraction-refinement for hierarchical probabilistic models. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 102–123. Springer, 2022. doi:10.1007/978-3-031-13185-1_6.
[31] Joost-Pieter Katoen. The probabilistic model checking landscape. In LICS, pages 31–45. ACM, 2016. doi:10.1145/2933575.2934574.
[32] Anvesh Komuravelli, Corina S. Pasareanu, and Edmund M. Clarke. Assume-guarantee abstraction refinement for probabilistic systems. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 310–326. Springer, 2012. doi:10.1007/978-3-642-31424-7_25.
[33] Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Using probabilistic model checking in systems biology. SIGMETRICS Perform. Evaluation Rev., 35(4):14–21, 2008. doi:10.1145/1364644.1364651.
[34] Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Assume-guarantee verification for probabilistic systems. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 23–37. Springer, 2010. doi:10.1007/978-3-642-12002-2_3.
[35] Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38–65, 2013. doi:10.1016/J.IC.2013.10.001.
[36] Rui Li and Yang Liu. Compositional stochastic model checking probabilistic automata via symmetric assume-guarantee rule. In 17th IEEE International Conference on Software Engineering Research, Management and Applications, SERA 2019, Honolulu, HI, USA, May 29-31, 2019, pages 110–115. IEEE, 2019. doi:10.1109/SERA.2019.8886808.
[37] Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, and Tobias Winkler. Accurately computing expected visiting times and stationary distributions in Markov chains. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14571 of Lecture Notes in Computer Science, pages 237–257. Springer, 2024. doi:10.1007/978-3-031-57249-4_12.
[38] Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen. Compositional reasoning for parametric probabilistic automata, 2025. arXiv:2506.08525.
[39] Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 589–606. Springer, 2016. doi:10.1007/978-3-662-49674-9_39.
[40] Gethin Norman and Vitaly Shmatikov. Analysis of probabilistic contract signing. J. Comput. Secur., 14(6):561–589, 2006. doi:10.3233/jcs-2006-14604.
[41] Corina S. Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M. Cobleigh, and Howard Barringer. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des., 32(3):175–205, 2008. doi:10.1007/S10703-008-0049-6.
[42] Corina S. Pasareanu, Divya Gopinath, and Huafeng Yu. Compositional verification for autonomous systems with deep learning components. CoRR, abs/1810.08303, 2018. arXiv:1810.08303.
[43] Corina S. Pasareanu, Ravi Mangal, Divya Gopinath, and Huafeng Yu. Assumption generation for learning-enabled autonomous systems. In Panagiotis Katsaros and Laura Nenzi, editors, Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3-6, 2023, Proceedings, volume 14245 of Lecture Notes in Computer Science, pages 3–22. Springer, 2023. doi:10.1007/978-3-031-44267-4_1.
[44] Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8-19 October 1984, volume 13 of NATO ASI Series, pages 123–144. Springer, 1984. doi:10.1007/978-3-642-82453-1_5.
[45] Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter synthesis for Markov models: Faster than ever. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 50–67, 2016. doi:10.1007/978-3-319-46520-3_4.
[46] Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. URL: https://hdl.handle.net/1721.1/36560.
[47] Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. Nord. J. Comput., 2(2):250–273, 1995.
[48] Antti Siirtola and Keijo Heljanko. Parametrised compositional verification with multiple process and data types. In Josep Carmona, Mihai T. Lazarescu, and Marta Pietkiewicz-Koutny, editors, 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013, pages 60–69. IEEE Computer Society, 2013. doi:10.1109/ACSD.2013.9.
[49] Jip Spel. Monotonicity in Markov models. PhD thesis, RWTH Aachen University, Germany, 2023. URL: https://publications.rwth-aachen.de/record/974903.
[50] Jip Spel, Sebastian Junges, and Joost-Pieter Katoen. Are parametric Markov chains monotonic? In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 479–496. Springer, 2019. doi:10.1007/978-3-030-31784-3_28.
[51] Jip Spel, Sebastian Junges, and Joost-Pieter Katoen. Finding provably optimal Markov chains. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 173–190. Springer, 2021. doi:10.1007/978-3-030-72016-2_10.
[52] Mariëlle Stoelinga. An introduction to probabilistic automata. Bull. EATCS, 78:176–198, 2002.
[53] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, and Matthias Volk, editors, Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, volume 15262 of Lecture Notes in Computer Science, pages 423–445. Springer, 2024. doi:10.1007/978-3-031-75778-5_20.
[54] Clemens Wiltsche. Assume-guarantee strategy synthesis for stochastic games. PhD thesis, University of Oxford, UK, 2015. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.719857.
[55] Xiaobin Zhang, Bo Wu, and Hai Lin. Assume-guarantee reasoning framework for MDP-POMDP. In 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016, pages 795–800. IEEE, 2016. doi:10.1109/CDC.2016.7798365.

[bib.bib1] [1] Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods Syst. Des., 15(1):7–48, 1999. doi:10.1023/A:1008739929481.

[bib.bib2] [2] Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, and Harald Ruess. Compositional parameter synthesis. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 60–68, 2016. doi:10.1007/978-3-319-48989-6_4.

[bib.bib3] [3] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.

[bib.bib4] [4] Samik Basu and C. R. Ramakrishnan. Compositional analysis for verification of parameterized systems. Theor. Comput. Sci., 354(2):211–229, 2006. doi:10.1016/J.TCS.2005.11.016.

[bib.bib5] [5] Redouane Bouchekir and Mohand Cherif Boukala. Toward implicit learning for the compositional verification of Markov decision processes. In Mohamed Faouzi Atig, Saddek Bensalem, Simon Bliudze, and Bruno Monsuez, editors, Verification and Evaluation of Computer and Communication Systems - 12th International Conference, VECoS 2018, Grenoble, France, September 26-28, 2018, Proceedings, volume 11181 of Lecture Notes in Computer Science, pages 200–217. Springer, 2018. doi:10.1007/978-3-030-00359-3_13.

[bib.bib6] [6] Redouane Bouchekir, Saïda Boukhedouma, and Mohand Cherif Boukala. Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes. In Yuri Merkuryev, Tuncer I. Ören, and Mohammad S. Obaidat, editors, Proceedings of the 6th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2016), Lisbon, Portugal, July 29-31, 2016, pages 244–253. SciTePress, 2016. doi:10.5220/0005978602440253.

[bib.bib7] [7] Radu Calinescu, Shinji Kikuchi, and Kenneth Johnson. Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In Radu Calinescu and David Garlan, editors, Large-Scale Complex IT Systems. Development, Operation and Management - 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012, Revised Selected Papers, volume 7539 of Lecture Notes in Computer Science, pages 303–329. Springer, 2012. doi:10.1007/978-3-642-34059-8_16.

[bib.bib8] [8] Luca Cardelli, Kim G. Larsen, and Radu Mardare. Modular Markovian logic. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 380–391. Springer, 2011. doi:10.1007/978-3-642-22012-8_30.

[bib.bib9] [9] Souymodip Chakraborty and Joost-Pieter Katoen. Parametric LTL on Markov chains. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 207–221. Springer, 2014. doi:10.1007/978-3-662-44602-7_17.

[bib.bib10] [10] Krishnendu Chatterjee, Martin Chmelik, and Przemyslaw Daca. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods Syst. Des., 47(2):230–264, 2015. doi:10.1007/S10703-015-0235-2.

[bib.bib11] [11] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer, 2000. doi:10.1007/10722167_15.

[bib.bib12] [12] Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989, pages 353–362. IEEE Computer Society, 1989. doi:10.1109/LICS.1989.39190.

[bib.bib13] [13] Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. Learning assumptions for compositional verification. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 331–346. Springer, 2003. doi:10.1007/3-540-36577-X_24.

[bib.bib14] [14] Conrado Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of Lecture Notes in Computer Science, pages 280–294. Springer, 2004. doi:10.1007/978-3-540-31862-0_21.

[bib.bib15] [15] Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science, pages 351–365. Springer, 2001. doi:10.1007/3-540-44685-0_24.

[bib.bib16] [16] Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. Automated circular assume-guarantee reasoning. Formal Aspects Comput., 30(5):571–595, 2018. doi:10.1007/S00165-017-0436-0.

[bib.bib17] [17] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci., 4(4), 2008. doi:10.2168/LMCS-4(4:8)2008.

[bib.bib18] [18] Lu Feng, Marta Z. Kwiatkowska, and David Parker. Compositional verification of probabilistic systems using learning. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pages 133–142. IEEE Computer Society, 2010. doi:10.1109/QEST.2010.24.

[bib.bib19] [19] Lu Feng, Marta Z. Kwiatkowska, and David Parker. Automated learning of probabilistic assumptions for compositional reasoning. In Dimitra Giannakopoulou and Fernando Orejas, editors, Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6603 of Lecture Notes in Computer Science, pages 2–17. Springer, 2011. doi:10.1007/978-3-642-19811-3_2.

[bib.bib20] [20] Lu Feng, Clemens Wiltsche, Laura R. Humphrey, and Ufuk Topcu. Controller synthesis for autonomous systems interacting with human operators. In ICCPS, pages 70–79. ACM, 2015. doi:10.1145/2735960.2735973.

[bib.bib21] [21] Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Automated verification techniques for probabilistic systems. In Marco Bernardo and Valérie Issarny, editors, Formal Methods for Eternal Networked Software Systems - 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011. Advanced Lectures, volume 6659 of Lecture Notes in Computer Science, pages 53–113. Springer, 2011. doi:10.1007/978-3-642-21455-4_3.

[bib.bib22] [22] Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, and Sarai Sheinvald. Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf., 24(5):667–689, 2022. doi:10.1007/S10009-022-00669-9.

[bib.bib23] [23] Anubhav Gupta, Kenneth L. McMillan, and Zhaohui Fu. Automated assumption generation for compositional verification. Formal Methods Syst. Des., 32(3):285–301, 2008. doi:10.1007/S10703-008-0050-0.

[bib.bib24] [24] Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and Lijun Zhang. Learning weighted assumptions for compositional verification of Markov decision processes. ACM Trans. Softw. Eng. Methodol., 25(3):21:1–21:39, 2016. doi:10.1145/2907943.

[bib.bib25] [25] Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. You assume, we guarantee: Methodology and case studies. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV ’98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 440–451. Springer, 1998. doi:10.1007/BFB0028765.

[bib.bib26] [26] Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596–619, 1983. doi:10.1145/69575.69577.

[bib.bib27] [27] Sebastian Junges. Parameter synthesis in Markov models. PhD thesis, RWTH Aachen University, Germany, 2020. URL: https://publications.rwth-aachen.de/record/783179.

[bib.bib28] [28] Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des., 62(1):181–259, 2024. doi:10.1007/S10703-023-00442-X.

[bib.bib29] [29] Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, and Tobias Winkler. The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci., 119:183–210, 2021. doi:10.1016/J.JCSS.2021.02.006.

[bib.bib30] [30] Sebastian Junges and Matthijs T. J. Spaan. Abstraction-refinement for hierarchical probabilistic models. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 102–123. Springer, 2022. doi:10.1007/978-3-031-13185-1_6.

[bib.bib31] [31] Joost-Pieter Katoen. The probabilistic model checking landscape. In LICS, pages 31–45. ACM, 2016. doi:10.1145/2933575.2934574.

[bib.bib32] [32] Anvesh Komuravelli, Corina S. Pasareanu, and Edmund M. Clarke. Assume-guarantee abstraction refinement for probabilistic systems. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 310–326. Springer, 2012. doi:10.1007/978-3-642-31424-7_25.

[bib.bib33] [33] Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Using probabilistic model checking in systems biology. SIGMETRICS Perform. Evaluation Rev., 35(4):14–21, 2008. doi:10.1145/1364644.1364651.

[bib.bib34] [34] Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Assume-guarantee verification for probabilistic systems. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 23–37. Springer, 2010. doi:10.1007/978-3-642-12002-2_3.

[bib.bib35] [35] Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38–65, 2013. doi:10.1016/J.IC.2013.10.001.

[bib.bib36] [36] Rui Li and Yang Liu. Compositional stochastic model checking probabilistic automata via symmetric assume-guarantee rule. In 17th IEEE International Conference on Software Engineering Research, Management and Applications, SERA 2019, Honolulu, HI, USA, May 29-31, 2019, pages 110–115. IEEE, 2019. doi:10.1109/SERA.2019.8886808.

[bib.bib37] [37] Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, and Tobias Winkler. Accurately computing expected visiting times and stationary distributions in Markov chains. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14571 of Lecture Notes in Computer Science, pages 237–257. Springer, 2024. doi:10.1007/978-3-031-57249-4_12.

[bib.bib38] [38] Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen. Compositional reasoning for parametric probabilistic automata, 2025. arXiv:2506.08525.

[bib.bib39] [39] Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 589–606. Springer, 2016. doi:10.1007/978-3-662-49674-9_39.

[bib.bib40] [40] Gethin Norman and Vitaly Shmatikov. Analysis of probabilistic contract signing. J. Comput. Secur., 14(6):561–589, 2006. doi:10.3233/jcs-2006-14604.

[bib.bib41] [41] Corina S. Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M. Cobleigh, and Howard Barringer. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des., 32(3):175–205, 2008. doi:10.1007/S10703-008-0049-6.

[bib.bib42] [42] Corina S. Pasareanu, Divya Gopinath, and Huafeng Yu. Compositional verification for autonomous systems with deep learning components. CoRR, abs/1810.08303, 2018. arXiv:1810.08303.

[bib.bib43] [43] Corina S. Pasareanu, Ravi Mangal, Divya Gopinath, and Huafeng Yu. Assumption generation for learning-enabled autonomous systems. In Panagiotis Katsaros and Laura Nenzi, editors, Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3-6, 2023, Proceedings, volume 14245 of Lecture Notes in Computer Science, pages 3–22. Springer, 2023. doi:10.1007/978-3-031-44267-4_1.

[bib.bib44] [44] Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8-19 October 1984, volume 13 of NATO ASI Series, pages 123–144. Springer, 1984. doi:10.1007/978-3-642-82453-1_5.

[bib.bib45] [45] Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter synthesis for Markov models: Faster than ever. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 50–67, 2016. doi:10.1007/978-3-319-46520-3_4.

[bib.bib46] [46] Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. URL: https://hdl.handle.net/1721.1/36560.

[bib.bib47] [47] Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. Nord. J. Comput., 2(2):250–273, 1995.

[bib.bib48] [48] Antti Siirtola and Keijo Heljanko. Parametrised compositional verification with multiple process and data types. In Josep Carmona, Mihai T. Lazarescu, and Marta Pietkiewicz-Koutny, editors, 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013, pages 60–69. IEEE Computer Society, 2013. doi:10.1109/ACSD.2013.9.

[bib.bib49] [49] Jip Spel. Monotonicity in Markov models. PhD thesis, RWTH Aachen University, Germany, 2023. URL: https://publications.rwth-aachen.de/record/974903.

[bib.bib50] [50] Jip Spel, Sebastian Junges, and Joost-Pieter Katoen. Are parametric Markov chains monotonic? In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 479–496. Springer, 2019. doi:10.1007/978-3-030-31784-3_28.

[bib.bib51] [51] Jip Spel, Sebastian Junges, and Joost-Pieter Katoen. Finding provably optimal Markov chains. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 173–190. Springer, 2021. doi:10.1007/978-3-030-72016-2_10.

[bib.bib52] [52] Mariëlle Stoelinga. An introduction to probabilistic automata. Bull. EATCS, 78:176–198, 2002.

[bib.bib53] [53] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, and Matthias Volk, editors, Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, volume 15262 of Lecture Notes in Computer Science, pages 423–445. Springer, 2024. doi:10.1007/978-3-031-75778-5_20.

[bib.bib54] [54] Clemens Wiltsche. Assume-guarantee strategy synthesis for stochastic games. PhD thesis, University of Oxford, UK, 2015. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.719857.

[bib.bib55] [55] Xiaobin Zhang, Bo Wu, and Hai Lin. Assume-guarantee reasoning framework for MDP-POMDP. In 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016, pages 795–800. IEEE, 2016. doi:10.1109/CDC.2016.7798365.

Compositional Reasoning for Parametric Probabilistic Automata

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Example 1.

Contributions.

2 Preliminaries

2.1 Parametric Probabilistic Automata

Definition 2.

Example 3 (pPA).

Definition 4.

Example 5.

▶ Remark 6.

Definition 7 (Parallel Composition).

Example 8 (Parallel Composition).

Definition 9 (Fair Strategy).

Proposition 10.

3 Strategy Projections

3.1 Projections for non-parametric PAs

Definition 11 (Strategy Projection for PA).

Lemma 12.

Lemma 13.

Lemma 14.

Example 15 (Strategy Projection for pPA).

3.2 Projections for Parametric PAs

Definition 16 (Strategy Projection for pPA).

Example 17 (Strategy Projection for pPA).

Lemma 18.

4 Verification Objectives for pPAs

Definition 19 (Objectives).

Definition 20 (Region Satisfaction Relation).

▶ Remark 21.

Definition 22 (MO-Query).

▶ Remark 23.

Definition 24 (Safety Objective).

Lemma 25.

4.1 Preservation Under Projection

Theorem 26.

Example 27.

Definition 28 (Alphabet Extension).

Example 29 (Alphabet Extension).

Theorem 30.

▶ Remark 31.

5 Assume-Guarantee Reasoning for pPA

5.1 Assume-Guarantee Triples for pPA

Definition 32 (AG Triple).

5.2 Assume-Guarantee Rules for pPA

Theorem 33 (Asymmetric Rule).

Proof sketch.

Example 34 (Asymmetric Rule).

Theorem 35 (Circular Rule).

Proof sketch.

▶ Remark 36.

6 Compositional Reasoning about Monotonicity

Definition 37 (Solution Function).

Example 38 (Solution Function).

Definition 39 (Monotonicity).

▶ Remark 40.

Theorem 41 (Monotonicity).

Proof.

▶ Remark 42.

Example 43.

7 Related Work

8 Conclusion

References

$\blacktriangleright$ Remark 6.

$\blacktriangleright$ Remark 21.

$\blacktriangleright$ Remark 23.

$\blacktriangleright$ Remark 31.

$\blacktriangleright$ Remark 36.

$\blacktriangleright$ Remark 40.

$\blacktriangleright$ Remark 42.