Paper deep dive
Supermartingale Certificates for Parametric MDPs
Kaushik Mallik, Ðorđe Žikelić
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 9/19/2026, 2:55:31 AM
Summary
This paper introduces a novel framework for the formal verification and synthesis of parametric Markov Decision Processes (pMDPs) with general measurable state and action spaces. The core contribution is a 'parameter flattening transformation' that converts parametric MDPs into semantically equivalent non-parametric MDPs. This enables the use of 'parametric supermartingale certificates,' a generalization of traditional supermartingale certificates, to design algorithms for verification and approximate synthesis in polynomial arithmetic pMDPs. The authors provide the first such algorithms for general state/action spaces and demonstrate their approach via a prototype implementation on continuous parametric random walk benchmarks.
Entities (9)
Relation Signals (6)
Kaushik Mallik → affiliatedwith → IMDEA Software Institute
confidence 95% · Affiliation: IMDEA Software Institute, Madrid, Spain
Đorđe Žikelić → affiliatedwith → Nanyang Technological University
confidence 95% · Affiliation: Nanyang Technological University, Singapore, Singapore
Parameter Flattening Transformation → transforms → Parametric Markov Decision Process
confidence 95% · The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs.
Parametric Supermartingale Certificate → enables → Verification
confidence 90% · We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis...
Parametric Supermartingale Certificate → enables → Synthesis
confidence 90% · We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis...
Parametric Supermartingale Certificate → generalizes → Supermartingale Certificate
confidence 90% · parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.
Tags
Links
- Source: https://arxiv.org/abs/2609.12715v1
- Canonical: https://arxiv.org/abs/2609.12715v1
Trouble viewing inline? Open PDF directly →
Full Text
119,016 characters extracted from source content.
Expand or collapse full text
Supermartingale Certificates for Parametric MDPs Kaushik Mallik🖂 Affiliation: IMDEA Software Institute, Madrid, Spain E-mail kaushik.mallik@imdea.org Đorđe Žikelić 🖂 Affiliation: Nanyang Technological University, Singapore, Singapore E-mail djordje.zikelic@ntu.edu.sg Abstract We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates—used for non-parametric MDPs—to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks. Keywords: MDPs Parameter synthesis Supermartingales. 1 Introduction Markov decision processes (MDPs) are a standard model for sequential decision making under probabilistic uncertainty [41]. A central assumption underlying classical MDPs and their probabilistic model checking algorithms is that all transition probabilities are exactly known. In practice, however, transition probabilities often depend on quantities such as failure rates, packet loss probabilities, or environmental conditions, whose values are rarely known precisely [32]. Parametric Markov decision processes (pMDPs) address this limitation by allowing transition probabilities to depend on finitely many real-valued parameters [33]. The values of parameters may be unknown or only partially known, for instance when they are constrained to lie within given bounds [27]. As a result, pMDPs can model uncertainties in probabilistic dynamics, including complex dependencies such as multivariate polynomial transition probabilities [32, 33]. Substantial progress has been made in the probabilistic model checking of parametric Markov chains and finite-state pMDPs [23, 31, 25, 43, 8, 28, 21, 22]. The core problems studied in this setting are parameter verification—establishing that a specification holds for all parameter valuations in a given region—and parameter synthesis—computing regions of parameter valuations for which the specification is satisfied [33]. Due to the inherent complexity of exact synthesis, approximate synthesis variants are also considered. Most existing methods are restricted to pMDPs with finite state and action spaces, whereas infinite space models are common in many applications, such as stochastic control and robotics [26], and probabilistic programs with unbounded or continuous state spaces [9]. Addressing this gap is our main motivation. Our contributions. We initiate the study of automated verification and synthesis for pMDPs with general measurable state and action spaces, by using supermartingale certificates. Supermartingale certificates are locally checkable proof rules with strong theoretical foundations in probability theory [49], that were successfully applied to a wide range of properties in non-parametric stochastic systems, including reachability [11, 13, 12, 38, 3, 16, 36, 17, 37, 34], safety [40, 45, 18, 46, 52, 47, 1, 48], reach-avoidance [50, 53, 54, 51], and ω-regular specifications [4, 30, 5, 35, 2]. However, they have not been considered in the parametric setting. Our first contribution is the parameter flattening transformation of pMDPs that embeds parameter valuations into the state space, allowing us to transform pMDPs into semantically equivalent non-parametric MDPs. The transformation is applicable to pMDPs with general measurable state and action spaces, that may be both finite and infinite sets. This transformation, that has previously not been explored in the literature, opens an opportunity to bring the techniques for formal verification of non-parametric MDPs to the setting of pMDPs. Our second contribution is the introduction of parametric supermartingale certificates. We develop these certificates by instantiating existing non-parametric supermartingale certificates in the parameter flattened MDP. This yields a new toolkit for reasoning about pMDPs that fundamentally differs from the existing techniques for finite-state pMDP model checking, and provides a general framework for generalizing supermartingale certificates to pMDPs with general measurable state and action spaces. Our third contribution consists of fully automated algorithms for verification and approximate synthesis in polynomial pMDPs, i.e. pMDPs whose state-, action- and parameter-spaces and the stochastic kernel can be expressed in polynomial real arithmetic. Using template-based synthesis and SMT solving, we automatically construct parametric supermartingale certificates for verification. For synthesis, we employ an abstraction–refinement procedure that partitions the parameter space into regions of satisfaction and violation. Alongside, as a witness of the satisfaction of the specification, both our verification and synthesis algorithms produce a parametric strategy in a closed-form expression that explicitly captures the strategy as a symbolic polynomial function of a parameter valuation, which can be instantiated to concrete strategies by substituting in the parameter valuation. To the best of our knowledge, this is the first algorithm that produces such parametric strategies in the literature on pMDPs. Finally, we implement a prototype and evaluate it on infinite-state pMDP benchmarks modeling continuous random walk scenarios. Related work. The verification of stochastic systems has a long and well-established history, encompassing the analysis of Markov chains as well as the synthesis and verification of policies for Markov decision processes (MDPs) and partially observable MDPs (POMDPs). More recently, significant attention has been devoted to stochastic systems with uncertain transition probabilities in finite-state domains. This line of work broadly falls into two categories: models with interval-valued probabilities [19] and models with parametric probability distributions [32]. Parametric models are strictly more expressive, as appropriate choices of parameters can also represent probability intervals. The study of pMDPs over infinite or continuous state spaces remains limited. To the best of our knowledge, the only known approach [39] is restricted to abstraction-based techniques that support bounded-horizon properties, thereby limiting their applicability to long-run or asymptotic behaviors. Independently, supermartingale-based certificates have played a central role in the verification and synthesis of stochastic systems. These techniques apply to general (including infinite and continuous) state spaces and support a broad class of specifications, ranging from safety [40, 45, 18, 46, 52, 47, 1, 48] and reachability [11, 13, 12, 38, 3, 16, 36, 17, 37, 34] to more expressive ω-regular properties [30, 4, 5, 35, 2]. Our work bridges two lines of research by combining supermartingale certificates with parametric stochastic models over infinite state spaces, thereby enabling verification of rich behavioral properties in the presence of parametric uncertainty. 2 Preliminaries We assume that the reader is familiar with basic notions of measure and probability theory such as measurable space, probability measure, or expected value, see [49] for formal definitions of these notions. For a measurable space (X,ℱX)(X,F_X) consisting of a set X and a σ-algebra ℱXF_X over X, we use Δ(X,ℱX) (X,F_X) to denote the set of all probability distributions over (X,ℱX)(X,F_X). For a probability distribution δ∈Δ(X,ℱX)δ∈ (X,F_X), we use support(δ) support(δ) to denote its support. For a set X, we use X∗X^* and XωX^ω to denote the sets of all finite and infinite words over X. MDPs. We now formally define Markov decision processes (MDPs) over general measurable state and action spaces. A (measurable) MDP is a tuple M=(S,ℱS,A,ℱA,P,Init)M=(S,F_S,A,F_A,P, Init), where • (S,ℱS)(S,F_S) is the state space, with S being the set of states and ℱSF_S being a σ-algebra over the set S, with Init⊆S Init S being the set of initial states, • (A,ℱA)(A,F_A) is the action space, with A being the set of actions and ℱAF_A being a σ-algebra over the set A, and • P:S×A×ℱS→[0,1]P:S× A×F_S→[0,1] is the stochastic kernel (or probabilistic transition function), where we require that (1) P(s,a,⋅):ℱS→[0,1]P(s,a,·):F_S→[0,1] is a probability measure for each state-action pair (s,a)∈S×A(s,a)∈ S× A, and (2) P(⋅,⋅,B):S×A→[0,1]P(·,·,B):S× A→[0,1] is a measurable function for each event B∈ℱSB _S. For each state-action pair (s,a)∈S×A(s,a)∈ S× A, we sometimes use the notation P(⋅∣s,a)=P(s,a,⋅):ℱS→[0,1]P(· s,a)=P(s,a,·):F_S→[0,1] to denote the probability distribution over the state space induced by the stochastic kernel at the state-action pair (s,a)(s,a). In the special case when the action set is a singleton, i.e. |A|=1|A|=1 and ℱA=∅,AF_A=\ ,A\, we say that M is a (measurable) Markov chain. A path is an infinite sequence of state-action pairs s0,a0,s1,a1,⋯∈(S×A)ωs_0,a_0,s_1,a_1,…∈(S× A)^ω such that s0∈Inits_0∈ Init and si+1∈support(P(⋅∣si,ai))s_i+1∈ support(P(· s_i,a_i)) for each i∈ℕ0i _0. A finite path s0,a0,s1,a1,…,sis_0,a_0,s_1,a_1,…,s_i is a finite prefix of a path that ends in a state. We use PathM Path^M and FPathM FPath^M to denote the sets of all paths and finite paths in the MDP M. Strategies and semantics of MDPs. Similarly to finite-state MDPs, the semantics of general measurable MDPs are formalized via the notion of strategies [41]. A strategy (also known as a policy or a controller) in an MDP is a measurable map σ:S→Aσ:S→ A which to each state in the MDP assigns an action. We use StrM Str^M to denote the set of all strategies in the MDP M. Note that in this work we restrict our attention to deterministic memoryless strategies, i.e. strategies whose action assignment only depends on the current state and does not use information about the past, and which do not randomize between actions. We discuss the implications of this restriction in Remark 2. The semantics of an MDP are defined as follows. For each initial state s∈Inits∈ Init, an MDP M and a strategy σ together define a probability space over the set of all MDP paths. A random path in this probability space is generated as follows. The initial state of the path is s0=s_0=s. For each i∈ℕ0i _0, let the i-th state of the path be sis_i. The i-th action aia_i of the path is then specified by the strategy via ai=σ(si)a_i=σ(s_i), and the (i+1)(i+1)-st state si+1s_i+1 is sampled from the probability distribution P(⋅∣si,ai)P(· s_i,a_i) specified by the stochastic kernel. The process is executed ad infinitum and gives rise to a random infinite path s0,a0,s1,a1,⋯∈PathMs_0,a_0,s_1,a_1,…∈ Path^M in the MDP. This process is formalized via the cylinder construction [7, Theorem 2.7.2] and it gives rise to a probability space (PathM,ℱPathM,ℙsM,σ)( Path^M,F_ Path^M,P_s^M,σ) over the set of all MDP paths, where ℱPathMF_ Path^M is a σ-algebra over the paths and ℙsM,σP_s^M,σ is a probability measure. We use sM,σE_s^M,σ to denote expectation operator in this probability space. Parametric MDPs (pMDP). We now define pMDPs, which are the central object of study in this work. Intuitively, a pMDP is an MDP whose stochastic kernel is parametrized by finitely many real-valued parameters, and each parameter valuation gives rise to one concrete MDP with the stochastic kernel defined by the parameter valuation. Formally, a parametric MDP (pMDP) is a tuple M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U), where each component is defined analogously as above in the case of MDPs, with two exceptions, namely • U⊆ℝnU ^n is a Borel-measurable set of parameter valuations, where n∈ℕ0n _0 is the number of real-valued parameters, and • P:U×S×A×ℱS→[0,1]P:U× S× A×F_S→[0,1] is the parametric stochastic kernel (or parametric probabilistic transition function), where we require that (1) for each parameter valuation u∈Uu∈ U, P(u,⋅,⋅,⋅):S×A×ℱS→[0,1]P(u,·,·,·):S× A×F_S→[0,1] is a stochastic kernel as defined above, and (2) P(⋅,s,a,B):U→[0,1]P(·,s,a,B):U→[0,1] is a measurable function, where U is equipped with the Borel σ-algebra. Intuitively, each parameter valuation u∈Uu∈ U produces a stochastic kernel P[u]=P(u,⋅,⋅,⋅):S×A×ℱS→[0,1]P[u]=P(u,·,·,·):S× A×F_S→[0,1], which in turn gives rise to a (non-parametric) MDP M[u]=(S,ℱS,A,ℱA,P[u],Init)M[u]=(S,F_S,A,F_A,P[u], Init). Moreover, (non-parametric) MDPs are a special case of pMDPs, where the stochastic kernel P=P[u]P=P[u] for all u∈Uu∈ U. Example 1 (Running example) We define a pMDP M which will serve as our running example throughout this work. The state space (S,ℱS)(S,F_S) of this pMDP is the interval of real values S=[−2,150]S=[-2,150] equipped with the Borel σ-algebra ℱS=ℬ([−2,150])F_S=B([-2,150]), and the action space (A,ℱA)(A,F_A) is the interval of real values A=[0,0.6]A=[0,0.6] equipped with the Borel σ-algebra ℱA=ℬ([0,0.6])F_A=B([0,0.6]). The pMDP contains 22 real-valued parameters and the set of parameter valuations is U=[−1,1]2=(u1,u2)∣−1≤u1,u2≤1U=[-1,1]^2=\(u_1,u_2) -1≤ u_1,u_2≤ 1\. Finally, the parametric stochastic kernel is defined by the equation s′≔s+a+u1+u2⋅Uniform[−0.75,0.25],if 0≤s≤100,s,otherwise,s casess+a+u_1+u_2· Uniform[-0.75,0.25],&if 0≤ s≤ 100,\\ s,&otherwise, cases (1) where Uniform[−0.75,0.25] Uniform[-0.75,0.25] denotes the uniform distribution over the real interval [−0.75,0.25][-0.75,0.25]. In other words, for each parameter valuation (u1,u2)∈U(u_1,u_2)∈ U, state s∈Ss∈ S and action a∈Aa∈ A, the probability distribution P(⋅∣u,s,a)P(· u,s,a) induced by the parametric stochastic kernel is defined as in eq. (1). Finally, the set of initial states is the interval of real values Init=[2,3] Init=[2,3]. Parametric strategies and semantics of pMDPs. The semantics of pMDPs are formalized via the notion of parametric strategies. Intuitively, a parametric strategy in a pMDP is an object which, for each parameter valuation, gives rise to one concrete map that to each state assigns an action. Formally, a parametric strategy in a pMDP M is a measurable map σ:U×S→Aσ:U× S→ A such that, for each parameter valuation u∈Uu∈ U, the map σ[u]=σ(u,⋅):S→Aσ[u]=σ(u,·):S→ A is a strategy in the MDP M[u]M[u]. We use StrM Str^M to denote the set of all parametric strategies in M. For each parameter valuation u∈Uu∈ U, the MDP M[u]M[u], initial state s∈Inits∈ Init and parametric strategy σ[u]σ[u] together gives rise to a probability space (PathM[u],ℱPathM[u],ℙsM[u],σ[u])( Path^M[u],F_ Path^M[u],P_s^M[u],σ[u]) defined analogously as above. We use sM[u],σ[u]E_s^M[u],σ[u] to denote the expectation operator in this probability space. Specifications. A specification ϕφ in a pMDP M is a set of paths ϕφ in PathM Path^M. For the semantics of our problem to be well-defined, we require that this set of paths belongs to the σ-algebra induced by the pMDP semantics, i.e. that ϕ∈ℱPathM[u]φ _ Path^M[u] for every u∈Uu∈ U. We say that a path ρ∈PathMρ∈ Path^M satisfies the specification ϕφ, if ρ∈ϕρ∈φ. For each parameter valuation u∈Uu∈ U, initial state s∈Inits∈ Init, and parametric strategy σ, we write ℙsM[u],σ[u][ϕ]P_s^M[u],σ[u][φ] to denote the probability that a path in M sampled from the underlying probability space satisfies ϕφ. We use ¬ϕ=PathM\ϕ φ= Path^M φ to denote the specification which is satisfied by all paths that do not satisfy ϕφ and vice versa. Our examples will mostly focus on reachability and safety specifications. Let X∈ℱSX _S be a measurable set of MDP states. We define the reachability specification with respect to the set X via Reach(X)=s0,a0,s1,a1,⋯∈PathM∣∃i∈ℕ0.si∈X Reach(X)=\s_0,a_0,s_1,a_1,…∈ Path^M ∃ i _0.\,s_i∈ X\, and the safety specification with respect to the set X via Safe(X)=s0,a0,s1,a1,⋯∈PathM∣∀i∈ℕ0.si∈X Safe(X)=\s_0,a_0,s_1,a_1,…∈ Path^M ∀ i _0.\,s_i∈ X\. 3 Problem Statement We now define the parameter verification and synthesis problems that we consider in this work. In what follows, suppose that M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) is a pMDP with U⊆ℝnU ^n being the set of parameter valuations, and let ϕφ be a specification in M. Following the terminology in [33], we say that a parameter region is a Borel-measurable subset R⊆UR U of parameter valuations. We use MR=(S,ℱS,A,ℱA,P,Init,R)M^R=(S,F_S,A,F_A,P, Init,R) to denote the pMDP identical to M but whose set of parameter valuations is restricted to R. Specifications in pMDPs. Section 2 formalizes specifications and the notion of paths satisfying specifications. However, a pMDP gives rise to a probability space over the set of all paths for each parameter valuation. Hence, when reasoning about specification satisfaction in pMDPs, we are interested in deriving lower (and, dually, upper) bounds on the probability of a random path in this probability space satisfying the specification. Formally, we distinguish between angelic and demonic satisfaction of the specification, depending on whether the specification needs to be satisfied for some or for all parametric strategies in the pMDP. Our definitions generalize the definitions of [33] from the setting of finite-state pMDPs to the setting of general measurable pMDPs: 1. Angelic satisfaction. We say that the pMDP M angelically satisfies specification ϕφ with probability at least p∈[0,1]p∈[0,1], denoted M⊧aϕ,pM _aφ,p, if there exists a parametric strategy σ:U×S→Aσ:U× S→ A that leads to specification satisfaction for all parameter valuations, i.e. ∃σ∈StrM.∀u∈U.∀s∈Init.ℙsM[u],σ[u][ϕ]≥p.∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ Init.\,\,\,P_s^M[u],σ[u][φ]≥ p. (2) 2. Demonic satisfaction. We say that the pMDP M demonically satisfies specification ϕφ with probability at least p∈[0,1]p∈[0,1], denoted M⊧dϕ,pM _dφ,p, if all parametric strategies σ:U×S→Aσ:U× S→ A lead to specification satisfaction for all parameter valuations, i.e. ∀σ∈StrM.∀u∈U.∀s∈Init.ℙsM[u],σ[u][ϕ]≥p.∀σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ Init.\,\,\,P_s^M[u],σ[u][φ]≥ p. (3) In both cases, quantification is over parametric strategies of type σ:U×S→Aσ:U× S→ A, which for each parameter valuation induce one regular, non-parametric strategy. Problems. We consider the following problems, as discussed in Section 1: 1. Verification problem. Given a pMDP M with a set of parameter valuations U, a specifciation ϕφ, a probability threshold p∈[0,1]p∈[0,1], and a type of specification satisfaction ♡∈a,d ∈\a,d\, prove that M⊧♡ϕ,pM _ φ,p. 2. Synthesis problem. Given a pMDP M with a set of parameter valuations U, a specifciation ϕφ, a probability threshold p∈[0,1]p∈[0,1], and a type of specification satisfaction ♡∈a,d ∈\a,d\, partition the parameter set U into two regions R and U R such that MR⊧♡ϕ,pM^R _ φ,p and MU ⊧¬♣ϕ,1−pM^U R _ φ,1-p, where ♣ is the opposite symbol of ♡ in a,d\a,d\. 3. Approximate synthesis problem. Given a pMDP M with a set of parameter valuations U, a specifciation ϕφ, a probability threshold p∈[0,1]p∈[0,1], a type of specification satisfaction ♡∈a,d ∈\a,d\, and an approximation parameter c∈[0,1]c∈[0,1], partition the parameter set U into two disjoint regions R and R′R such that MR⊧♡ϕ,pM^R _ φ,p and MR′⊧¬♣ϕ,1−pM^R _ φ,1-p, where ♣ is the opposite symbol of ♡ in a,d\a,d\, and such that (μ(R)+μ(R′))/μ(U)≥1−c(μ(R)+μ(R ))/μ(U)≥ 1-c where μ is the Lebesgue measure over the parameter space. Example 2 Consider the pMDP M with parameter valuations U=[−1,1]2U=[-1,1]^2 as in Example 1. Let ϕ=Reach([90,150])φ= Reach([90,150]), i.e. a reachability specification for the target set T=[90,150]T=[90,150], and let p=0.9p=0.9. For the sake of the example, suppose that we are interested in angelic satisfaction, i.e. ♡=a =a. Given a parameter region R⊆UR U, the verification problem is concerned with proving that there exists a parametric strategy s.t., for each (u1,u2)∈R(u_1,u_2)∈ R and initial state s∈[2,3]s∈[2,3], Reach([90,150]) Reach([90,150]) is satisfied with probability at least 0.90.9. On the other hand, the (approximate) synthesis problem is concerned with partitioning U into two parameter regions R and R′R such that (1) there exists a parametric strategy s.t., for each (u1,u2)∈R(u_1,u_2)∈ R and initial state s∈[2,3]s∈[2,3], Reach([90,150]) Reach([90,150]) is satisfied with probability at least 0.90.9, while (2) for all parametric strategies, for each (u1,u2)∈R(u_1,u_2)∈ R and initial state s∈[2,3]s∈[2,3], ¬Reach([90,150])=Safe([−2,90)) Reach([90,150])= Safe([-2,90)) is satisfied with probability at least 1−0.9=0.11-0.9=0.1. Thus, for parameter valuations in R we require satisfaction of an angelic reachability specification with probability at least 0.90.9, while for parameter valuations in R′R we require satisfaction of a demonic safety specification with probability at least 0.10.1. Remark 1 (Consistency with finite-state pMDP definitions) It may seem that our definitions of angelic and demonic satisfaction in eq. (2) and (3) syntactically deviate from those presented in [33] for finite-state pMDPs, which require: [angelic:] ∀u∈U.∃σ[u]∈StrM[u].∀s∈Init.ℙsM[u],σ[u][ϕ]≥p, ∀ u∈ U.\,\,\,∃σ[u]∈ Str^M[u].\,\,\,∀ s∈ Init.\,\,\,P_s^M[u],σ[u][φ]≥ p, (4) [demonic:] ∀u∈U.∀σ[u]∈StrM[u].∀s∈Init.ℙsM[u],σ[u][ϕ]≥p. ∀ u∈ U.\,\,\,∀σ[u]∈ Str^M[u].\,\,\,∀ s∈ Init.\,\,\,P_s^M[u],σ[u][φ]≥ p. (5) In reality, our definitions in eq. (2) and (3) generalize these definitions to the setting of general measurable pMDPs, such that they are mathematically well-defined and satisfy all measurability requirements, while remaining equivalent to the definitions of [33] for finite-state pMDPs. This is because our definitions in eq. (2) and (3) consider existential and universal quantifications over parametric strategies, but we still require that for each u∈Uu∈ U there exists σ[u]σ[u] for angelic satisfaction, and that for each u∈Uu∈ U demonic satisfaction holds for all σ[u]∈Uσ[u]∈ U. On the other hand, the existential and universal quantification over parametric strategies is necessary to ensure that the resulting strategies are measurable (note that this is a condition in our definition of parametric strategies), while the conditions in eq. (4) and (5) do not guarantee that the induced parametric strategies are measurable. Eq. (4) guarantees the existence of a strategy σ[u]σ[u] in M[u]M[u] for each parameter valuation u∈Uu∈ U, the parametric strategy σ in the pMDP defined via σ(u,s):=σ[u](s)σ(u,s):=σ[u](s) for every u∈Uu∈ U and s∈Ss∈ S may not give rise to a measurable function. However, in the setting of finite-state pMDPs, the two definitions coincide since we consider the discrete topology over the finite state and action spaces, so each parametric strategy σ in M gives rise to one strategy σ[u]σ[u] in M[u]M[u] for every parameter valuation u∈Uu∈ U and vice versa. Remark 2 (Restriction to deterministic memoryless strategies) As stated in Section 2, we restrict our attention to deterministic memoryless strategies. The question of whether deterministic memoryless strategies are sufficient to satisfy a specification, both in MDPs and pMDPs, depends on the specification of interest. For instance, it is known that whenever there exists a strategy in an MDP satisfying a reachability specification, then there exists a memoryless deterministic strategy satisfying the specification. However, this statement does not hold for general omega-regular specifications in MDPs. In Proposition 1, we show that our parameter flattening transformation is semantics preserving, which implies that deterministic memoryless parametric strategies are sufficient in pMDPs whenever deterministic memoryless strategies are sufficient in non-parametric MDPs. 4 Parameter Flattening The heart of our approach is parameter flattening, which is a novel transformation of pMDPs into their semantically equivalent non-parametric counterparts. This transformation allows us to take any existing verification or synthesis tool for non-parametric MDPs, and use it for solving the analogous problem for pMDPs. In our work, we will use supermartingale certificates built for non-parametric MDPs to design parametric supermartingale certificates for pMDPs; this will be shown in Section 5 and 6. Given a pMDP M, the parameter flattening transformation gives rise to a non-parametric MDP M~ M, which we call the parameter flattened MDP of M. Intuitively, the parameter flattened MDP M~ M is obtained by incorporating parameter valuations into the state space of the original pMDP M. Hence, each state in the parameter flattened MDP is a pair of a state and a parameter valuation in the original pMDP. On the other hand, the stochastic kernel of the parameter flattened MDP for each state-parameter valuation pair and for each action samples the successor state according to the stochastic kernel of the original pMDP M, while keeping the parameter valuation unchanged. The following definition formalizes this informal construction. Definition 1 (Parameter flattening) Let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a pMDP. A parameter flattened MDP of M is the non-parametric MDP M~=(S~,ℱS~,A~,ℱA~,P~,Init~) M=( S, F_S, A, F_A, P, Init) whose each component is defined as follows: • S~=S×U S=S× U and ℱS~=ℱS×ℬ(U) F_S=F_S×B(U) where ℬ(U)B(U) is the Borel σ-algebra over U, i.e. the state space of the parameter flattened MDP is the product of the state space and the parameter space of the original pMDP. • A~=A A=A and ℱA~=ℱA F_A=F_A, i.e. the action space of the parameter flattened MDP coincides with the action space of the original pMDP. • P~:S~×A~×ℱS~→[0,1] P: S× A× F_S→[0,1] is defined as follows: For all (s,u)∈S~=S×U(s,u)∈ S=S× U, a∈A~=Aa∈ A=A and (B,X)∈ℱS~=ℱS×ℬ(U)(B,X)∈ F_S=F_S×B(U), we set P~((s,u),a,(B,X))=P(u,s,a,B) P((s,u),a,(B,X))=P(u,s,a,B) if u∈Xu∈ X and P~((s,u),a,(B,X))=0 P((s,u),a,(B,X))=0 if u∉Xu ∈ X. That is, the stochastic kernel of the parameter flattened MDP induces the same probability distribution over the successor state as the original stochastic kernel while keeping the parameter value u unchanged (so u′=u =u). • Init~=Init×U Init= Init× U, i.e. the set of the initial states in the parameter flattened MDP is the product of the set of initial states and the set of parameter valuations of the original pMDP. Example 3 Consider the pMDP M in Example 1. The parameter flattened MDP M~ M of M is defined as follows. The state space is S~=[−2,150]×[−1,1]2 S=[-2,150]×[-1,1]^2, i.e. the product of the state space and parameter valuations in M, with the Borel σ-algebra ℱS~=ℬ([−2,150])×ℬ([−1,1]2)=ℬ([−2,150]×[−1,1]2) F_S=B([-2,150])×B([-1,1]^2)=B([-2,150]×[-1,1]^2). The action space is the same as in M, i.e. A~=[0,0.6] A=[0,0.6] and ℱA~=ℬ([0,0.6]) F_A=B([0,0.6]). For each state (s,u1,u2)∈S~=[−2,150]×[−1,1]2(s,u_1,u_2)∈ S=[-2,150]×[-1,1]^2 and for each action a∈A~=[0,0.6]a∈ A=[0,0.6], the probability distribution P~(⋅∣(s,u1,u2),a) P(· (s,u_1,u_2),a) induced by the stochastic kernel is again defined by eq. (1). Finally, the initial set is Init~=[2,3]×[−1,1]2 Init=[2,3]×[-1,1]^2. Every path s0,a0,s1,a1,…s_0,a_0,s_1,a_1,… and parameter valuation u∈Uu∈ U in M together induce a path (s0,u),a0,(s1,u),a1,…(s_0,u),a_0,(s_1,u),a_1,… in the parameter flattened MDP M~ M. Hence, a specification ϕφ in M induces a parameter flattened specification ϕ~ φ in the parameter flattened MDP M~ M defined via ϕ~=(s0,u),a0,(s1,u),a1,⋯∈PathM~∣s0,a0,s1,a1,⋯∈ϕ∧u∈U φ=\(s_0,u),a_0,(s_1,u),a_1,…∈ Path M s_0,a_0,s_1,a_1,…∈φ u∈ U\. On the other hand, every parametric strategy σ:U×S→Aσ:U× S→ A in the pMDP M induces a parameter flattened strategy σ~:S~→A~ σ: S→ A via σ~(s,u)=σ[u](s) σ(s,u)=σ[u](s) for all (s,u)∈S~=S×U(s,u)∈ S=S× U. The following proposition establishes the semantic equivalence between pMDPs and their parameter flattened MDPs. The proof is in Appendix 0.A. Proposition 1 (Parameter flattening is semantic preserving) Let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a pMDP, σ:U×S→Aσ:U× S→ A be a parametric strategy in M, and ϕφ be a specification in M. Let M~=(S~,ℱS~,A~,ℱA~,P~,Init~) M=( S, F_S, A, F_A, P, Init), σ~:S~→A~ σ: S→ A and ϕ~ φ be the parameter flattened MDP of M, the parameter flattened strategy of σ and the parameter flattened specification of ϕφ, respectively. Then, for each initial state s∈Inits∈ Init and each parameter valuation u∈Uu∈ U in the pMDP M, ℙsM[u],σ[u][ϕ]=ℙ(s,u)M~,σ~[ϕ~].P_s^M[u],σ[u][φ]=P_(s,u) M, σ[ φ]. The following theorem is then a corollary of the above proposition and of our definitions of angelic and demonic satisfaction of specifications in parametric and non-parametric MDPs. We defer the proof to Appendix 0.B. Theorem 4.1 (Soundness and completeness) Let M be a pMDP, M~ M be the parameter flattened MDP of M, ϕφ be a specification in ϕφ, p∈[0,1]p∈[0,1] be a probability threshold, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. Then, we have M⊧♡ϕ,pM _ φ,p if and only if M~⊧♡ϕ~,p M _ φ,p. Hence, in order to prove specification satisfaction in a pMDP, it suffices to prove satisfaction in the parameter flattened MDP. This motivates our construction of parametric supermartingale certificates as instantiations of supermartingale certificates in the state space of parameter flattened MDPs. 5 Parametric Supermartingale Certificates We now present our novel parametric supermartingale certificates for proving satisfaction of specifications in pMDPs. Our parametric supermartingale certificates generalize the existing supermartingale certificates for non-parametric MDPs by incorporating the parameters within the definitions of the certificates. This is done in such a way that the new parametric certificates can be computed by instantiating non-parametric supermartingale certificates in the state space of the parameter flattened MDP. While this leads to an elegant framework for generalizing most existing supermartingale certificates to the setting of pMDPs, it is technically non-trivial and requires care in appropriately handling the quantification of parameter valuations and distinguishing between angelic and demonic satisfaction of specifications in pMDPs. To the best of our knowledge, this is the first work that uses supermartingale certificates to reason about pMDPs. This section is organized as follows. We illustrate the definition of parametric supermartingale certificates via instantiation in the state space of the parameter flattened MDP on two classes of commonly used supermartingale certificates which will also be used in our experimental evaluation. Specifically, we present pMDP generalizations of stochastic barrier functions for probability p∈[0,1)p∈[0,1) safety [40] (Section 5.1) and of reach-avoid supermartingales for probability p∈[0,1)p∈[0,1) reachability [53] (Section 5.2). In Appendix 0.E, we show a pMDP generalization of another established supermartingale certificate, namely ranking supermartingales (RSMs) for probability 1 reachability [11]. While we use these established supermartingale certificates to illustrate our construction of parametric supermartingale certificates, we stress that our construction applies to other supermartingale certificates as well, allowing us to generalize a broad class of supermartingale certificates to the setting of pMDPs. These include the recent certificates for general ω-regular specifications in non-parametric MDPs [4, 30, 5]. Appendix 0.F formalizes the class of supermartingale certificates that can be generalized for pMDPs in the same manner. Invariants. Supermartingale certificates are functions that map MDP states to real values that are required to satisfy a set of conditions at every reachable MDP state. Since computing the set of reachable states in a general measurable MDP is computationally intractable, we define supermartingale certificates with respect to an over-approximation of the set of all reachable states which is called a (supporting) invariant. Formally, a state in an MDP is said to be reachable if it is contained in some MDP path. An invariant in an MDP is a measurable set I of MDP states that contains all reachable states in the MDP. We note that, while in this section we assume the existence of a supporting invariant, our verification and synthesis algorithms in Section 6 will compute the invariant together with the parametric supermartingale certificate. 5.1 Parametric Supermartingales for Safety Specifications For proving probability p∈[0,1)p∈[0,1) (a.k.a. quantitative) safety specifications, stochastic barrier functions (SBFs) are an established supermartingale certificate [40]. We present their generalization to the setting of pMDPs by instantiating them in the state space of parameter flattened MDPs. We first recall (non-parametric) SBFs. Intuitively, given a Markov chain M, a set of safe states X that we want to prove the system always remains in with probability at least p, and an invariant I that over-approximates the set of reachable states, an SBF is a measurable function V:S→ℝV:S that to each state assigns a real value that is required to satisfy the following four conditions: (C1) V is nonnegative at all states in the invariant I, (C2) V(s)≤1V(s)≤ 1 at all initial states s in the MDP, (C3) V(s)≥11−pV(s)≥ 11-p at all invariant states s outside of the safe set X, and (C4) at all invariant states s at which V(s)≤11−pV(s)≤ 11-p, the value of V (non-strictly) decrease in expected value upon the one-step execution of the Markov chain. Thus, the value of the SBF is required to be nonnegative, initially be below 11 and to decrease in expectation, while the safety specification can be violated only if the value of the SBF exceeds 11−p 11-p despite the expected decrease. It was shown in [40] that these conditions together ensure that the safety specification is satisfied with probability at least p. The following definition formalizes the above intuition and generalizes it to the setting of pMDPs by instantiating it in the state space of parameter flattened MDP. In doing so, however, we need to exercise additional care to properly quantify parameter valuations, and to achieve the extension from Markov chains to MDPs by differentiating between angelic and demonic satisfaction. Note that, since parametric SBFs are defined over the state space of parameter flattened MDP, they are defined as measurable functions of type V:S×U→ℝV:S× U that map states of the parameter flattened MDP to real values. Definition 2 (Parametric SBFs) Let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a pMDP, I∈ℱSI _S be an invariant, X∈ℱSX _S be a set of safe states, p∈[0,1)p∈[0,1) be a probability threshold, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. A parametric stochastic barrier function (parametric SBF) for X with respect to I and ♡ is a measurable function V:S×U→ℝV:S× U , which is required to satisfy the following four conditions: 1. Nonnegativity. V(s,u)≥0V(s,u)≥ 0 for all s∈Is∈ I and u∈Uu∈ U. 2. Initial. V(s,u)≤1V(s,u)≤ 1 for all s∈Inits∈ Init and u∈Uu∈ U. 3. Safety. V(s,u)≥11−pV(s,u)≥ 11-p for all s∈I ∈ I X and u∈Uu∈ U. 4. Expected decrease. We distinguish between angelic and demonic satisfaction: (a) Angelic satisfaction, i.e. ♡=a =a. There exists a parametric strategy σ:U×S→Aσ:U× S→ A in M such that, for every parameter valuation u∈Uu∈ U and for every state s∈Is∈ I with V(s,u)≤1/(1−p)V(s,u)≤ 1/(1-p), V satisfies expected decrease for the action a=σ[u](s)a=σ[u](s), i.e. ∃σ∈StrM.∀u∈U.∀s∈I.V(s,u)≤11−p⇒V(s,u)≥s′∼P(⋅∣u,s,σ[u](s))[V(s′,u)]. split∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ I.\,\,\,&V(s,u)≤ 11-p\\ & V(s,u) _s P(· u,s,σ[u](s))[V(s ,u)]. split (b) Demonic satisfaction, i.e. ♡=d =d. For every parametric strategy σ:U×S→Aσ:U× S→ A in M and for every parameter valuation u∈Uu∈ U and state s∈Is∈ I with V(s,u)≤1/(1−p)V(s,u)≤ 1/(1-p), we have that V satisfies expected decrease, i.e. ∀σ∈StrM.∀u∈U.∀s∈I.V(s,u)≤11−p⇒V(s,u)≥s′∼P(⋅∣u,s,σ[u](s))[V(s′,u)]. split∀σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ I.\,\,\,&V(s,u)≤ 11-p\\ & V(s,u) _s P(· u,s,σ[u](s))[V(s ,u)]. split The following theorem shows that parametric SBFs provide a sound proof rule for proving probability p∈[0,1)p∈[0,1) safety in pMDPs. The proof proceeds by showing that the parametric SBF induces a non-parametric SBF in the parameter flattened MDP and then using the soundness of SBFs for proving probability p∈[0,1)p∈[0,1) safety [40], while taking additional care to correctly handle the cases of angelic and demonic satisfaction. We defer it to Appendix 0.C. Theorem 5.1 (Soundness of parametric SBFs) Let M be a pMDP, I be an invariant, X be a set of safe states, p∈[0,1)p∈[0,1), and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. Suppose that there exists a parametric SBF for V with respect to I and ♡ . Then, we have M⊧♡Safe(X),pM _ Safe(X),p. Example 4 Consider the pMDP M in Example 1 with the demonic safety specification ϕ=Safe([−2,90])φ= Safe([-2,90]), ♡=d =d, and probability threshold p=0.1p=0.1 as in Example 2. Let R=[−0.25,−0.125]×1R=[-0.25,-0.125]×\1\ be a parameter region for which we want to prove that MR⊧dSafe([−2,90]),0.1M^R _d Safe([-2,90]),0.1. An example of a parametric SBF and a supporting invariant computed by our prototype tool, which can be used to prove this statement, are given by V(s,u1,u2)=−2⋅10−5−u1+0.011⋅sV(s,u_1,u_2)=-2· 10^-5-u_1+0.011· s and I=[−2,150]I=[-2,150], i.e the invariant is equal to the whole set of states. One can verify by inspection that V satisfies all the defining conditions in Definition 2. Hence, by Theorem 5.1, it provides a proof that MR⊧dSafe([−2,90]),0.1M^R _d Safe([-2,90]),0.1. Remark 3 (Probability 11 safety) Our parametric SBFs are defined and proved to be sound for p∈[0,1)p∈[0,1) safety. However, for p=1p=1, parametric SBFs become ill defined due to the quotient 11−p 11-p in their defining conditions. This issue already arises in the non-parametric setting, and is not an artifact of pMDPs. The more conceptual issues regarding the unsoundness of SBFs when p=1p=1 are discussed in [44]. In practice, to achieve soundness for p=1p=1, one can strengthen almost-sure safety to sure safety and use classical (non-probabilistic) barrier functions. Their instantiation in the setting of pMDPs is achieved similarly to parametric SBFs in Definition 2, by considering the parameter flattened MDP. 5.2 Parametric Supermartingales for Reachability Specifications We now present a parametric spermartingale certificate generalization of reach-avoid supermartingales (RASMs) for proving probability p∈[0,1)p∈[0,1) (a.k.a. quantitative) reachability and reach-avoidance specifications [53]. Here we consider reachability since our focus in the experiments will be on reachability specifications, however an extansion to reach-avoid specifications can be achieved by including an additional safety condition analogous to condiiton 33 in Definition 2. We first recall (non-parametric) RASMs. Intuitively, given a Markov chain M, a set of target states T that we want to prove the system reaches with probability at least p, and an invariant I, a RASM is a measurable function V:S→ℝV:S that to each state assigns a real value that is required to satisfy the following four conditions: (C1) V is nonnegative at all states in the invariant I, (C2) V(s)≤1V(s)≤ 1 at all initial states s in the MDP, and (C3) at all non-target invariant states s∈I ∈ I T at which V(s)≤11−pV(s)≤ 11-p, the value of V strictly decrease by at least ϵ>0ε>0 in expected value upon the one-step execution of the Markov chain. Thus, the value of the SBF is required to be nonnegative, initially be below 11 and to strictly ϵε-decrease in expectation until it either reaches the target set or a state with V(s)≥11−pV(s)≥ 11-p. It was shown in [53] that these conditions together ensure that the reachability specification is satisfied with probability at least p. The following definition formalizes the above intuition and generalizes it to the setting of pMDPs by instantiating it in the state space of parameter flattened MDP. Since parametric RASMs are defined over the state space of parameter flattened MDP, they are defined as measurable functions of type V:S×U→ℝV:S× U that map states of the parameter flattened MDP to real values. Definition 3 (Parametric RASMs) Let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a pMDP, I∈ℱSI _S be an invariant, T∈ℱST _S be a set of target states, p∈[0,1)p∈[0,1) be a probability threshold, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. A parametric reach-avoid supermartingale (parametric RASM) for T with respect to I and ♡ is a measurable function V:S×U→ℝV:S× U , which is required to satisfy the following four conditions: 1. Nonnegativity. V(s,u)≥0V(s,u)≥ 0 for all s∈Is∈ I and u∈Uu∈ U. 2. Initial. V(s,u)≤1V(s,u)≤ 1 for all s∈Inits∈ Init and u∈Uu∈ U. 3. Expected decrease. We distinguish between angelic and demonic satisfaction: (a) Angelic satisfaction, i.e. ♡=a =a. There exist ϵ>0ε>0 and a parametric strategy σ:U×S→Aσ:U× S→ A in M such that, for every parameter valuation u∈Uu∈ U and for every non-target state s∈I ∈ I T with V(s,u)≤1/(1−p)V(s,u)≤ 1/(1-p), V satisfies expected decrease for the action a=σ[u](s)a=σ[u](s), i.e. ∃σ∈StrM.∀u∈U.∀s∈I.s∈I ∧V(s,u)≤11−p⇒V(s,u)≥s′∼P(⋅∣u,s,σ[u](s))[V(s′,u)]+ϵ. split∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,&∀ s∈ I.\,\,\,s∈ I T V(s,u)≤ 11-p\\ & V(s,u) _s P(· u,s,σ[u](s))[V(s ,u)]+ε. split (b) Demonic satisfaction, i.e. ♡=d =d. There exists ϵ>0ε>0 such that for all parametric strategies σ:U×S→Aσ:U× S→ A in M, for every parameter valuation u∈Uu∈ U and for every non-target state s∈I ∈ I T with V(s,u)≤1/(1−p)V(s,u)≤ 1/(1-p), V satisfies expected decrease for the action a=σ[u](s)a=σ[u](s), i.e. ∀σ∈StrM.∀u∈U.∀s∈I.s∈I ∧V(s,u)≤11−p⇒V(s,u)≥s′∼P(⋅∣u,s,σ[u](s))[V(s′,u)]+ϵ. split∀σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,&∀ s∈ I.\,\,\,s∈ I T V(s,u)≤ 11-p\\ & V(s,u) _s P(· u,s,σ[u](s))[V(s ,u)]+ε. split The following theorem shows that parametric RASMs provide a sound proof rule for probability p∈[0,1)p∈[0,1) reachability in pMDPs; the proof is in Appendix 0.D. Theorem 5.2 (Soundness of parametric RASMs) Let M be a pMDP, I be an invariant, T be a set of target states, p∈[0,1)p∈[0,1) be a probability threshold, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. Suppose that there exists a parametric RASM for T with respect to I and ♡ . Then, M⊧♡Reach(T),pM _ Reach(T),p. Example 5 Consider the pMDP M in Example 1 with the angelic reachability specification ϕ=Reach([90,150])φ= Reach([90,150]), ♡=a =a, and probability threshold p=0.9p=0.9 as in Example 2. Let R=[0.25,0.5]×1R=[0.25,0.5]×\1\ be a parameter region for which we want to prove that MR⊧aReach([90,150]),0.9M^R _a Reach([90,150]),0.9. An example of a parametric RASM and a supporting invariant computed by our prototype tool, which can be used to prove this statement, are given by V(s,u1,u2)=0.5⋅u1−3.5⋅10−14⋅sV(s,u_1,u_2)=0.5· u_1-3.5· 10^-14· s and I=s∈[−2,150]∣−9.875+98.752⋅s≥0I=\s∈[-2,150] -9.875+98.752· s≥ 0\. One can verify by inspection that V satisfies all the defining conditions in Definition 3. An existentially quantified parametric strategy, which is also computed by our tool, is defined via σ(s,u1,u2)=0.6σ(s,u_1,u_2)=0.6. Hence, by Theorem 5.2, it provides a proof that MR⊧aReach([90,150]),0.9M^R _a Reach([90,150]),0.9. 6 Automated Parameter Verification and Synthesis We now present our algorithms for solving the verification and approximate synthesis problems defined in Section 3. We first present our algorithm for the verification problem, which will then be used as a subroutine for the synthesis algorithm. As a byproduct, our algorithms also produce a closed form expression for a parametric strategy that witnesses specification satisfaction. To the best of our knowledge, this is novel with respect to the existing literature both on finite- and infinite-state pMDPs: existing works considered the question of the existence of concrete strategies in the verification and synthesis problems [33], but how to obtain these strategies in a succinct form was open. Our algorithms are applicable to polynomial pMDPs and parametric supermartingale certificates, which we formalize below. In what follows, let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a pMDP with U⊆ℝnU ^n, ϕφ a specification, p∈[0,1]p∈[0,1], and ♡∈a,d ∈\a,d\ a type of specification satisfaction. 6.1 Verification Algorithm The goal of the verification problem is to formally prove that M⊧♡ϕ,pM _ φ,p. Our verification algorithm proceeds by synthesizing a parametric supermartingale certificate V with a supporting invariant I which provides a sound proof rule for proving this statement. We aim for a unifying verification algorithm that can be used to synthesize a broad class of parametric supermartingale certificates. Thus, we first formalize the class of parametric supermartingale certificates that can be synthesized by our verification algorithm. Supported parametric supermartingale certificates. Our verification algorithm can synthesize parametric generalizations of any supermartingale certificate whose defining conditions are all either bound conditions or expectation conditions. For a measurable function V:S×U→ℝV:S× U , we define these as follows: 1. Bound condition. Consider a measurable set of states X∈ℱSX _S and a Borel-measurable set of real values Y⊆ℝY . We define the (X,Y)(X,Y)-bound condition to be the logical formula which encodes that, for all invariant states in the set X, the value of V must lie in the set Y, i.e. ∀u∈U.∀s∈I.s∈X⇒V(s,u)∈Y.∀ u∈ U.\,\,\,∀ s∈ I.\,\,\,s∈ X V(s,u)∈ Y. 2. Expectation condition. Consider a measurable set of states X∈ℱSX _S and two Borel-measurable set of real values Y,Z⊆ℝY,Z . We define the (X,Y,Z)(X,Y,Z)-expectation condition to be the logical formula which encodes that, for all invariant states in the set X at which the value of V lies in the set Y, the difference between the value of V and the expected value of V upon the one-step execution of the Markov chain must lie in the set Z, i.e. ∃σ∈StrM.∀u∈U.∀s∈I.s∈X∧V(s,u)∈Y⇒V(s,u)−s′∼P(⋅∣u,s,σ[u](s))[V(s′)]∈Z, split∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ I.\,\,\,&s∈ X V(s,u)∈ Y\\ & V(s,u)-E_s P(· u,s,σ[u](s))[V(s )]∈ Z, split for angelic satisfaction, whereas for demonic satisfaction the existential quantification ∃σ∈StrM∃σ∈ Str^M changes to the universal quantification ∀σ∈StrM∀σ∈ Str^M. Observe that the defining conditions both parametric SBFs and parametric RASMs are either bound conditions (all but the expectation decrease condition) or expectation conditions (the expectation decrease condition). This remains true for parametric generalizations of most other existing supermartingale certificates, as we discuss in Appendix 0.F. This includes Streett supermartingales [4, 5] and limit-deterministic Büchi supermartingales [30] for general ω-regular specifications. Hence, in what follows, we present a unifying algorithmic framework for computing any parametric supermartingale certificate whose defining conditions are either bound conditions or expectation conditions. Assumptions. Our algorithm is restricted to pMDPs and parametric supermartingale certificates represented in polynomial real arithmetic: 1. We assume that the pMDP M is polynomial, meaning that: • The sets of parameter valuations U⊆ℝnU ^n, states S⊆ℝnSS ^n_S and actions A⊆ℝnAA ^n_A are all subsets of finite-dimensional Euclidean spaces, represented as satisfiability sets of boolean combinations of finitely many polynomial inequalities over parameter variables u1,…,unu_1,…,u_n (for U), state variables s1,…,snSs_1,…,s_n_S (for S), and action variables a1,…,anAa_1,…,a_n_A (for A). • The parametric stochastic kernel P can be represented in polynomial real arithmetic, that is, the probability distribution P(⋅∣u,s,a)P(· u,s,a) induced by the stochastic kernel can be represented via a polynomial equation s′=P(u1,…,un,s1,…,snS,a1,…,anA,r1,…,rnr)s =P(u_1,…,u_n,s_1,…,s_n_S,a_1,…,a_n_A,r_1,…,r_n_r), where r1,…,rnrr_1,…,r_n_r are random variables sampled from given probability distributions that are assumed to be independent. We allow sampling from arbitrary discrete or continuous probability distributions. However, we assume that the first D moments of distributions are known and available, where D is the algorithm’s polynomial degree parameter. 2. We assume that the defining conditions of the parametric supermartingale certificate can be represented in polynomial real arithmetic. In particular, for each bound condition, we assume that X and Y can be represented as a satisfiability set of a boolean combination of finitely many polynomial inequalities over state variables s1,…,snSs_1,…,s_n_S and parameters u1,…,unu_1,…,u_n. For each expectation condition, we assume that X, Y and Z can be represented as a satisfiability set of a boolean combination of finitely many polynomial inequalities over state variables s1,…,snSs_1,…,s_n_S and parameters u1,…,unu_1,…,u_n. Note that these assumptions are clearly satisfied by parametric SBFs and RASMs. Algorithm outline. Our verification algorithm follows a template-based synthesis approach and reduces the computation of the parametric supermartingale certificate V and the invariant I to solving a system of polynomial real constraints. This is a standard procedure for synthesizing (non-parametric) supermartingale certificates, see e.g. [12, 16, 5, 30], hence we keep the exposition brief. In outline, the algorithm proceeds in three steps. In Step 1, the algorithm fixes a symbolic polynomial template for the parametric supermartingale certificate V:S×U→ℝV:S× U and the invariant I⊆SI S. In the case of angelic satisfaction, i.e. ♡=a =a, the algorithm also fixes a template for the existentially quantified parametric strategy σ:S×U→Aσ:S× U→ A. The templates are defined via symbolic polynomials of maximal polynomial degree D, which is an algorithm parameter. In Step 2, the algorithm collects a system of quantified polynomial constraints over the symbolic template variables that together entail the defining conditions of the parametric supermartingale certificate V and of I being a valid inductive invariant, by substituting the symbolic polynomial templates in the defining conditions. To handle quantification over the parametric strategy in the expectation condition, for the case of angelic satisfaction, i.e. ⋄=a =a, we remove the existential quantification over the parametric strategy and instead substitute the symbolic polynomial template into the parametric stochastic kernel. For the case of demonic satisfaction, i.e. ⋄=d =d, we remove the universal quantification over the parametric strategy and replace it with ∀a∈A∀ a∈ A, which slightly strengthens the parametric supermartingale certificate conditions and thus preserves soundness of our algorithm. In Step 3, this system of symbolic polynomial constraints is first reduced to solving a system of purely existentially quantified system of polynomial constraints by using existing techniques [14], and finally solved by using an off-the-shelf SMT solver. Any solution gives rise to a valid instance of the parametric supermartingale certificate V and the invariant I. We present the details of the verification algorithm and establish its soundness in Appendix 0.G. 6.2 Synthesis Algorithm We now present our approximate synthesis algorithm which, given an approximation parameter c∈[0,1]c∈[0,1], partitions the parameter set U into two disjoint parameter regions R and R′R such that MR⊧♡ϕ,pM^R _ φ,p and MR′⊧¬♣ϕ,1−pM^R _ φ,1-p with ♣ being the opposite type of satisfaction, where (μ(R)+μ(R′))/μ(U)≥1−c(μ(R)+μ(R ))/μ(U)≥ 1-c. Our synthesis algorithm uses the verification algorithm in Section 6.1 as a subroutine. To that end, we assume the subroutine (M,ϕ,p,♡) Verify(M,φ,p, ) which either (1) returns SAT which stands for the statement M⊧♡ϕ,pM _ φ,p being formally proved, or (2) returns UNSAT or UNKNOWN, depending on the output of the SMT solver. Assumptions. We make the same assumptions as in Section 6.1. In addition, we assume that the parameter set U⊆ℝnU ^n is bounded and covered by a hyperrectangular box B (i.e. a product of intervals). We assume that this box B is provided. Note that the boundedness assumption is also necessary for the approximation synthesis problem to be well-defined, since we need μ(U)<∞μ(U)<∞. Algorithm. The algorithm executes an abstraction refinement procedure which synthesizes two parameter regions R and R′R as unions of disjoint hyperrectangular boxes. It initializes two empty sets of hyperrectangular boxes ⟦R⟧ R and ⟦R′⟧ R , which will be gradually enlarged with verified hyperrectangular boxes until they together cover at least ratio c of the total volume of U. We define volume(⟦R⟧)=∑b∈⟦R⟧μ(b∩U) volume( R )= _b∈ R μ(b∩ U) to be the Lebesgue measure of the part of the parameter valuation set U that it covers, and volume(⟦R′⟧) volume( R ) is defined analogously. Here, we assume that we have access to an oracle that can compute (or at least formally lower bound) μ(b∩U)μ(b∩ U) for any hyperrectangular box b. This assumption is made for simplicity, since volume computation is not our contribution. For the case when the parameter set U is a hyperrectangle (as in our experiments), the computation is trivial and can be done exactly. For the case when U is a polytope (i.e. expressible in linear real arithmetic), the computation can also be done exactly by using classical methods [10]. Finally, for the most general case when U is represented via polynomial real arithmetic, one can compute a lower bound up to arbitrary ϵε-precision by using e.g. the method of [6]. The algorithm proceeds as follows. It defines a queue ToExplore of hyperrectangular boxes to be explored, initialized to =B ToExplore=\B\. It then implements the following abstraction refinement procedure: 1. Check if (volume(⟦R⟧)+volume(⟦R′⟧))/μ(U)≥1−c( volume( R )+ volume( R ))/μ(U)≥ 1-c. If yes, return R and R′R to the user. Otherwise, proceed to Step 2. 2. Pop the next box b from the queue ToExplore. 3. Run (MU∩b,ϕ,p,♡) Verify(M^U∩ b,φ,p, ). If the output is SAT, add b to ⟦R⟧ R . 4. Run (MU∩b,¬ϕ,1−p,♣) Verify(M^U∩ b, φ,1-p, ). If the output is SAT, add b to ⟦R′⟧ R . 5. If neither of the two runs of Verify output SAT, divide b along the longest side into two boxes b1b_1 and b2b_2. Add b1b_1 and b2b_2 to ToExplore. Return to Step 1. The soundness of our approximation synthesis algorithm follows by the soundness of our verification algorithm, which ensures that at any point in the algorithm execution we have MR⊧♡ϕ,pM^R _ φ,p and MR′⊧¬♣ϕ,1−pM^R _ φ,1-p. In addition, the termination condition ensures that (μ(R)+μ(R′))/μ(U)≥1−c(μ(R)+μ(R ))/μ(U)≥ 1-c on output. 7 Experiments We implemented our algorithms in a prototype written in Python.11 1 Public URL: https://github.com/kmallik/parametric-verification-and-control In the back end, the quantified polynomial entailments collected in Step 2 of our verification algorithm are discharged to the third party tool PolyQEnt [15]. We use MathSAT5 [20] and Z3 [24] for SMT solving. Experiments were run on a machine with 72 virtual cores (Xeon Gold 6154 @3GHz), 128 GB RAM (DDR4@2666 MHz). We consider the pMDP described in Example 1, and the approximate synthesis problem for the angelic reachability (and, dually, demonic safety) specification defined in Example 2. We consider three different variants of the pMDP, namely (1) with one purely additive parameter, i.e., u1=0u_1=0 but u2u_2 variable, written as M+M^+; (2) with one purely multiplicative parameter, i.e., u2=1u_2=1 but u1u_1 variable, written as M×M^×; and (3) with both additive and multiplicative parameters, i.e., both u1u_1 and u2u_2 being variable, written as M+,×M^+,×. Table 1: Results for different values of the approximation parameter c. Total time represents the total time the tool needed to reach the specified approximation level. Angelic and Demonic SAT time respective represent the mean and standard deviation of the time of those individual SMT queries that returned “SAT.” TO means timeout of the total runtime, which was set to be 900 ss. While reporting the stats of the SMT calls, the remaining cases (total −- (SAT ++ UNSAT ++ inconclusive)) are timeouts (25 ss). c Total time (ss) Av. time (ss) ang. SAT Av. time (ss) dem. SAT # SMT calls Tot.-SAT-UNSAT-Inconl. Z3 MS Z3 MS Z3 MS Z3 MS M+M^+: u1=0u_1=0, u2∈[−1,1]u_2∈[-1,1], template unknowns = 9 0.40.4 138.48 45.51 8.168.16 4.924.92 0.190.19 0.350.35 22k-18-22k-17 22-3-0-13 0.30.3 310.30 45.62 6.046.04 2.672.67 0.190.19 0.350.35 52k-20-52k-20 22-4-0-14 0.20.2 TO 60.49 - 2.672.67 - 0.300.30 - 30-5-0-19 0.150.15 TO 90.90 - 1.521.52 - 0.300.30 - 62-7-0-37 0.1250.125 TO TO - - - - - - M×M^×: u1∈[−1,1]u_1∈[-1,1], u2=1u_2=1, template unknowns = 9 0.40.4 57.47 75.38 11.5411.54 13.6913.69 7.117.11 11.7511.75 22-3-8-8 38-4-0-22 0.30.3 59.14 89.75 11.8811.88 10.9010.90 7.117.11 11.7511.75 22-4-8-8 62-7-0-37 0.20.2 73.87 117.58 11.9011.90 8.878.87 7.117.11 8.688.68 34-5-13-10 154-14-0-90 0.150.15 83.27 136.08 9.729.72 9.179.17 6.766.76 8.298.29 46-7-18-14 218-21-0-137 0.1250.125 83.32 153.65 9.729.72 8.078.07 6.766.76 8.228.22 46-7-18-14 298-31-0-209 M+,×M^+,×: u1=0u_1=0, u2∈[−1,1]u_2∈[-1,1], template unknowns = 11 0.40.4 214.01 76.56 1.601.60 0.610.61 0.230.23 0.570.57 2k-28-1k-325 86-10-0-52 0.30.3 TO 91.74 - 0.640.64 - 0.610.61 - 134-15-0-81 0.20.2 TO 122.26 - 1.371.37 - 0.720.72 - 270-27-0-181 0.150.15 TO 144.18 - 2.472.47 - 0.920.92 - 360-42-0-256 0.1250.125 TO 177.40 - 3.433.43 - 2.032.03 - 530-65-0-403 Table 1 reports the results of our experiments, with further details (variance in computation times) being available in Table 2 in Appendix 0.H. For each of the three variants of the pMDP, we report results for multiple values for the approximation parameter c. For every call to the verification subroutine, timeout is set to tmax=25st_ =25\,s. Figure 1 visualizes the computed parameter regions. From the results in Table 1, we observe that M+M^+ and M+,×M^+,×, the SMT solver MathSAT5 significantly outperforms Z3, whereas for M×M^×, the trend is opposite. This suggests that different SMT solvers have their own strengths and weaknesses, and choosing the right solver has significant impact on performance. On the other hand, Figure 1 shows how our refinement algorithm is able to solve the approximate synthesis problem with reasonable accuracy. Observe that the granularity of the cells is the finest near the frontier between the two parameter regfions, which is expected. # (a) (b) (c) Figure 1: Partition of the parameter space based on the output of the approximate synthesis procedure. The green region is the angelic reachability region, the red region is the demonic safety region, and the grey region is the inconclusive region. 8 Conclusion We introduced a novel automated framework for verification and approximate synthesis in infinite-state pMDPs based on parametric supermartingale certificates. By combining parameter flattening with template-based synthesis, our approach enables formal reasoning about rich specifications under parametric uncertainty. In future, we plan to extend our methods to quantitative properties and develop heuristics to mitigate current scalability bottlenecks. Acknowledgements This research is supported by the NTU Start Up Grant and the project RYC2024-049116-I funded by MICIU/AEI/10.13039/501100011033 and the ESF+. Part of the work was done while Đorđe Žikelić was at Singapore Management University. References [1] A. Abate, A. Edwards, M. Giacobbe, H. Punchihewa, and D. Roy (2023) Quantitative verification with neural networks. In 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium, September 18-23, 2023, G. A. Pérez and J. Raskin (Eds.), LIPIcs, Vol. 279, p. 22:1–22:18. External Links: Link, Document Cited by: §1, §1. [2] A. Abate, M. Giacobbe, S. Ichtchenko, and D. Roy (2026) Complete ω-regular supermartingale certificates. In 41st Annual Symposium on Logic in Computer Science, LICS 2026, Lisbon, Portugal, July 20-23, 2026, C. Faggian and J. Katoen (Eds.), LIPIcs, Vol. 380, p. 3:1–3:28. External Links: Link, Document Cited by: §1, §1. [3] A. Abate, M. Giacobbe, and D. Roy (2021) Learning probabilistic termination proofs. In Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, A. Silva and K. R. M. Leino (Eds.), Lecture Notes in Computer Science, Vol. 12760, p. 3–26. External Links: Link, Document Cited by: §1, §1. [4] A. Abate, M. Giacobbe, and D. Roy (2024) Stochastic omega-regular verification and control with supermartingales. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, A. Gurfinkel and V. Ganesh (Eds.), Lecture Notes in Computer Science, Vol. 14683, p. 395–419. External Links: Link, Document Cited by: Appendix 0.F, §1, §1, §5, §6.1. [5] A. Abate, M. Giacobbe, and D. Roy (2025) Quantitative supermartingale certificates. In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, R. Piskac and Z. Rakamaric (Eds.), Lecture Notes in Computer Science, Vol. 15932, p. 3–28. External Links: Link, Document Cited by: Appendix 0.F, Appendix 0.G, Appendix 0.G, Appendix 0.G, §1, §1, §5, §6.1, §6.1. [6] S. Akshay, S. Chakraborty, S. Farokhnia, A. K. Goharshady, H. J. Motwani, and D. Zikelic (2025) LP-based weighted model integration over non-linear real arithmetic. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, August 16-22, 2025, p. 9040–9048. External Links: Link, Document Cited by: §6.2. [7] R. B. Ash and C. A. Doléans-Dade (2000) Probability and measure theory. Academic press. Cited by: Appendix 0.A, §2. [8] C. Baier, C. Hensel, L. Hutschenreiter, S. Junges, J. Katoen, and J. Klein (2020) Parametric markov chains: PCTL complexity and fraction-free gaussian elimination. Inf. Comput. 272, p. 104504. External Links: Link, Document Cited by: §1. [9] G. Barthe, J. Katoen, and A. Silva (Eds.) (2020) Foundations of probabilistic programming. Cambridge University Press. External Links: Link, Document, ISBN 9781108770750 Cited by: §1. [10] M. Beck and S. Robins (2007) Computing the continuous discretely: integer-point enumeration in polyhedra. Springer. Cited by: §6.2. [11] A. Chakarov and S. Sankaranarayanan (2013) Probabilistic program analysis with martingales. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, N. Sharygina and H. Veith (Eds.), Lecture Notes in Computer Science, Vol. 8044, p. 511–526. External Links: Link, Document Cited by: Appendix 0.E, Appendix 0.F, §1, §1, §5, Proof, Proof. [12] K. Chatterjee, H. Fu, and A. K. Goharshady (2016) Termination analysis of probabilistic programs through positivstellensatz’s. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, S. Chaudhuri and A. Farzan (Eds.), Lecture Notes in Computer Science, Vol. 9779, p. 3–22. External Links: Link, Document Cited by: Appendix 0.G, Appendix 0.G, Appendix 0.G, §1, §1, §6.1. [13] K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad (2018) Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. 40 (2), p. 7:1–7:45. External Links: Link, Document Cited by: §1, §1. [14] K. Chatterjee, A. K. Goharshady, E. K. Goharshady, M. Karrabi, M. Saadat, M. Seeliger, and D. Zikelic (2025) PolyQEnt: A polynomial quantified entailment solver. In Automated Technology for Verification and Analysis - 23rd International Symposium, ATVA 2025, Bengaluru, India, October 27-31, 2025, Proceedings, M. D’Souza, R. Komondoor, and B. Srivathsan (Eds.), Lecture Notes in Computer Science, Vol. 16145, p. 411–424. External Links: Link, Document Cited by: Appendix 0.G, §6.1. [15] K. Chatterjee, A. K. Goharshady, E. K. Goharshady, M. Karrabi, M. Saadat, M. Seeliger, and Đ. Žikelić (2025) Polyqent: a polynomial quantified entailment solver. In International Symposium on Automated Technology for Verification and Analysis, p. 411–424. Cited by: §7. [16] K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic (2022) Sound and complete certificates for quantitative termination analysis of probabilistic programs. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, S. Shoham and Y. Vizel (Eds.), Lecture Notes in Computer Science, Vol. 13371, p. 55–78. External Links: Link, Document Cited by: Appendix 0.G, Appendix 0.G, Appendix 0.G, §1, §1, §6.1. [17] K. Chatterjee, E. K. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic (2023) On lexicographic proof rules for probabilistic termination. Formal Aspects Comput. 35 (2), p. 11:1–11:25. External Links: Link, Document Cited by: §1, §1. [18] K. Chatterjee, P. Novotný, and D. Zikelic (2017) Stochastic invariants for probabilistic termination. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, G. Castagna and A. D. Gordon (Eds.), p. 145–160. External Links: Link, Document Cited by: Appendix 0.F, §1, §1. [19] K. Chatterjee, K. Sen, and T. A. Henzinger (2008) Model-checking ω-regular properties of interval markov chains. In International Conference on Foundations of Software Science and Computational Structures, p. 302–317. Cited by: §1. [20] A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani (2013) The mathsat5 SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, p. 93–107. External Links: Link, Document Cited by: §7. [21] M. Cubuktepe, N. Jansen, S. Junges, J. Katoen, I. Papusha, H. A. Poonawala, and U. Topcu (2017) Sequential convex programming for the efficient verification of parametric mdps. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, A. Legay and T. Margaria (Eds.), Lecture Notes in Computer Science, Vol. 10206, p. 133–150. External Links: Link, Document Cited by: §1. [22] M. Cubuktepe, N. Jansen, S. Junges, J. Katoen, and U. Topcu (2022) Convex optimization for parameter synthesis in mdps. IEEE Trans. Autom. Control. 67 (12), p. 6333–6348. External Links: Link, Document Cited by: §1. [23] C. Daws (2004) Symbolic and parametric model checking of discrete-time markov chains. In Theoretical Aspects of Computing - ICTAC 2004, First International Colloquium, Guiyang, China, September 20-24, 2004, Revised Selected Papers, Z. Liu and K. Araki (Eds.), Lecture Notes in Computer Science, Vol. 3407, p. 280–294. External Links: Link, Document Cited by: §1. [24] L. M. de Moura and N. S. Bjørner (2008) Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, p. 337–340. External Links: Link, Document Cited by: §7. [25] C. Dehnert, S. Junges, N. Jansen, F. Corzilius, M. Volk, H. Bruintjes, J. Katoen, and E. Ábrahám (2015) PROPhESY: A probabilistic parameter synthesis tool. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, D. Kroening and C. S. Pasareanu (Eds.), Lecture Notes in Computer Science, Vol. 9206, p. 214–231. External Links: Link, Document Cited by: §1. [26] W. H. Fleming and R. W. Rishel (2012) Deterministic and stochastic optimal control. Vol. 1, Springer Science & Business Media. Cited by: §1. [27] R. Givan, S. M. Leach, and T. L. Dean (2000) Bounded-parameter markov decision processes. Artif. Intell. 122 (1-2), p. 71–109. External Links: Link, Document Cited by: §1. [28] E. M. Hahn, T. Han, and L. Zhang (2011) Synthesis for PCTL in parametric markov decision processes. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, M. G. Bobaru, K. Havelund, G. J. Holzmann, and R. Joshi (Eds.), Lecture Notes in Computer Science, Vol. 6617, p. 146–161. External Links: Link, Document Cited by: §1. [29] D. Handelman (1988) Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics 132 (1), p. 35–62. Cited by: Appendix 0.G. [30] T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic (2025) Supermartingale certificates for quantitative omega-regular verification and control. In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, R. Piskac and Z. Rakamaric (Eds.), Lecture Notes in Computer Science, Vol. 15932, p. 29–55. External Links: Link, Document Cited by: Appendix 0.F, Appendix 0.G, Appendix 0.G, Appendix 0.G, §1, §1, §5, §6.1, §6.1. [31] N. Jansen, F. Corzilius, M. Volk, R. Wimmer, E. Ábrahám, J. Katoen, and B. Becker (2014) Accelerating parametric probabilistic verification. In Quantitative Evaluation of Systems - 11th International Conference, QEST 2014, Florence, Italy, September 8-10, 2014. Proceedings, G. Norman and W. H. Sanders (Eds.), Lecture Notes in Computer Science, Vol. 8657, p. 404–420. External Links: Link, Document Cited by: §1. [32] N. Jansen, S. Junges, and J. Katoen (2022) Parameter synthesis in markov models: A gentle survey. In Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, J. Raskin, K. Chatterjee, L. Doyen, and R. Majumdar (Eds.), Lecture Notes in Computer Science, Vol. 13660, p. 407–437. External Links: Link, Document Cited by: §1, §1, §1. [33] S. Junges, E. Ábrahám, C. Hensel, N. Jansen, J. Katoen, T. Quatmann, and M. Volk (2024) Parameter synthesis for markov models: covering the parameter space. Formal Methods Syst. Des. 62 (1), p. 181–259. External Links: Link, Document Cited by: §1, §1, §3, §3, §6, Remark 1, Remark 1. [34] S. Kura, H. Unno, and T. Tsukada (2026) Supermartingales for unique fixed points: A unified approach to lower bound verification. Proc. ACM Program. Lang. 10 (PLDI), p. 2525–2548. External Links: Link, Document Cited by: §1, §1. [35] S. Kura and H. Unno (2026) A hierarchy of supermartingales for ω-regular verification. Proc. ACM Program. Lang. 10 (PLDI), p. 253–276. External Links: Link, Document Cited by: §1, §1. [36] M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger (2022) Stability verification in stochastic control systems via neural network supermartingales. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, p. 7326–7336. External Links: Link, Document Cited by: §1, §1. [37] R. Majumdar and V. R. Sathiyanarayana (2025) Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang. 9 (POPL), p. 1871–1902. External Links: Link, Document Cited by: §1, §1. [38] A. McIver, C. Morgan, B. L. Kaminski, and J. Katoen (2018) A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2 (POPL), p. 33:1–33:28. External Links: Link, Document Cited by: §1, §1. [39] A. Peruffo and A. Abate (2021) Formal abstraction and synthesis of parametric stochastic processes. In International Conference on Formal Modeling and Analysis of Timed Systems, p. 135–153. Cited by: §1. [40] S. Prajna, A. Jadbabaie, and G. J. Pappas (2007) A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control. 52 (8), p. 1415–1428. External Links: Link, Document Cited by: Appendix 0.C, Appendix 0.C, Appendix 0.F, §1, §1, §5.1, §5.1, §5.1, §5. [41] M. L. Puterman (1994) Markov decision processes: discrete stochastic dynamic programming. Wiley Series in Probability and Statistics, Wiley. External Links: Link, Document, ISBN 978-0-47161977-2 Cited by: §1, §2. [42] M. Putinar (1993) Positive polynomials on compact semi-algebraic sets. Indiana University Mathematics Journal 42 (3), p. 969–984. Cited by: Appendix 0.G. [43] T. Quatmann, C. Dehnert, N. Jansen, S. Junges, and J. Katoen (2016) Parameter synthesis for markov models: faster than ever. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, C. Artho, A. Legay, and D. Peled (Eds.), Lecture Notes in Computer Science, Vol. 9938, p. 50–67. External Links: Link, Document Cited by: §1. [44] O. So, A. Clark, and C. Fan (2023) Almost-sure safety guarantees of stochastic zero-control barrier functions do not hold. CoRR abs/2312.02430. External Links: Link, Document, 2312.02430 Cited by: Remark 3. [45] J. Steinhardt and R. Tedrake (2012) Finite-time regional verification of stochastic non-linear systems. Int. J. Robotics Res. 31 (7), p. 901–923. External Links: Link, Document Cited by: §1, §1. [46] T. Takisaka, Y. Oyabu, N. Urabe, and I. Hasuo (2021) Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43 (2), p. 5:1–5:46. External Links: Link, Document Cited by: §1, §1. [47] J. Wang, Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady (2021) Quantitative analysis of assertion violations in probabilistic programs. In PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, S. N. Freund and E. Yahav (Eds.), p. 1171–1186. External Links: Link, Document Cited by: §1, §1. [48] P. Wang, T. Yang, H. Fu, G. Li, and C.-H. L. Ong (2024) Static posterior inference of bayesian probabilistic programming via polynomial solving. Proc. ACM Program. Lang. 8 (PLDI), p. 1361–1386. External Links: Link, Document Cited by: §1, §1. [49] D. Williams (1991) Probability with martingales. Cambridge university press. Cited by: item 3, §1, §2. [50] B. Xue, R. Li, N. Zhan, and M. Fränzle (2021) Reach-avoid analysis for stochastic discrete-time systems. In 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, p. 4879–4885. External Links: Link, Document Cited by: §1. [51] B. Xue (2024) Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems. CoRR abs/2408.15572. External Links: Link, Document, 2408.15572 Cited by: §1. [52] D. Zhi, P. Wang, S. Liu, C.-H. L. Ong, and M. Zhang (2024) Unifying qualitative and quantitative safety verification of dnn-controlled systems. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, A. Gurfinkel and V. Ganesh (Eds.), Lecture Notes in Computer Science, Vol. 14682, p. 401–426. External Links: Link, Document Cited by: §1, §1. [53] D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee (2023) Learning control policies for stochastic systems with reach-avoid guarantees. In Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, B. Williams, Y. Chen, and J. Neville (Eds.), p. 11926–11935. External Links: Link, Document Cited by: Appendix 0.D, Appendix 0.D, Appendix 0.F, §1, §5.2, §5.2, §5. [54] D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger (2023) Compositional policy learning in stochastic control systems with formal guarantees. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine (Eds.), External Links: Link Cited by: §1. Appendix 0.A Proof of Proposition 1 Let σ be a parametric strategy and ϕφ a specification in the parametric MDP, with the corresponding parameter flattened strategy σ~ σ and the parameter flattened specification ϕ~ φ. Let s∈Inits∈ Init be an initial state and u∈Uu∈ U be a parameter valuation. To prove the proposition claim, we need to show ℙsM[u],σ[u][ϕ]=ℙ(s,u)M~,σ~[ϕ~].P_s^M[u],σ[u][φ]=P_(s,u) M, σ[ φ]. In what follows, denote by (PathsM[u],ℱPathsM[u],ℙsM[u],σ[u])( Path^M[u]_s,F_ Path^M[u]_s,P_s^M[u],σ[u]) the probability space induced by the MDP M[u]M[u] with the initial state s under strategy σ[u]σ[u], and denote by (Path(s,u)M~,ℱPath(s,u)M~,ℙ(s,u)M~,σ~)( Path M_(s,u),F_ Path M_(s,u),P_(s,u) M, σ) the probability space induced by the parameter flattened MDP M~ M with the initial state (s,u)(s,u) under the parameter flattened strategy σ~ σ. Recall, the probability spaces are formally defined via the cylinder construction [7]. The proof proceeds in four steps: 1. Bijection between paths. We construct a bijection Φ:PathsM[u]→Path(s,u)M~ : Path^M[u]_s→ Path M_(s,u) between the sets of all infinite paths in the two MDPs. The bijection is defined as follows (also defined in p.9 in the paper) Φ(s,a0,s1,a1,…)=(s,u),a0,(s1,u),a1,… (s,a_0,s_1,a_1,…)=(s,u),a_0,(s_1,u),a_1,… with inverse Φ−1((s,u),a0,(s1,u),a1,…)=s,a0,s1,a1,…. ^-1((s,u),a_0,(s_1,u),a_1,…)=s,a_0,s_1,a_1,…. We can easily see that Φ−1∘Φ ^-1 and Φ∘Φ−1 ^-1 are the identity functions over the sets of infinite paths in the two MDPs, hence, they are indeed bijections and inverses of each other. 2. Bijection between measurable sets of paths. We now show that Φ gives rise to a bijection Φℱ:ℱPathsM[u]→ℱPath(s,u)M~ ^F:F_ Path^M[u]_s _ Path M_(s,u) between the two σ-algebras of infinite paths of the two MDPs. For every measurable set of paths B∈ℱPathsM[u]B _ Path^M[u]_s, define Φℱ(B)=Φ(ρ)∣ρ∈B. ^F(B)=\ (ρ) ρ∈ B\. We show that Φℱ ^F is a bijection with the inverse (Φℱ)−1:ℱPath(s,u)M~→ℱPathsM[u]( ^F)^-1:F_ Path M_(s,u) _ Path^M[u]_s defined via (Φℱ)−1(B~)=Φ−1(ρ~)∣ρ~∈B~( ^F)^-1( B)=\ ^-1( ρ) ρ∈ B\ for every B~∈ℱPath(s,u)M~ B _ Path M_(s,u). The fact that (Φℱ)−1∘Φℱ( ^F)^-1 ^F and Φℱ∘(Φℱ)−1 ^F ( ^F)^-1 are the identity functions over the two sigma algebras easily follows from the fact that Φ and Φ−1 ^-1 are inverses. Hence, Φℱ ^F and (Φℱ)−1( ^F)^-1 are indeed bijections and inverses of each other. 3. Bijection is measure preserving. Next, we show that the bijection Φℱ ^F over σ-algebras is measure preserving, i.e. that ℙsM[u],σ[u][B]=ℙ(s,u)M~,σ~[Φℱ(B)]P_s^M[u],σ[u][B]=P_(s,u) M, σ[ ^F(B)] holds for all B∈ℱPathsM[u]B _ Path^M[u]_s. To prove this, observe first that ℙsM[u],σ[u][⋅]P_s^M[u],σ[u][·] and ℙ(s,u)M~,σ~[Φℱ(⋅)]P_(s,u) M, σ[ ^F(·)] are two probability measures over the measurable spaces (PathsM[u],ℱPathsM[u])( Path^M[u]_s,F_ Path^M[u]_s) and (Path(s,u)M~,ℱPath(s,u)M~)( Path M_(s,u),F_ Path M_(s,u)), respectively. Thus, we want to prove that these two probability measures are equal on all B∈ℱPathsM[u]B _ Path^M[u]_s. To prove this, it suffices to prove that they are equal on a set of events that generates the σ-algebra ℱPathsM[u]F_ Path^M[u]_s (see e.g. [49, Section 1.6], where it is shown that any two probability measures that agree on a π-system must agree on the whole σ-algebra generated by that π-system). In our case, the σ-algebra ℱPathsM[u]F_ Path^M[u]_s is generated by cylinder sets, i.e. sets of the form Cyl(s,a0,s1,a1,…,sk)=ρ∈PathsM[u]∣s,a0,s1,a1,…,sk is a prefix of ρCyl(s,a_0,s_1,a_1,…,s_k)=\ρ∈ Path^M[u]_s s,a_0,s_1,a_1,…,s_k is a prefix of ρ\. Now, observe that ℙsM[u],σ[u][Cyl(s,a0,s1,a1,…,sk)]=ℙ(s,u)M~,σ~[Cyl((s,u),a0,(s1,u),a1,…,(sk,u)))]=ℙ(s,u)M~,σ~[Φℱ(Cyl(s,a0,s1,a1,…,sk))], split&P_s^M[u],σ[u][Cyl(s,a_0,s_1,a_1,…,s_k)]\\ &=P_(s,u) M, σ[Cyl((s,u),a_0,(s_1,u),a_1,…,(s_k,u)))]\\ &=P_(s,u) M, σ[ ^F(Cyl(s,a_0,s_1,a_1,…,s_k))], split where the first equality follows from the cylinder construction and how the probability measures over the two MDPs are defined, whereas the second equality follows from our definition of the bijection Φℱ ^F. Hence, the two probability measures agree on all cylinder sets which generate the σ-algebra ℱPathsM[u]F_ Path^M[u]_s, hence they also must agree on all elements of the σ-algebra ℱPathsM[u]F_ Path^M[u]_s. This concludes our proof that Φℱ ^F is measure preserving. 4. Proof of the proposition claim. We are finally ready to prove the proposition claim, i.e. that ℙsM[u],σ[u][ϕ]=ℙ(s,u)M~,σ~[ϕ~]P_s^M[u],σ[u][φ]=P_(s,u) M, σ[ φ]. First, recall that the parameter flattened specification ϕ~ φ is defined via ϕ~=(s,u),a0,(s1,u),a1,…∣s,a0,s1,a1,⋯∈ϕ∧u∈U. φ=\(s,u),a_0,(s_1,u),a_1,… s,a_0,s_1,a_1,…∈φ u∈ U\. Hence, we have ϕ~=Φℱ(ϕ) φ= ^F(φ). Now, by Step 3 above Φℱ ^F is measure preserving, so it follows that ℙsM[u],σ[u][ϕ]=ℙ(s,u)M~,σ~[ϕ~]P_s^M[u],σ[u][φ]=P_(s,u) M, σ[ φ], which proves the claim. ∎ Appendix 0.B Proof of Theorem 4.1 We distinguish between the cases of angelic and demonic satisfaction. Angelic satisfaction. Suppose that ♡=a =a. We have M⊧aϕ,p≡∃σ∈StrM.∀u∈U.∀s∈Init.ℙsM[u],σ[u][ϕ]≥p.M _aφ,p ≡ ∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ Init.\,\,\,P_s^M[u],σ[u][φ]≥ p. On the other hand, for the flattened MDP M~ M, the parameter valuations are now incorporated into the state space so angelic satisfaction reduces to M~⊧aϕ~,p≡∃σ∈StrM~.∀(s,u)∈Init×U.ℙ(s,u)M~,σ~[ϕ~]≥p. M _a φ,p ≡ ∃σ∈ Str M.\,\,\,∀(s,u)∈ Init× U.\,\,\,P_(s,u) M, σ[ φ]≥ p. Since each parametric strategy in M induces a parameter flattened strategy σ~ σ in the parameter flattened MDP M~ M and vice versa, and since by Proposition 1 we have that ℙsM[u],σ[u][ϕ]≥pP_s^M[u],σ[u][φ]≥ p if and only if ℙ(s,u)M~,σ~[ϕ~]≥pP_(s,u) M, σ[ φ]≥ p, we conclude that M⊧aϕ,pM _aφ,p if and only if M~⊧aϕ~,p M _a φ,p. Demonic satisfaction. Suppose that ♡=d =d. We have M⊧dϕ,p≡∀σ∈StrM.∀u∈U.∀s∈Init.ℙsM[u],σ[u][ϕ]≥p.M _dφ,p ≡ ∀σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ Init.\,\,\,P_s^M[u],σ[u][φ]≥ p. On the other hand, for the flattened MDP M~ M, the parameter valuations are now incorporated into the state space so demonic satisfaction reduces to M~⊧dϕ~,p≡∀σ∈StrM~.∀(s,u)∈Init×U.ℙ(s,u)M~,σ~[ϕ~]≥p. M _d φ,p ≡ ∀σ∈ Str M.\,\,\,∀(s,u)∈ Init× U.\,\,\,P_(s,u) M, σ[ φ]≥ p. Since each parametric strategy in M induces a parameter flattened strategy σ~ σ in the parameter flattened MDP M~ M and vice versa, and since by Proposition 1 we have that ℙsM[u],σ[u][ϕ]≥pP_s^M[u],σ[u][φ]≥ p if and only if ℙ(s,u)M~,σ~[ϕ~]≥pP_(s,u) M, σ[ φ]≥ p, we conclude that M⊧dϕ,pM _dφ,p if and only if M~⊧dϕ~,p M _d φ,p. ∎ Appendix 0.C Proof of Theorem 5.1 Suppose that there exists a parametric SBF V for X with respect to I and ♡ . We distinguish between angelic and demonic satisfaction. Angelic satisfaction. Consider first the case of ♡=a =a. Let σ be a parametric strategy whose existence is ensured by the Expected decrease condition for angelic satisfaction, and let σ~ σ be the parameter flattened strategy of σ. Then, by the defining conditions of parametric SBFs in Definition 2, it follows that V:S×U→ℝV:S× U is an SBF for the safe set X×UX× U with respect to the invariant I×UI× U in the non-parametric Markov chain defined by the parameter flattened MDP M~ M and the parameter flattened strategy σ~ σ. Hence, by the soundness of SBFs for proving probability p∈[0,1)p∈[0,1) safety in Markov chains [40], it follows that for all initial states (s,u)∈Init×U(s,u)∈ Init× U in the parameter flattened MDP M~ M, we have ℙ(s,u)M~,σ~[Safe(X×U)]≥pP_(s,u) M, σ[ Safe(X× U)]≥ p. Thus, we have M~⊧aSafe(X×U),p M _a Safe(X× U),p. Hence, by Theorem 4.1, we conclude that M⊧aSafe(X),pM _a Safe(X),p, as claimed. Demonic satisfaction. Consider now the case of ♡=d =d. Let σ~ σ be an arbitrary strategy in the parameter flattened MDP M~ M. Then, by the defining conditions of parametric SBFs in Definition 2, it follows that V:S×U→ℝV:S× U is an SBF for the safe set X×UX× U with respect to the invariant I×UI× U in the non-parametric Markov chain defined by the parameter flattened MDP M~ M and the parameter flattened strategy σ~ σ. Hence, by the soundness of SBFs for proving probability p∈[0,1)p∈[0,1) safety in Markov chains [40], it follows that for all initial states (s,u)∈Init×U(s,u)∈ Init× U in the parameter flattened MDP M~ M, we have ℙ(s,u)M~,σ~[Safe(X×U)]≥pP_(s,u) M, σ[ Safe(X× U)]≥ p. Since the strategy σ~ σ in M~ M was arbitrary, we have M~⊧dSafe(X×U),p M _d Safe(X× U),p. Hence, by Theorem 4.1, we conclude that M⊧dSafe(X),pM _d Safe(X),p, as claimed. ∎ Appendix 0.D Proof of Theorem 5.2 Suppose that there exists a parametric RASM V for T with respect to I and ♡ . We distinguish between angelic and demonic satisfaction. Angelic satisfaction. Consider first the case of ♡=a =a. Let σ be a parametric strategy whose existence is ensured by the Expected decrease condition for angelic satisfaction, and let σ~ σ be the parameter flattened strategy of σ. Then, by the defining conditions of parametric RASMs in Definition 3, it follows that V:S×U→ℝV:S× U is a RASM for the target set T×UT× U with respect to the invariant I×UI× U in the non-parametric Markov chain defined by the parameter flattened MDP M~ M and the parameter flattened strategy σ~ σ. Hence, by the soundness of RASMs for proving probability p∈[0,1)p∈[0,1) reachability in Markov chains [53], it follows that for all initial states (s,u)∈Init×U(s,u)∈ Init× U in the parameter flattened MDP M~ M, we have ℙ(s,u)M~,σ~[Reach(T×U)]≥pP_(s,u) M, σ[ Reach(T× U)]≥ p. Thus, we have M~⊧aReach(T×U),p M _a Reach(T× U),p. Hence, by Theorem 4.1, we conclude that M⊧aReach(T),pM _a Reach(T),p, as claimed. Demonic satisfaction. Consider now the case of ♡=d =d. Let σ~ σ be an arbitrary strategy in the parameter flattened MDP M~ M. Then, by the defining conditions of parametric RASMs in Definition 3, it follows that V:S×U→ℝV:S× U is a RASM for the target set T×UT× U with respect to the invariant I×UI× U in the non-parametric Markov chain defined by the parameter flattened MDP M~ M and the parameter flattened strategy σ~ σ. Hence, by the soundness of RASMs for proving probability p∈[0,1)p∈[0,1) reachability in Markov chains [53], it follows that for all initial states (s,u)∈Init×U(s,u)∈ Init× U in the parameter flattened MDP M~ M, we have ℙ(s,u)M~,σ~[Reach(T×U)]≥pP_(s,u) M, σ[ Reach(T× U)]≥ p. Since the strategy σ~ σ in M~ M was arbitrary, we have M~⊧dReach(T×U),p M _d Reach(T× U),p. Hence, by Theorem 4.1, we conclude that M⊧dReach(T),pM _d Reach(T),p, as claimed. ∎ Appendix 0.E Parametric Supermartingales for Probability 1 Reachability We now present a parametric spermartingale certificate generalization of ranking supermartingaes (RSMs) for proving probability 11 (a.k.a. almost-sure) reachability [11]. We first recall (non-parametric) RSMs. Intuitively, given a Markov chain M, a set of target states T that we want to prove is reached with probability 11, and an invariant I that over-approximates the set of all reachable states, an RSM is a measurable function V:S→ℝV:S that to each state assigns a real value that is required to satisfy the following two conditions: (C1) V is non-negative at all states in the invariant I, and (C2) at all non-target states, i.e. states in I T, V strictly decreases in expected value by at least ϵ>0ε>0 upon the one-step execution of the Markov chain. The following definition formalizes the above intuition and generalizes it to the setting of parametric MDPs by instantiating it in the state space of parameter flattened MDP. Since parametric RSMs are defined over the state space of parameter flattened MDP, they are defined as measurable functions of type V:S×U→ℝV:S× U that map states of the parameter flattened MDP to real values. Definition 4 (Parametric RSMs) Let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a parametric MDP, I∈ℱSI _S be an invariant, T∈ℱST _S be a set of target states, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. A parametric ranking supermartingale (parametric RSM) for T with respect to I and ♡ is a measurable function V:S×U→ℝV:S× U , which is required to satisfy the following four conditions: 1. Nonnegativity. V(s,u)≥0V(s,u)≥ 0 for all s∈Is∈ I and u∈Uu∈ U. 2. Expected decrease. We distinguish between angelic and demonic satisfaction: (a) Angelic satisfaction, i.e. ♡=a =a. There exist ϵ>0ε>0 and a parametric strategy σ:U×S→Aσ:U× S→ A in M such that, for every parameter valuation u∈Uu∈ U and for every non-target state s∈I ∈ I T, V satisfies expected decrease for the action a=σ[u](s)a=σ[u](s), i.e. ∃σ∈StrM.∀u∈U.∀s∈I.s∈I ⇒V(s,u)≥s′∼P(⋅∣u,s,σ[u](s))[V(s′,u)]+ϵ. split∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,&∀ s∈ I.\,\,\,s∈ I T\\ & V(s,u) _s P(· u,s,σ[u](s))[V(s ,u)]+ε. split (b) Demonic satisfaction, i.e. ♡=d =d. There exists ϵ>0ε>0 such that for all parametric strategies σ:U×S→Aσ:U× S→ A in M, for every parameter valuation u∈Uu∈ U and for every non-target state s∈I ∈ I T, V satisfies expected decrease for the action a=σ[u](s)a=σ[u](s), i.e. ∀σ∈StrM.∀u∈U.∀s∈I.s∈I ⇒V(s,u)≥s′∼P(⋅∣u,s,σ[u](s))[V(s′,u)]+ϵ. split∀σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,&∀ s∈ I.\,\,\,s∈ I T\\ & V(s,u) _s P(· u,s,σ[u](s))[V(s ,u)]+ε. split The following theorem shows that parametric RSMs provide a sound proof rule for proving probability 11 reachability in parametric MDPs. Theorem 0.E.1 (Soundness of parametric RSMs) Let M be a parametric MDP, I be an invariant, T be a set of target states, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. Suppose that there exists a parametric RSM for T with respect to I and ♡ . Then, we have M⊧♡Reach(T),1M _ Reach(T),1. Proof Suppose that there exists a parametric RSM V for T with respect to I and ♡ . We distinguish between angelic and demonic satisfaction. Angelic satisfaction. Consider first the case of ♡=a =a. Let σ be a parametric strategy whose existence is ensured by the Expected decrease condition for angelic satisfaction, and let σ~ σ be the parameter flattened strategy of σ. Then, by the defining conditions of parametric RSMs in Definition 4, it follows that V:S×U→ℝV:S× U is an RSM for the target set T×UT× U with respect to the invariant I×UI× U in the non-parametric Markov chain defined by the parameter flattened MDP M~ M and the parameter flattened strategy σ~ σ. Hence, by the soundness of RSMs for proving probability 1 reachability in Markov chains [11], it follows that for all initial states (s,u)∈Init×U(s,u)∈ Init× U in the parameter flattened MDP M~ M, we have ℙ(s,u)M~,σ~[Reach(T×U)]=1P_(s,u) M, σ[ Reach(T× U)]=1. Thus, we have M~⊧aReach(T×U),1 M _a Reach(T× U),1. Hence, by Theorem 4.1, we conclude that M⊧aReach(T),1M _a Reach(T),1, as claimed. Demonic satisfaction. Consider now the case of ♡=d =d. Let σ~ σ be an arbitrary strategy in the parameter flattened MDP M~ M. Then, by the defining conditions of parametric RSMs in Definition 4, it follows that V:S×U→ℝV:S× U is an RSM for the target set T×UT× U with respect to the invariant I×UI× U in the non-parametric Markov chain defined by the parameter flattened MDP M~ M and the parameter flattened strategy σ~ σ. Hence, by the soundness of RSMs for proving probability 1 reachability in Markov chains [11], it follows that for all initial states (s,u)∈Init×U(s,u)∈ Init× U in the parameter flattened MDP M~ M, we have ℙ(s,u)M~,σ~[Reach(T×U)]=1P_(s,u) M, σ[ Reach(T× U)]=1. Since the strategy σ~ σ in M~ M was arbitrary, we have M~⊧dReach(T×U),1 M _d Reach(T× U),1. Hence, by Theorem 4.1, we conclude that M⊧dReach(T),1M _d Reach(T),1, as claimed. ∎ Appendix 0.F Parametric Generalization of Other Supermartingale Certificates Our presentation so far has focused on parametric generalizations of established supermartingale certificates, such as RSMs, SBFs and RASMs, which serve as our illustrating examples throughout the paper. However, our generalization is applicable to all other supermartingale certificates for measurable Markov chains whose defining conditions are of one of the two types that we formalize below. Bound and expectation conditions. Let M=(S,ℱS,A,ℱA,P,Init)M=(S,F_S,A,F_A,P, Init) be a Markov chain and I∈ℱSI _S be an invariant. For a measurable function V:S→ℝV:S , we define bound conditions and expectation conditions as follows: 1. Bound condition. Consider a measurable set of states X∈ℱSX _S and a Borel-measurable set of real values Y⊆ℝY . We define the (X,Y)(X,Y)-bound condition to be the logical formula which encodes that, for all invariant states in the set X, the value of V must lie in the set Y, i.e. ∀s∈I.s∈X⇒V(s)∈Y.∀ s∈ I.\,\,\,s∈ X V(s)∈ Y. 2. Expectation condition. Consider a measurable set of states X∈ℱSX _S and two Borel-measurable set of real values Y,Z⊆ℝY,Z . We define the (X,Y,Z)(X,Y,Z)-expectation condition to be the logical formula which encodes that, for all invariant states in the set X at which the value of V lies in the set Y, the difference between the value of V and the expected value of V upon the one-step execution of the Markov chain must lie in the set Z, i.e. ∀s∈I.s∈X∧V(s)∈Y⇒V(s)−s′∈P(⋅∣s)∈Z.∀ s∈ I.\,\,\,s∈ X V(s)∈ Y V(s)-E_s ∈ P(· s)∈ Z. Observe that the defining conditions of all supermartingale certificates considered in this work, namely RSMs, SBFs and RASMs, are either bound conditions (all but the expectation decrease condition) or expectation conditions (the expectation decrease condition). This remains true for many other supermartingale certificates considered in the literature as well. For instance, all defining conditions of repulsing supermartingales [18] which were also considered for proving quantiative reachability and safety, are either bound or expectation conditions. This is also true even the recently introduced Streett supermartingales [4, 5] and limit-deterministic Büchi supermartingales [30] for proving satisfaction of general ω-regular specifications. Generalization to parametric MDPs. Consider now a supermartingale certificate for measurable Markov chains whose all defining conditions are either bound or expectation conditions. We extend it to the setting of parametric MDPs as follows. Let M=(S,ℱS,A,ℱA,P,Init,U)M=(S,F_S,A,F_A,P, Init,U) be a parametric MDP, I∈ℱSI _S be an invariant, and ♡∈a,d ∈\a,d\ denote either angelic or demonic satisfaction. For each defining condition of the supermartingale certificate in Markov chains, we define its parametric generalization as follows: 1. Parametric generalization of bound conditions. For a bound condition ∀s∈I.s∈X⇒V(s)∈Y∀ s∈ I.\,\,\,s∈ X V(s)∈ Y, its parametric generalization remains unchanged, i.e. we keep the condition ∀s∈I.s∈X⇒V(s)∈Y∀ s∈ I.\,\,\,s∈ X V(s)∈ Y. 2. Parametric generalization of expectation conditions. For an expectation condition ∀s∈I.s∈X∧V(s)∈Y⇒V(s)−s′∈P(⋅∣s)∈Z∀ s∈ I.\,\,\,s∈ X V(s)∈ Y V(s)-E_s ∈ P(· s)∈ Z, we generalize it to the setting of parametric MDPs as follows depending on whether we are interested in angelic satisfaction or demonic satisfaction: (a) Angelic satisfaction. If ♡=a =a, then the expectation condition is generalized to the setting of parametric MDPs as follows: We require that there exists a parametric strategy σ:U×S→Aσ:U× S→ A such that, for every parameter valuation u∈Uu∈ U and for every state s∈Is∈ I, if the premise of the entailment holds then the conclusion of the entailment holds, i.e. ∃σ∈StrM.∀u∈U.∀s∈I.s∈X∧V(s)∈Y⇒V(s)−s′∈P(⋅∣u,s,σ[u](s))∈Z split∃σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ I.\,\,\,&s∈ X V(s)∈ Y\\ & V(s)-E_s ∈ P(· u,s,σ[u](s))∈ Z split (b) Demonic satisfaction. If ♡=d =d, then the expectation condition is generalized to the setting of parametric MDPs as follows: We require that for all parametric strategies σ:U×S→Aσ:U× S→ A, for every parameter valuation u∈Uu∈ U and for every state s∈Is∈ I, if the premise of the entailment holds then the conclusion of the entailment holds, i.e. ∀σ∈StrM.∀u∈U.∀s∈I.s∈X∧V(s)∈Y⇒V(s)−s′∈P(⋅∣u,s,σ[u](s))∈Z split∀σ∈ Str^M.\,\,\,∀ u∈ U.\,\,\,∀ s∈ I.\,\,\,&s∈ X V(s)∈ Y\\ & V(s)-E_s ∈ P(· u,s,σ[u](s))∈ Z split Note that the defining conditions of parametric RSMs in Definition 4, parametric SBFs in Definition 2 and parametric RASMs in Definition 3 are obtained precisely by applying these two parametric generalizations to the defining conditions of RSMs [11], SBFs [40] and RASMs [53]. It can also be analogously applied to obtain the parametric generalization of any other supermartingale certificate for Markov chains whose defining conditions are all either bound or expectation conditions. The proof of generalization soundness follows analogously as the proofs of Theorem 0.E.1, Theorem 5.1 and Theorem 5.2, which all proceed by showing that the parametric supermartingale certificate induces a non-parametric supermartingale certificate in the parameter flattened MDP and then using the soundness of the non-parametric supermartingale certificate for proving the specification of interest, while taking additional care to correctly handle the cases of angelic and demonic satisfaction. Appendix 0.G Verification Algorithm Our verification algorithm follows a template-based synthesis approach and reduces the computation of the parametric supermartingale certificate V and the invariant I to solving a system of polynomial real constraints. This is a standard procedure for synthesizing (non-parametric) supermartingale certificates, see e.g. [12, 16, 5, 30]. The algorithm proceeds in three steps. Step 1: Fixing templates. The algorithm fixes symbolic polynomial templates for the parametric supermartingale certificate V:S×U→ℝV:S× U and the invariant I⊆SI S. In the case of angelic satisfaction, i.e. ♡=a =a, the algorithm also fixes a template for the existentially quantified parametric strategy σ:S×U→Aσ:S× U→ A. For the parametric supermartingale certificate V, the symbolic polynomial template is defined by a polynomial expression PV(s1,…,snS,u1,…,un)P_V(s_1,…,s_n_S,u_1,…,u_n) over the state variables and parameters of polynomial degree D, which is an algorithm parameter. The values of coefficients of each monomial are at this stage unknown and are given by the symbolic template variables, whose concrete values will be computed at the later stages of the algorithm. For the invariant I, since it is a subset of the state space, we define its symbolic polynomial template to be the satisfiability set of a conjunction of finitely many symbolic polynomial inequalities (PI1(s))≥0∧⋯∧(PINI(s)≥0)(P^1_I(s))≥ 0 … (P^N_I_I(s)≥ 0), where each PIj(s1,…,snS)P^j_I(s_1,…,s_n_S) is a polynomial over the state variables of polynomial degree D, while the number NIN_I of inequalities is another algorithm parameter. Finally, if ♡=a =a, the symbolic polynomial template for the existentially quantified parametric strategy σ is a symbolic polynomial Pσ(s1,…,snS,u1,…,un)P_σ(s_1,…,s_n_S,u_1,…,u_n) over the state variables and parameters of polynomial degree D. Example 6 Suppose that the dimension of the state space is p=1p=1 and the number of parameters is n=2n=2, as in Example 1. Suppose that the polynomial degree parameter is D=1D=1 and NI=1N_I=1. The symbolic polynomial template of V is a degree 11 polynomial expression defined by PV(s1,u1,u2)=α1⋅s1+α2⋅u1+α3⋅u2+α4P_V(s_1,u_1,u_2)= _1· s_1+ _2· u_1+ _3· u_2+ _4, where α1,…,α4 _1,…, _4 are the symbolic template variables. The symbolic polynomial template for I is s∈S∣PI1(s1)≥0\s∈ S P_I^1(s_1)≥ 0\ with PI1(s1)=β1⋅s1+β2P_I^1(s_1)= _1· s_1+ _2, where β1,β2 _1, _2 are the symbolic template variables. If ♡=a =a, the symbolic polynomial template for σ is Pσ(s1,u1,u2)=γ1⋅s1+γ2⋅u1+γ3⋅u2+γ4P_σ(s_1,u_1,u_2)= _1· s_1+ _2· u_1+ _3· u_2+ _4, where γ1,…,γ4 _1,…, _4 are the symbolic template variables. Step 2: Constraint collection. The algorithm collects a system of polynomial constraints over the symbolic template variables which together encode that all defining conditions of the parametric supermartingale certificate V are satisfied, as well as that the invariant I is an inductive invariant. This is achieved by substituting the polynomial expressions that define the symbolic polynomial templates in Step 1 into the defining conditions of parametric supermartingale certificates and inductive invariants. For the case of angelic satisfaction, i.e. ♡=a =a, we remove the existential quantification over the parametric strategy and instead substitute the symbolic polynomial template Pσ(s,u)P_σ(s,u) into the parametric stochastic kernel. For the case of demonic satisfaction, i.e. ♡=d =d, we remove the universal quantification over the parametric strategy and replace it with ∀a∈A∀ a∈ A, which slightly strengthens the parametric supermartingale certificate conditions and thus preserves soundness of our algorithm. Since constraint collection is standard and analogous to existing template-based synthesis algorithms for non-parametric supermartingale certificates [12, 16, 5, 30], we omit the details. Step 3: Constraint solving. The previous step results in a system of quantified polynomial entailments, i.e. constraints of the form ∀a∈A.∀u∈U.∀s∈I.Φ(s,u)⟹Ψ(s,u,a),∀ a∈ A.\,\,\,∀ u∈ U.\,\,\,∀ s∈ I.\,\,\, (s,u) (s,u,a), where Φ and Ψ are boolean combinations of symbolic polynomial inequalities over the state, parameter and action variables, whose coefficients are either concrete real values or symbolic template variables introduced in Step 1. Our algorithm now solves this system of constraints as follows. First, by using Putinar’s theorem [42] (or Handelman’s theorem [29], if all polynomials are of degree 11), each quantified polynomial entailment is translated into a system of purely existentially quantified polynomial constraints over the symbolic template variables, as well as fresh variables introduced by the Putinar’s theorem. This step is again standard so we omit the details and refer the reader to [12, 16, 5, 30]. The resulting system is then solved by an SMT solver. This translation and reduction to SMT solving can be achieved via an off-the-shelf PolyQEnt tool [14], as we do in our implementation, which also includes details on how boolean combinations of polynomial inequalities are handled before applying Putinar’s theorem. The following theorem establishes soundness of our algorithm. The proof is immediate since the system of constraints collected in Step 2 entails that V is a valid parametric supermartingale certificate with the supporting invariant I, and the reduction to SMT solving in Step 3 is sound. Theorem 0.G.1 (Soundness) Suppose that the verification algorithm returns a parametric supermartingale certificate V and an invariant I. Then M⊧♡ϕ,pM _ φ,p. Appendix 0.H Full Experimental Results Table (including Variance in Runtime) Table 2: Extended version of Table 1 with variance of computation times. Results for different values of the approximation parameter c. Total time represents the total time the tool needed to reach the specified approximation level. Angelic and Demonic SAT time respective represent the mean and standard deviation of the time of those individual SMT queries that returned “SAT.” TO means timeout of the total runtime, which was set to be 900 ss. While reporting the stats of the SMT calls, the remaining cases (total −- (SAT ++ UNSAT ++ inconclusive)) are timeouts (25 ss). @box@std 90 c Total time (ss) Angelic SAT time (ss) Demonic SAT time (ss) # SMT calls and their outcome total-SAT-UNSAT-inconclusive Z3 MathSAT Z3 MathSAT Z3 MathSAT Z3 MathSAT M+M^+: u1=0u_1=0, u2∈[−1,1]u_2∈[-1,1], template unknowns = 9 0.40.4 138.48 45.51 8.16±0.008.16± 0.00 4.92±0.004.92± 0.00 0.19±0.040.19± 0.04 0.35±0.070.35± 0.07 22192-18-22112-17 22-3-0-13 0.30.3 310.30 45.62 6.04±3.016.04± 3.01 2.67±3.192.67± 3.19 0.19±0.040.19± 0.04 0.35±0.070.35± 0.07 52400-20-52320-20 22-4-0-14 0.20.2 TO 60.49 - 2.67±3.192.67± 3.19 - 0.30±0.100.30± 0.10 - 30-5-0-19 0.150.15 TO 90.90 - 1.52±2.271.52± 2.27 - 0.30±0.100.30± 0.10 - 62-7-0-37 0.1250.125 TO TO - - - - - - M×M^×: u1∈[−1,1]u_1∈[-1,1], u2=1u_2=1, template unknowns = 9 0.40.4 57.47 75.38 11.54±0.7311.54± 0.73 13.69±0.6713.69± 0.67 7.11±0.007.11± 0.00 11.75±0.0011.75± 0.00 22-3-8-8 38-4-0-22 0.30.3 59.14 89.75 11.88±0.7811.88± 0.78 10.90±4.7710.90± 4.77 7.11±0.007.11± 0.00 11.75±0.0011.75± 0.00 22-4-8-8 62-7-0-37 0.20.2 73.87 117.58 11.90±0.6411.90± 0.64 8.87±5.458.87± 5.45 7.11±0.007.11± 0.00 8.68±3.308.68± 3.30 34-5-13-10 154-14-0-90 0.150.15 83.27 136.08 9.72±4.929.72± 4.92 9.17±5.149.17± 5.14 6.76±0.496.76± 0.49 8.29±2.638.29± 2.63 46-7-18-14 218-21-0-137 0.1250.125 83.32 153.65 9.72±4.929.72± 4.92 8.07±5.168.07± 5.16 6.76±0.496.76± 0.49 8.22±2.418.22± 2.41 46-7-18-14 298-31-0-209 M+,×M^+,×: u1=0u_1=0, u2∈[−1,1]u_2∈[-1,1], template unknowns = 11 0.40.4 214.01 76.56 1.60±0.751.60± 0.75 0.61±0.320.61± 0.32 0.23±0.050.23± 0.05 0.57±0.470.57± 0.47 1568-28-1183-325 86-10-0-52 0.30.3 TO 91.74 - 0.64±0.290.64± 0.29 - 0.61±0.390.61± 0.39 - 134-15-0-81 0.20.2 TO 122.26 - 1.37±1.151.37± 1.15 - 0.72±0.400.72± 0.40 - 270-27-0-181 0.150.15 TO 144.18 - 2.47±2.202.47± 2.20 - 0.92±0.520.92± 0.52 - 360-42-0-256 0.1250.125 TO 177.40 - 3.43±3.443.43± 3.44 - 2.03±2.062.03± 2.06 - 530-65-0-403