Pith. sign in

REVIEW 3 major objections 5 minor 46 references

Robust Probabilistic Model Checking with Continuous Reward Domains

T0 review · 3 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A moment-matched Erlang mixture makes chance constraints on Markov reward distributions decidable with bounded error.

desk verdict The empirical moment-matching approach is worth a look, but the advertised bounded-error guarantee rests on a theorem whose proof only shows weak convergence and is false for atomic reward distributions. read the letter →

arxiv 2502.04530 v1 pith:UZX5VRBD submitted 2025-02-06 cs.AI cs.FLcs.LG

Xiaotong Ji , Hanchun Wang , Antonio Filieri , Ilenia Epifani This is my paper · ORCID
classification cs.AIcs.FLcs.LG MSC 60J1062E1765C40
keywords probabilisticmodelcheckingdistributionalverificationErlangmixturemomentmatchingMarkovrewardprocesschanceconstraintsgeneratingfunctioncontinuousrewards
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to move probabilistic model checking beyond expected values by verifying properties of the entire cumulative-reward distribution of a discrete-time Markov chain. The proposed method matches the first $K$ moments of the true reward distribution to a mixture of Erlang distributions, with the moments computed analytically by differentiating the moment generating function of the reward-to-absorption process. Once the mixture is fitted, chance requirements of the form $\Pr(X \le r^*) \ge \alpha$ are evaluated in closed form from the mixture CDF, and a moment-based inequality can sometimes decide the requirement before the mixture is even fitted. If correct, the method gives engineers a smooth approximation of reward distributions in both continuous and discrete reward spaces, including heavy tails and multimodal behavior that histograms miss.

What carries the argument

The machinery is a finite Erlang mixture $f_{\mathrm{approx}}(x)=\sum_{i=1}^n \omega_i f_{\mathrm{Erlang}}(x; a_i, \lambda)$ with a common rate parameter $\lambda$: a weighted sum of gamma-type densities with integer shapes, a family that can approximate any positive random variable to arbitrary accuracy. The argument runs through three pieces: an MGF first-step analysis that yields the $k$-th moments of cumulative reward to absorption; a truncated Stieltjes moment problem on $[0,+\infty)$ whose objective trades moment discrepancies against differential entropy; and a fixed-shape heuristic ($a_i = 3^i$) that turns the mixed-integer optimization into a non-convex quadratic problem. The CDF of the fitted mixture is a finite sum of Erlang CDF terms, so the chance constraint $\Pr(X \le r^*) \ge \alpha$ is evaluated as a closed-form expression, with a one-sided moment bound available as an early-termination test.

What would settle it

Take a small DTMC whose exact cumulative-reward distribution is computable in closed form, fit the paper's default mixture with $K=3$, $n=3$, and shapes $3^i$, and evaluate $\Pr(X \le r^*)$ at a threshold where the true CDF lies just above $\alpha$ but the fitted CDF lies just below; if such a threshold exists, the practical decision procedure returns the wrong verdict, showing that the finite-$K$ fit is not sound without an instance-specific error certificate.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that the cumulative reward to absorption in a DTMC can be represented, for verification purposes, by a finite mixture of Erlang distributions with a common rate parameter, where the mixture is chosen to match the first $K$ analytically computed moments of the true reward process. The moment generating function of the total reward satisfies a first-step linear system, so the moments are exact without simulation. Theorems IV.1 through IV.3 establish that this representation is dense: any positive reward distribution can be approached arbitrarily closely by Erlang mixtures, and the discretized-markov and Erlangization chain converges in distribution and in moments. The resulting density is the maximum-entropy density among those matching the given moments, and its CDF gives a direct closed-form decision procedure for chance constraints. On discrete-reward benchmarks the paper reports agreement with simulated reward distributions at least as close as histogram-based distributional model checking, and on continuous-reward models it provides a smooth distributional approximation without discretization.

Load-bearing premise

