Supermartingale Certificates for Parametric MDPs

• Classical MDP methods assume exactly known transition probabilities, while pMDPs allow probabilities to depend on real-valued parameters that may be unknown or only partially known.Such models can express dependencies including multivariate polynomial transition probabilities.Source: §1 · p. 1
• Most existing pMDP methods are restricted to finite state and action spaces, while the known approach for infinite or continuous spaces is limited to bounded-horizon properties.Infinite-space models occur in applications such as stochastic control, robotics, and probabilistic programs with unbounded or continuous states.Source: §1 · pp. 2–3
• Parameter flattening embeds parameter valuations in the state space, yielding a semantically equivalent non-parametric MDP for general measurable state and action spaces.The transformation creates an opportunity to apply non-parametric MDP verification techniques to pMDPs.Source: §1 · p. 2
• Parametric supermartingale certificates extend certificates used in non-parametric systems by instantiating them in the parameter-flattened MDP.The paper presents them as a general framework for pMDPs with general measurable state and action spaces.Source: §1 · p. 2
• The algorithms automate verification and approximate synthesis for polynomial pMDPs using template-based certificate synthesis and abstraction–refinement.They also produce closed-form parametric strategies that can be instantiated by substituting a parameter valuation.Source: §1 · p. 2
• A prototype implements the proposed algorithms and is evaluated on infinite-state pMDP benchmarks modeling continuous random walks.Source: §1 · p. 2

• A measurable MDP has measurable state and action spaces, a stochastic kernel assigning transition distributions, and a set of initial states.Source: §2 · p. 3
• The paper restricts MDP strategies to measurable deterministic memoryless maps from states to actions; a strategy and initial state define a probability space over paths.Source: §2 · p. 4
• A pMDP has a Borel-measurable set of parameter valuations and a measurable parametric stochastic kernel, with each valuation inducing a concrete MDP.Source: §2 · p. 4
• The running example is a pMDP with real-valued state S=[−2,150], action A=[0,0.6], and two parameters in [−1,1]^2; when 0≤s≤100, its kernel is s+a+u1+u2·Uniform[−0.75,0.25], otherwise s.Its initial states are [2,3].Source: §2 · p. 5
• A parametric strategy maps each parameter valuation and state to an action, inducing a strategy in the corresponding concrete MDP; specifications are measurable sets of paths.Examples include reaching a measurable state set and remaining in one at every step.Source: §2 · p. 5

• Angelic satisfaction requires a parametric strategy that meets the specification threshold across parameter valuations, whereas demonic satisfaction requires the threshold for all such strategies.Source: §3 · p. 6
• Verification proves threshold satisfaction, while synthesis partitions the parameter set into regions satisfying the specification and its complement under the opposite satisfaction mode.Source: §3 · p. 6
• Approximate synthesis requires disjoint satisfying and violating regions whose combined Lebesgue measure covers at least 1 − c of the parameter set.Source: §3 · p. 7
• The definitions quantify over measurable parametric strategies; this ensures the induced strategies are measurable and agrees with finite-state pMDP definitions in the finite-state setting.Source: §3 · pp. 7–8
• The paper restricts attention to deterministic memoryless strategies, which suffice for reachability in MDPs but not for general ω-regular specifications.The stated sufficiency in pMDPs follows when it holds in the corresponding non-parametric MDPs.Source: §3 · p. 8

4 Parameter Flattening

• Each flattened state pairs an original state with a parameter valuation, which remains unchanged while the successor state is sampled using the original stochastic kernel.The flattened action space matches the original, and its initial states pair original initial states with parameter valuations.Source: §4 · pp. 8–9
• Flattening preserves satisfaction: a pMDP satisfies a specification at a probability threshold if and only if its flattened MDP satisfies the flattened specification at that threshold.The equivalence holds for angelic and demonic satisfaction.Source: §4 · p. 9
• Because satisfaction can be proved in the flattened MDP, non-parametric supermartingale certificates can be instantiated there to reason about pMDPs.The transformation is described as applicable to general measurable state and action spaces.Source: §4 · pp. 8–9

5 Parametric Supermartingale Certificates

• Parametric certificates instantiate non-parametric supermartingale certificates in the parameter-flattened state space, with parameter quantification and angelic or demonic satisfaction requiring careful treatment.The framework is presented as generalizing a broad class of certificates, including certificates for ω-regular specifications; conditions are checked over an invariant containing all reachable states.Source: §5 · p. 10

5.1 Parametric Supermartingales for Safety Specifications

• For safety thresholds p ∈ [0, 1), parametric stochastic barrier functions provide a sound proof rule when a suitable certificate and invariant exist.The paper’s example gives a demonic safety proof for threshold 0.1 on parameter region [−0.25, −0.125] × {1}.Source: §5.1 · p. 12
• Parametric stochastic barrier functions are not defined for probability-1 safety; the paper suggests strengthening almost-sure safety to sure safety and using classical barrier functions.The defining conditions contain 1/(1−p), which is undefined at p = 1.Source: §5.1 · p. 12

5.2 Parametric Supermartingales for Reachability Specifications

• For reachability thresholds p ∈ [0, 1), parametric reach-avoid supermartingales provide a sound proof rule when a suitable certificate and invariant exist.The paper presents reachability certificates; an extension to reach-avoidance can add a safety condition analogous to the safety-certificate condition.Source: §5.2 · pp. 12, 14

6 Automated Parameter Verification and Synthesis

• The algorithms address verification and approximate synthesis and also produce a closed-form parametric strategy witnessing satisfaction.The authors describe succinct strategy construction as open in earlier work on finite- and infinite-state pMDPs.Source: §6 · p. 14