The load-bearing premise is that a finite Erlang mixture fitted to a finite number of moments (in the paper's default, three moments and three components with shapes $3^i$) is close enough to the true reward CDF that the verdict on $\Pr(X \le r^*) \ge \alpha$ is correct, since the proved guarantees are denseness and weak convergence rather than finite-$K$ error bounds.

Editorial extensions

If this is right

  • Chance constraints of the form $\Pr(X \le r^*) \ge \alpha$ can be evaluated directly from the fitted mixture CDF, without simulations, for both continuous and integer reward spaces.
  • A one-sided moment inequality computed from the first $K$ moments can decide some requirements instantly; only when that test is inconclusive does the system need to fit the mixture.
  • Because moments are computed by solving $K$ linear systems of size equal to the state space, the distributional analysis carries polynomial cost in the number of states, independent of the reward range.
  • The method captures skewness, kurtosis, heavy tails, and multiple modalities that expected-value verification ignores, and it does not require binning or discretization of continuous rewards.
  • On discrete-reward benchmarks the paper reports agreement with empirical reward distributions comparable to histogram-based distributional model checking, while on continuous-reward models it handles cases the histogram approach cannot analyze cleanly.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: because the paper's experiments show that accuracy is not monotonic in $K$ and $n$ under the non-convex optimizer, a practical deployment should inspect the fitted CDF's margin against the threshold $r^*$ before trusting borderline chance-constraint verdicts.
  • Editorial inference: the same moment-matched Erlang mixture could serve as a distributional critic in reinforcement learning, replacing histogram and quantile critics with a smooth density that supports analytic gradients with respect to policy parameters.
  • Editorial inference: a testable extension would compare the fitted mixture against exact or simulated CDFs at the specific quantile used by the constraint, rather than only a global worst-case distance, since a small global discrepancy can still hide a local error large enough to flip a verdict.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes a method for distributional probabilistic model checking of DTMCs with continuous or discrete rewards. The method computes the first K moments of the cumulative reward to absorption analytically via a moment-generating-function recurrence, then fits a mixture of Erlang distributions to those moments by solving a non-convex optimization problem with a maximum-entropy regularizer. The fitted CDF is used to decide chance-constrained properties of the form Pr(X ≤ r*) ≥ α, with Cantelli's inequality offered as an early sufficient test. The paper claims a theoretically bounded approximation error, supported by three theorems on discretization of rewards, Erlangization of discrete phase-type distributions, and denseness of Erlang mixtures.

Significance. If the bounded-error claim were correct, the paper would offer a useful alternative to histogram-based distributional model checking, especially for models with continuous rewards, and the analytical moment computation via MGFs (Eq. 2) is a genuine contribution. The Cantelli-based early-termination test is a sound and cheap sufficient condition, and the experimental evaluation covers several nontrivial benchmarks. However, the central theoretical guarantee is not established, and the practical decision procedure inherits no formal soundness from the provided theorems. The contribution is therefore currently an empirically evaluated heuristic, not a method with the advertised bounded-error verification semantics.

major comments (3)
  1. [Theorem IV.1 (Section IV)] The theorem states a uniform sup-norm bound, sup_{r≥0} |F(r) − F_~D(r)| ≤ ε, but the proof only establishes weak convergence: the Markov-inequality argument bounds the probability that the discretized cumulative reward differs by at least ε, and the proof concludes with pointwise convergence at continuity points. Weak convergence does not imply uniform sup-norm convergence. For atomic reward distributions, which are the paper's own discrete examples (e.g., Section II-B assigns each state a constant reward), a δ-shift of the reward lattice moves jump locations, so the sup-norm distance between the original and discretized CDFs cannot be made arbitrarily small. Since an Erlang-mixture CDF is continuous, its sup-norm distance from an atomic CDF is at least half the largest atom mass (e.g., a two-point distribution with masses 0.5 and 0.5). Consequently the 'theoretically bounded error' claimed in the abstract and used in Section III-B for the chance-constraint decision procedure is not delivered by the stated theorems.
  2. [Sections III-A and V-A (Algorithm 1, Table II)] No finite-K, finite-n error bound is derived. The theorems are asymptotic (δ → 0, m → ∞, or denseness as the mixture grows), whereas the practical procedure fixes K=3, n=3 and restricts shapes to the heuristic a_i = 3^i. The paper itself reports in Section V-B that accuracy is not monotone in K and n because the non-convex optimizer provides no global-optimality certificate; Table II shows, for example, D_KS = 0.17 for (K=3,n=4) but 0.26 for (K=3,n=5), and 0.07 for (K=4,n=6) but 0.09 for (K=4,n=9). Therefore the decision Pr(X ≤ r*) ≥ α can be wrong when the fitted CDF error exceeds the property's margin, and the method as deployed has no soundness guarantee. The paper should either supply a finite bound for the practical configuration or explicitly reframe the procedure as a heuristic approximation without the bounded-error claim.
  3. [Theorem IV.1, DPH construction] The construction introduces n_i = k_i − 1 intermediate states for each state with discretized reward k_iδ. For states with zero reward, k_i = 0 and n_i = −1, which is invalid. Since the reward function is only assumed to be non-negative and the paper's own examples include zero rewards (e.g., the landing state with reward 0.0), the DPH discretization proof is incomplete even before the sup-norm issue is considered.
minor comments (5)
  1. [Algorithm 1, lines 1–2] The pseudocode for the moment computation is garbled: f and G are defined with e^{k r(x)} rather than the MGF parameter θ, and the update formula µ_k = r^k f + Σ_{i=0}^k C(k,i) G^{(k−i)} does not match the correct recurrence in Eq. (2). Please align the pseudocode with Eq. (2).
  2. [Section V, experimental settings] The location shift loc = μ − σ can be negative when the standard deviation exceeds the mean, assigning positive probability to negative rewards even though the model rewards are non-negative. This also means the moments of the shifted fitted distribution are not the moments of the original reward variable; the paper should justify the shift or restrict it to loc ≥ 0.
  3. [Theorem IV.2] The coefficient d_{n,n−1} in the moment-expansion formula E[X^n_m] − E[X^n] = E[X^{n−1}] d_{n,n−1}/m + o(1/m) is never defined. Please provide the definition or an explicit reference.
  4. [Section III-B, Eq. (9)] The generalized Cantelli bound is stated for an arbitrary parameter b, but the condition on b (e.g., b ≥ 0 and how b relates to a) is not given. For n > 2 the optimal choice of b is nontrivial; please state the range of validity of the inequality and the intended choice of b.
  5. [Throughout] There are several typos and inconsistencies: 'Chebysehv's' in Section II-B, 'prosed' in Section VI, 'LeadSync' versus 'LeaderSync' in Table I, and an inconsistent use of the subscript in F_{X_i}(x; a_i, λ_i) in Eq. (8) where the mixture components already share a common rate λ. A careful proofreading pass is needed.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the moment-matched Erlang approximation is fitted to model-derived moments, not to the verification answer, and all load-bearing theoretical citations are external.

full rationale

The derivation chain is not circular. The paper's input is a DTMC; it computes the moment-generating function and the first K moments via a linear system (Eq. 2). The Erlang mixture is then fitted to those moments in Algorithm 1, and the chance-constraint decision is evaluated either from the fitted CDF (Eq. 8) or from Cantelli's inequality (Eq. 9). Neither step reduces the verification answer to the fitting target: the moments are model-derived statistics, not the tail probability Pr(X ≤ r*), and matching a finite number of moments does not by construction force the CDF value at an arbitrary threshold r*. The theoretical support cites external results (Tijms Theorem 3.9.1; He et al. Theorem 1) rather than a self-citation chain or an author-imported uniqueness theorem. The shape heuristic a_i = 3^i is an empirical hyperparameter choice evaluated on benchmarks, not a fitted parameter renamed as a prediction. The genuine gap—Theorem IV.1 claims a sup-norm bounded error while its proof establishes only weak convergence, and no finite-K/n error bound is derived—is a correctness and soundness concern, not circularity. The work is self-contained against external simulation benchmarks, so the appropriate circularity score is 0.

Assumptions & free parameters 5 free parameters · 5 assumptions · 0 invented entities

No new physical or formal entities are introduced. The paper's guarantee rests on known denseness results, a maximum-entropy reconstruction heuristic, and assumptions about optimizer quality and simulation fidelity. The finite-K error needed for a sound decision procedure is never quantified.

free parameters (5)
  • Mixture size n and moment count K = defaults K=3, n=3
    Chosen per experiment; no automatic selection. Accuracy and runtime vary with these, and no error certificate ties them to a bound.
  • Entropy weighting gamma = 1
    Set to 1 for all experiments; no sensitivity analysis reported.
  • Shape parameter set a_i = a_i = 3^i for i=1..n
    Heuristic selected by comparing shape sets on the evaluation benchmarks (Section V-B, Table III). Not derived from the model.
  • Rate parameter bounds = lambda in (0.01, 50)
    Bounds chosen 'based on our experience'; they constrain the feasible region of the optimizer.
  • Location shift = mu - sigma per model
    Applied to align Erlang mixtures with the positive support; the shift is computed from the model but is an extra fitting degree of freedom.
assumptions (5)
  • standard math Erlang mixtures are dense in the space of distributions on the positive half-line, so any positive random variable can be approximated arbitrarily well.
    Used in Section III-A and Theorem IV.3, citing Tijms [42].
  • domain assumption The discretized reward DTMC converges to the original in the uniform CDF sense as the reward granularity goes to zero.
    Theorem IV.1 states this uniform bound but the proof establishes only weak convergence; the paper needs the stronger statement to justify 'bounded error'.
  • domain assumption Among all distributions matching the first K moments, the maximum-entropy distribution is the least biased and therefore the best choice for verification.
    Maximum entropy principle, Section III-A, Equation (6); not a mathematical guarantee for finite K.
  • domain assumption The non-convex optimization finds parameters whose moments are close enough to the target moments for the verification to be reliable.
    No optimality certificate is provided; Section V-B notes non-monotonic accuracy due to non-convexity.
  • domain assumption One million simulations accurately represent the ground-truth reward distribution.
    Used as the empirical baseline in Section V; no confidence intervals are reported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Robust Probabilistic Model Checking with Continuous Reward Domains." pith.science (2026). https://pith.science/paper/UZX5VRBD

@misc{pith2026250204530,
  author       = {Pith},
  title        = {Pith review of: Robust Probabilistic Model Checking with Continuous Reward Domains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UZX5VRBD}},
  note         = {Machine review of arXiv:2502.04530}
}
read the original abstract