6.1 Verification Algorithm

• The verification algorithm is restricted to polynomial pMDPs and certificates representable in polynomial real arithmetic, with known first D moments for the random-variable distributions.The stochastic kernel is represented by a polynomial successor-state equation using independent random variables.Source: §6.1 · p. 15
• Verification uses templates for certificates and invariants, reduces their conditions to polynomial constraints, and solves them with an SMT solver.The framework covers certificates whose defining conditions are bounds or expectations; in the demonic case it replaces strategy quantification with quantification over actions, preserving soundness.Source: §6.1 · pp. 14–16

6.2 Synthesis Algorithm

• Synthesis partitions parameter space into verified satisfaction and violation regions, splitting unexplained boxes until their combined volume covers at least 1−c of U.It assumes bounded U, a supplied covering box, and access to a procedure that computes or lower-bounds the volume of each box’s intersection with U.Source: §6.2 · pp. 16–17

• MathSAT5 significantly outperforms Z3 on M+ and M+,×, while Z3 leads on M×.Source: §7 · p. 18
• Experiments vary approximation parameter c across additive, multiplicative, and combined variants; verification queries have 25 s timeouts and total runtime is capped at 900 s.Source: §7 · p. 18, Table 1 · p. 18
• The refinement algorithm solves approximate synthesis with reasonable accuracy, using the finest cells near the frontier between parameter regions.Source: §7 · p. 19, Figure 1 · p. 19

• The framework uses parametric supermartingale certificates for automated verification and approximate synthesis in infinite-state pMDPs.Source: §8 · p. 19
• Combining parameter flattening with template-based synthesis enables formal reasoning about rich specifications under parametric uncertainty.Source: §8 · p. 19
• Future work targets quantitative properties and heuristics to mitigate current scalability bottlenecks.Source: §8 · p. 19

• The path map Φ adds the parameter valuation to each state, and its inverse removes those valuations.Source: A Proof of Proposition 1 · p. 26
• The induced map Φ_F gives a bijection between measurable path sets in the two MDPs.Source: A Proof of Proposition 1 · p. 26
• The proof establishes measure preservation by showing that the two probability measures agree on cylinder sets generating the path σ-algebra.Source: A Proof of Proposition 1 · p. 27
• Because the mapped specification is the corresponding event in the flattened MDP, its probability is preserved.Source: A Proof of Proposition 1 · p. 27

• Angelic satisfaction requires a strategy that meets the probability bound for every parameter valuation and initial state.Source: B Proof of Theorem 1 · p. 27
• In the flattened MDP, parameter valuations are part of the state, and corresponding strategies and probabilities transfer the angelic condition.Source: B Proof of Theorem 1 · p. 28
• Demonic satisfaction quantifies over every strategy, parameter valuation, and initial state.Source: B Proof of Theorem 1 · p. 28
• Demonic satisfaction holds in the original MDP if and only if it holds in the flattened MDP.Source: B Proof of Theorem 1 · p. 28

C Proof of Theorem 2

• A parametric SBF becomes an SBF for X × U with invariant I × U in the flattened model, using an ensuring strategy for angelic satisfaction and any strategy for demonic satisfaction.The certificate conditions yield these ordinary SBFs for the respective induced Markov chains.Source: C Proof of Theorem 2 · p. 28
• SBF soundness gives safety probability at least p for every initial state in the flattened model, for the strategy used in each satisfaction mode.For demonic satisfaction, the argument applies to an arbitrary flattened strategy.Source: C Proof of Theorem 2 · pp. 28–29
• The parameter-flattening theorem transfers the safety result from X × U back to X in the original pMDP for both satisfaction modes.The proof concludes the corresponding angelic or demonic safety claim.Source: C Proof of Theorem 2 · pp. 28–29

D Proof of Theorem 3

• A parametric RASM proves reachability with probability at least p by inducing a RASM on the flattened model, applying ordinary RASM soundness, and transferring the result back to the pMDP.The proof handles angelic satisfaction using an ensuring strategy and demonic satisfaction by considering an arbitrary strategy.Source: D Proof of Theorem 3 · p. 29

E Parametric Supermartingales for Probability 1 Reachability

• A parametric RSM is a measurable function on S × U, and its soundness theorem establishes probability-1 reachability for either angelic or demonic satisfaction.The proof uses parameter flattening to apply ordinary RSM soundness to the induced Markov chain.Source: E Parametric Supermartingales for… · pp. 30–31

F Parametric Generalization of Other Supermartingale Certificates

• Certificate conditions that are bound or expectation conditions can be generalized to parametric MDPs, extending the framework beyond RSMs, SBFs, and RASMs.The text also identifies repulsing, Streett, and limit-deterministic Büchi supermartingales as examples whose conditions have these forms.Source: F Parametric Generalization of Other… · pp. 31–32

G Verification Algorithm

• The verification algorithm fixes polynomial templates, collects constraints encoding certificate validity and an inductive invariant, then solves the resulting polynomial entailments using theorem-based reduction and an SMT solver.For demonic satisfaction, replacing universal strategy quantification with universal actions slightly strengthens the certificate conditions and preserves soundness.Source: G Verification Algorithm · pp. 33–34

H Full Experimental Results Table (including Variance in Runtime)

• Total time records how long the tool takes to reach the specified approximation level, with the table reporting results for different values of c.The total-runtime timeout is 900 s.Source: Table 2 · p. 35
• Angelic and demonic SAT times report the mean and standard deviation for individual SMT queries that returned SAT.Source: Table 2 · p. 35
• Remaining SMT-call cases after SAT, UNSAT, and inconclusive results are timeouts of 25 s each.Source: Table 2 · p. 35