Probabilistic model checking traditionally verifies properties on the expected value of a measure of interest. This restriction may fail to capture the quality of service of a significant proportion of a system's runs, especially when the probability distribution of the measure of interest is poorly represented by its expected value due to heavy-tail behaviors or multiple modalities. Recent works inspired by distributional reinforcement learning use discrete histograms to approximate integer reward distribution, but they struggle with continuous reward space and present challenges in balancing accuracy and scalability. We propose a novel method for handling both continuous and discrete reward distributions in Discrete Time Markov Chains using moment matching with Erlang mixtures. By analytically deriving higher-order moments through Moment Generating Functions, our method approximates the reward distribution with theoretically bounded error while preserving the statistical properties of the true distribution. This detailed distributional insight enables the formulation and robust model checking of quality properties based on the entire reward distribution function, rather than restricting to its expected value. We include a theoretical foundation ensuring bounded approximation errors, along with an experimental evaluation demonstrating our method's accuracy and scalability in practical model-checking problems.

Figures

Figures reproduced from arXiv: 2502.04530 by the authors.

Figure 1
Figure 1. UAV flight process with states {s0, s1, s2, s3, s4} representing Takeoff, Stable Flight, Maneuvering, Descent, and Landing, respectively. Transition probabilities and rewards are shown on the edges in the form of p/r. The cumulative reward distribution at s0 is illustrated using the expected value (grey), probability histogram estimation (light blue), and true simulated distribution points (green), highlighting the … view at source ↗
Figure 2
Figure 2. Cantelli Bound’s Coarseness in Model Checking [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. PDF and CDF for discrete reward space subjects (figure 1 of 2) [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: PDF and CDF for discrete reward space subjects (figure 2 of 2) [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 5
Figure 5. Figure 5: PDF and CDF for continuous reward space subjects [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Approximated Probabilities Distribution of Financial Market with different number of mixtures [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

  1. [1]

    A YALA, D., J OFRÉ , L., G UTIÉRREZ , L., AND MENA, R. H. On a Dirichlet Process Mixture Representation of Phase-Type Distributions. Bayesian Analysis 17 , 3 (2022), 765 – 790

    work page 2022

  2. [2]

    Probabilistic model checking and non-standard multi-objective reasoning

    B AIER , C., D UBSLAFF , C., K LÜPPELHOLZ , S., D AUM, M., K LEIN , J., MÄRCKER , S., AND WUNDERLICH , S. Probabilistic model checking and non-standard multi-objective reasoning. In International Conference on Fundamental Approaches to Software Engineering (2014), Springer, pp. 1–16

    work page 2014

  3. [3]

    Model Checking Linear- Time Properties of Probabilistic Systems

    B AIER , C., G RÖSSER , M., AND CIESINSKI , F. Model Checking Linear- Time Properties of Probabilistic Systems . Springer Berlin Heidelberg, Berlin, Heidelberg, 2009, pp. 519–570

    work page 2009

  4. [4]

    Principles of Model Checking

    B AIER , C., K ATOEN , J., AND LARSEN , K. Principles of Model Checking. The MIT Press. MIT Press, 2008

    work page 2008

  5. [5]

    G., D ABNEY , W., AND MUNOS , R

    B ELLEMARE , M. G., D ABNEY , W., AND MUNOS , R. A distributional perspective on reinforcement learning. In International conference on machine learning (2017), PMLR, pp. 449–458

    work page 2017

  6. [6]

    B URER , S., AND LETCHFORD , A. N. Non-convex mixed-integer nonlinear programming: A survey. Surveys in Operations Research and Management Science 17 , 2 (2012), 97–106

    work page 2012

  7. [7]

    Self-adaptive software needs quantitative verification at runtime

    C ALINESCU , R., G HEZZI , C., K WIATKOWSKA , M., AND MIRAN - DOLA , R. Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55 , 9 (Sept. 2012), 69—-77

    work page 2012

  8. [8]

    C HAKRAVARTHY , S., AND ALFA, A. S. Matrix-analytic methods in stochastic models. CRC Press, 1996

    work page 1996

Show all 46 references
  1. [9]

    Introduction to stochastic processes

    C INLAR , E. Introduction to stochastic processes . Courier Corporation, 2013

    2013

  2. [10]

    Implicit quantile networks for distributional reinforcement learning

    D ABNEY , W., O STROVSKI , G., S ILVER , D., AND MUNOS , R. Implicit quantile networks for distributional reinforcement learning. In Interna- tional conference on machine learning (2018), PMLR, pp. 1096–1105

    2018

  3. [11]

    Distributional reinforcement learning with quantile regression

    D ABNEY , W., R OWLAND , M., B ELLEMARE , M., AND MUNOS , R. Distributional reinforcement learning with quantile regression. In Proceedings of the AAAI conference on artificial intelligence (2018), vol. 32

    2018

  4. [12]

    Distributional proba- bilistic model checking

    E LSAYED -ALY, I., P ARKER , D., AND FENG , L. Distributional proba- bilistic model checking. In NASA Formal Methods Symposium (2024), Springer, pp. 57–75

    2024

  5. [13]

    E RLANG , A. K. The theory of probabilities and telephone conversations. Nyt. Tidsskr. Mat. Ser. B 20 (1909), 33–39

    1909

  6. [14]

    S., M AJUMDAR , R., P RABHU , V

    F ARAHANI , S. S., M AJUMDAR , R., P RABHU , V. S., AND SOUDJANI , S. E. Z. Shrinking horizon model predictive control with chance- constrained signal temporal logic specifications. In 2017 American Control Conference (ACC) (2017), pp. 1740–1746

    2017

  7. [15]

    Supporting self- adaptation via quantitative verification and sensitivity analysis at run time

    F ILIERI , A., T AMBURRELLI , G., AND GHEZZI , C. Supporting self- adaptation via quantitative verification and sensitivity analysis at run time. IEEE Transactions on Software Engineering 42 , 1 (2016), 75–99

    2016

  8. [16]

    Quantitative multi-objective verification for probabilistic sys- tems

    F OREJT , V., K WIATKOWSKA , M., N ORMAN , G., P ARKER , D., AND QU, H. Quantitative multi-objective verification for probabilistic sys- tems. In Tools and Algorithms for the Construction and Analysis of Systems (Berlin, Heidelberg, 2011), P. A. Abdulla and K. R. M. Leino, Eds...

    2011

  9. [17]

    Con- strained approximate maximum entropy learning of markov random fields

    G ANAPATHI , V., V ICKREY , D., D UCHI , J., AND KOLLER , D. Con- strained approximate maximum entropy learning of markov random fields. arXiv preprint arXiv:1206.3257 (2012)

    2012 arXiv

  10. [18]

    The truncated stieltjes moment problem solved by using kernel density functions

    G AVRILIADIS , P., AND ATHANASSOULIS , G. The truncated stieltjes moment problem solved by using kernel density functions. Journal of Computational and Applied Mathematics 236 , 17 (2012), 4193–4213

    2012

  11. [19]

    G HOSH , B. K. Probability inequalities related to markov’s theorem. The American Statistician 56 , 3 (2002), 186–190

    2002

  12. [20]

    G ROSS , D., J ANSEN , N., J UNGES , S., AND PÉREZ , G. A. Cool-mc: a comprehensive tool for reinforcement learning and model checking. In International Symposium on Dependable Software Engineering: Theo- ries, Tools, and Applications (2022), Springer, pp. 41–49

    2022

  13. [21]

    Gurobi Optimizer Reference Manual, 2024

    G UROBI OPTIMIZATION , LLC. Gurobi Optimizer Reference Manual, 2024

    2024

  14. [22]

    R., M ILLMAN , K

    H ARRIS , C. R., M ILLMAN , K. J., V AN DER WALT, S. J., G OMMERS , R., V IRTANEN , P., C OURNAPEAU , D., W IESER , E., T AYLOR , J., BERG , S., S MITH , N. J., ET AL . Array programming with numpy. Nature 585, 7825 (2020), 357–362

    2020

  15. [23]

    Continuous approximations of discrete phase-type distributions and their applications to reliability models

    H E, Q.-M., L IU, B., AND WU, H. Continuous approximations of discrete phase-type distributions and their applications to reliability models. Performance Evaluation 154 (2022), 102284

    2022

  16. [24]

    Approximate probabilistic model checking

    H ÉRAULT, T., L ASSAIGNE , R., M AGNIETTE , F., AND PEYRONNET , S. Approximate probabilistic model checking. In International Workshop on Verification, Model Checking, and Abstract Interpretation (2004), Springer, pp. 73–84

    2004

  17. [25]

    Probabilistic self-stabilization

    H ERMAN , T. Probabilistic self-stabilization. Information Processing Letters 35, 2 (1990), 63–67

    1990

  18. [26]

    A kolmogorov-smirnov type statistic with application to test for nonlinearity in time series

    H ONG -ZHI, A., AND BING , C. A kolmogorov-smirnov type statistic with application to test for nonlinearity in time series. International Statistical Review/Revue Internationale de Statistique (1991), 287–307

    1991

  19. [27]

    Techniques for the reconstruction of a distribution from a finite number of its moments

    J OHN , V., A NGELOV , I., Ö NCÜL , A., AND THÉVENIN , D. Techniques for the reconstruction of a distribution from a finite number of its moments. Chemical Engineering Science 62 , 11 (2007), 2890–2904

    2007

  20. [28]

    A., AND TAAFFE , M

    J OHNSON , M. A., AND TAAFFE , M. R. Matching moments to phase dis- tributions: Mixtures of erlang distributions of common order. Stochastic Models 5, 4 (1989), 711–743

    1989

  21. [29]

    The probabilistic model checking landscape

    K ATOEN , J.-P. The probabilistic model checking landscape. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (New York, NY , USA, 2016), LICS ’16, Association for Computing Machinery, pp. 31––45

    2016

  22. [30]

    E., AND PAPPAS , G

    K RESS -GAZIT , H., F AINEKOS , G. E., AND PAPPAS , G. J. Temporal- logic-based reactive mission and motion planning. IEEE Transactions on Robotics 25 , 6 (2009), 1370–1381

    2009

  23. [31]

    Prism: Prob- abilistic symbolic model checker

    K WIATKOWSKA , M., N ORMAN , G., AND PARKER , D. Prism: Prob- abilistic symbolic model checker. In International Conference on Modelling Techniques and Tools for Computer Performance Evaluation (2002), Springer, pp. 200–204

    2002

  24. [32]

    Probabilistic model checking and autonomy

    K WIATKOWSKA , M., N ORMAN , G., AND PARKER , D. Probabilistic model checking and autonomy. Annual Review of Control, Robotics, and Autonomous Systems 5 (2022), 385–410

    2022

  25. [33]

    C., AND LIN, X

    L EE, S. C., AND LIN, X. S. Modeling dependent risks with multivariate erlang mixtures. ASTIN Bulletin 42 , 1 (2012), 153—-180

    2012

  26. [34]

    M ASSEY JR, F. J. The kolmogorov-smirnov test for goodness of fit. Journal of the American statistical Association 46 , 253 (1951), 68–78

    1951

  27. [35]

    Results on the quantitative µ-calculus qm µ

    M CIVER , A., AND MORGAN , C. Results on the quantitative µ-calculus qm µ. ACM Transactions on Computational Logic (TOCL) 8 , 1 (2007), 3–es

    2007

  28. [36]

    R., AND PAPANICOLAOU , N

    M EAD , L. R., AND PAPANICOLAOU , N. Maximum entropy in the problem of moments. Journal of Mathematical Physics 25 , 8 (1984), 2404–2417

    1984

  29. [37]

    M., AND HAKOBYAN , A

    M NATSAKANOV , R. M., AND HAKOBYAN , A. S. Recovery of distribu- tions via moments. Lecture Notes-Monograph Series (2009), 252–265

    2009

  30. [38]

    Monte carlo based statistical model checking of cyber-physical systems: A review

    P APPAGALLO , A., M ASSINI , A., AND TRONCI , E. Monte carlo based statistical model checking of cyber-physical systems: A review. Infor- mation 11, 12 (2020), 588

    2020

  31. [39]

    P UTERMAN , M. L. Markov decision processes. Handbooks in opera- tions research and management science 2 (1990), 331–434

    1990

  32. [40]

    G., Y ANG , M

    S AW, J. G., Y ANG , M. C., AND MO, T. C. Chebyshev inequality with estimated mean and variance. The American Statistician 38 , 2 (1984), 130–132

    1984

  33. [41]

    Meda: mixed erlang distributions as phase-type representations of empirical distribution functions

    S CHMICKLER , L. Meda: mixed erlang distributions as phase-type representations of empirical distribution functions. Communications in Statistics. Stochastic Models 8 , 1 (1992), 131–156

    1992

  34. [42]

    Stochastic Models: An Algorithmic Approach

    T IJMS , H. Stochastic Models: An Algorithmic Approach . Wiley Series in Probability and Statistics - Applied Probability and Statistics Section. Wiley, 1994

    1994

  35. [43]

    Phase-type distributions & mixtures of erlangs

    V ERBELEN , R. Phase-type distributions & mixtures of erlangs. A study of theoretical concepts, calibration techniques & actuarial applications university of leuven (2013)

    2013

  36. [44]

    Fitting mixtures of erlangs to censored and truncated data using the em algorithm

    V ERBELEN , R., G ONG , L., A NTONIO , K., B ADESCU , A., AND LIN, S. Fitting mixtures of erlangs to censored and truncated data using the em algorithm. ASTIN Bulletin 45 , 3 (2015), 729—-758

    2015

  37. [45]

    E., H ABERLAND , M., R EDDY, T., C OURNAPEAU , D., B UROVSKI , E., P ETERSON , P., WECKESSER , W., B RIGHT , J., ET AL

    V IRTANEN , P., G OMMERS , R., O LIPHANT , T. E., H ABERLAND , M., R EDDY, T., C OURNAPEAU , D., B UROVSKI , E., P ETERSON , P., WECKESSER , W., B RIGHT , J., ET AL . Scipy 1.0: fundamental algo- rithms for scientific computing in python. Nature methods 17, 3 (2020), 261–272

    2020

  38. [46]

    U., DE LA IGLESIA , D

    W EYNS , D., I FTIKHAR , M. U., DE LA IGLESIA , D. G., AND AHMAD , T. A survey of formal methods in self-adaptive systems. In Proceedings of the Fifth International C* Conference on Computer Science and Soft- ware Engineering (New York, NY , USA, 2012), C3S2E ’12, Association ...

    2012

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.