Pith. sign in

REVIEW 3 major objections 5 minor 2 cited by

Scalable control synthesis for stochastic systems via structural IMDP abstractions

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

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

Pith's one-line read The paper claims that stochastic systems with independent per-dimension noise can be verified by storing only marginal probability bounds, cutting memory from quadratic to near-linear in the grid size while tightening reach-avoid…

desk verdict Genuinely new abstraction class with real memory/tightness gains, but the abstract's optimality claim outruns the mathematics; fix that and this is a solid paper. read the letter →

arxiv 2411.11803 v2 pith:ZCQXLG5G submitted 2024-11-18 eess.SY cs.SY

Frederik Baymler Mathiesen , Sofie Haesaert , Luca Laurenti This is my paper · ORCID
classification eess.SYcs.SY
keywords orthogonallydecoupledintervalMarkovdecisionprocessesrobustvalueiterationprobabilisticreach-avoidabstraction-basedcontrollersynthesiscompositionalabstractionstochasticsystemsmarginalprobabilityboundsscalableverification
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 introduces a new class of robust Markov models, orthogonally decoupled Interval Markov Decision Processes (odIMDPs), in which every transition's uncertain probability distribution is a product of independent interval bounds, one per state dimension. The central claim is that for stochastic systems whose noise is independent across dimensions, this product structure makes the abstraction compositional: one stores only the marginal probability bounds of the original system, reducing memory from $2|S|^2|A|$ to $2|S||A|\, n\sqrt[n]{|S|}$ scalar values. The paper further claims that an optimal control strategy for an odIMDP can be computed by a divide-and-conquer sequence of linear programs, and that the strategy, mapped back to the concrete system, yields guaranteed lower and upper bounds on the reach-avoid probability that are never more conservative than the standard IMDP approach. If correct, this makes formal controller synthesis with probabilistic guarantees practical on 6D and 7D systems on ordinary CPU hardware, where existing abstraction-based tools run out of memory or time out.

What carries the argument

The load-bearing object is the odIMDP: a robust Markov decision process whose state space is a product $S=S_1\times\cdots\times S_n$ and whose transition ambiguity set for each source-action pair is $\Gamma_{s,a}=\bigotimes_{i=1}^n \Gamma^i_{s,a}$, an independent interval ambiguity set per dimension. This product form is what lets the abstraction store only the marginal bounds, because the joint transition probability is the product of marginal probabilities. The synthesis algorithm works on the same structure: instead of one large multilinear minimization over all joint distributions, it recursively applies O-maximization one marginal at a time (equation (15)), producing a sound lower bound at linear-programming cost. The correctness argument runs through Theorem 6.3, which lifts the abstract strategy to the concrete system via the region map and transfers the value interval.

What would settle it

Run a high-accuracy Monte Carlo simulation of the 6D linear benchmark under the odIMDP-optimal policy and check whether the empirical reach-avoid probability falls below the paper's reported guaranteed lower bound of 0.958; a violation would contradict Theorem 6.3.

Watch

Extended reading notes

Core claim

The central discovery is that encoding interval uncertainty in product form is not a lossy simplification of the usual IMDP but a strictly tighter model. Theorem 4.3 shows that the product ambiguity set $\Gamma = \bigotimes_{i=1}^n \Gamma^i$ is contained in the interval ambiguity set obtained by multiplying the marginal bounds, so some distributions admitted by the multiplied intervals cannot be factored as products of marginals and are correctly excluded. Theorem 6.1 proves that the recursive divide-and-conquer bound $W^k_{s,a}$ computed one marginal at a time is a sound lower bound on the true pessimistic value iteration, and Proposition 6.2 proves it is at least as large as the bound obtained by the standard IMDP relaxation. Theorem 6.3 then guarantees that any strategy synthesized on the odIMDP, applied to the concrete system through the region map $J(x)=s$, gives an interval $[V^H_\pi(J(x_0)), \hat V^H_\pi(J(x_0))]$ that contains the true reach-avoid probability. On the experimental side, the paper reports that this construction completes 6D and 7D verification tasks with guaranteed lower bounds above 0.95, at memory reductions of roughly 4,700x and 30,000x compared with the parallel IMDP baseline.

Load-bearing premise

The method rests on the assumption that the noise is independent across state dimensions (each Gaussian in the transition mixture has diagonal covariance), so each transition probability factors into a product of per-dimension marginals; if the noise is correlated, the product form and the guarantees collapse.

Editorial extensions

If this is right

  • Memory for the abstraction drops from $2|S|^2|A|$ to $2|S||A|\,n\sqrt[n]{|S|}$ scalars, which is what lets 6D and 7D grids fit in main memory.
  • For the same partition of the state space, the odIMDP lower bound on reach-avoid probability is guaranteed to be at least as high as the bound from an IMDP built by multiplying marginal intervals (Proposition 6.2).
  • The synthesized switching strategy $\pi_x(x,k)=\pi(J(x),k)$ comes with a certificate interval that provably contains the true reach-avoid probability of the original stochastic system (Theorem 6.3).
  • Systems with Gaussian-mixture transition kernels are handled by abstracting each mixture component separately and optimizing over the uncertain component weights, extending the same guarantees to non-Gaussian but independent noise.
  • The reported experiments show the approach is 5--80x faster to abstract on 2D benchmarks and at least two orders of magnitude faster above 3D, while producing tighter lower bounds than both interval-based baselines on most benchmarks.

Reading between the lines

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

  • Editorial inference: the memory savings grow with dimension $n$, so combining odIMDP abstractions with model-order reduction or dimension-wise refinement could plausibly push formal synthesis beyond 7D, where the paper's approach still spends about 13,900 seconds of certification time on the 7D case.
  • Editorial inference: the product ambiguity set is strictly smaller than the multiplied-interval set, which suggests that per-dimension adaptive grids can refine each marginal independently without destroying the product structure; the paper notes that heterogeneous non-grid partitioning is currently incompatible.
  • Editorial inference: the recursive value iteration is exponential in the number of marginals, so for high-dimensional systems with many states per dimension, an alternative that solves the multilinear problem (14) directly, or with a tighter relaxation, would be needed; the paper explicitly leaves exact solution of (14) open.
  • Editorial inference: for systems with correlated noise, one could try a preliminary decorrelating coordinate transform so that the diagonal-covariance assumption holds approximately; the paper restricts itself to the exactly independent case.
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 introduces orthogonally decoupled Interval Markov Decision Processes (odIMDPs), a subclass of robust MDPs whose transition ambiguity sets factor as products of marginal interval ambiguity sets. It shows how Gaussian and Gaussian-mixture stochastic systems with diagonal-covariance noise can be abstracted compositionally to odIMDPs, storing only marginal probability bounds and reducing memory from O(|S|^2|A|) to O(2|S||A| n |S|^{1/n}). The paper proposes a divide-and-conquer linear-programming value iteration for odIMDPs and proves (Theorem 4.3 and Proposition 6.2) that the resulting lower bounds are contained in and at least as tight as the interval bounds obtained by multiplying marginal bounds. It reports experiments on benchmarks up to 7D showing substantial memory and tightness improvements over IMDP/MDP-based tools.

Significance. If the claims hold, the memory-complexity improvement and the tightened ambiguity sets are valuable contributions to abstraction-based verification, because memory is a known bottleneck and the framework scales to 6D/7D systems on standard hardware. The theoretical comparisons (Theorem 4.3, Theorem 6.1, Proposition 6.2) are parameter-free derivations, and the empirical evaluation is extensive. The main reservation is that the advertised 'optimal' synthesis is not actually achieved; the algorithm computes a sound lower bound via a relaxation, which is still useful but is a weaker claim.

major comments (3)
  1. [Abstract and Section 6 (Eqs. (14)-(15))] The abstract claims that 'an optimal control strategy for an odIMDP can be computed by solving a set of linear problems,' but the algorithm presented in Section 6 solves the recursive relaxation in Eq. (15), which is only a lower bound on the exact pessimistic Bellman update in Eq. (14). Theorem 6.1 proves only an inequality, and Section 8 explicitly states that exactly solving Eq. (14) is open. Therefore the strategy maximizing W_{k,s,a} is optimal for the relaxed problem, not for the odIMDP robust value in Eq. (12) or for Problem 2.3 on the concrete system. This overstatement should be corrected in the abstract and in the list of contributions.
  2. [Section 6, Proposition 6.2] The proof of Proposition 6.2 asserts that if each marginal of a distribution lies in the corresponding interval set, then the joint probabilities lie between the products of the marginal bounds. That implication is false for arbitrary joint distributions; it holds for the distribution generated by Eq. (15) only because that distribution is built from conditional factors chosen recursively, not because of marginal containment alone. The proof should be rewritten to argue directly from the recursive construction, e.g., by showing that the sequentially defined minimizing distribution has conditional factors in the marginal sets and therefore satisfies the product bounds. As written, the proof is not valid.
  3. [Section 6.1, Theorem 6.3] The correctness proof is a single sentence referring to [29, Theorem 4], and the computation of the upper bound \hat{V}_\pi^H is not specified for odIMDPs. The text says 'the case min follows similarly,' but it does not give the analogous over-approximation update. Please provide the explicit upper-bound value iteration for odIMDPs and state the precise conditions under which [29, Theorem 4] applies to the relaxed values W_{k,s,a} used in the lower-bound computation.
minor comments (5)
  1. [Throughout] The phrase 'an odIMDPs' is grammatically incorrect; the abbreviation should be used as a singular noun: 'an odIMDP.'
  2. [Section 6] The notation \hat{V}_\pi^H is introduced but never explicitly defined. Please define it as the value obtained by replacing the inner minimization in Eq. (13) with a maximization, and state clearly that it is an upper bound on the satisfaction probability.
  3. [Section 5.2, Eq. (16)] In Eq. (16), the notation W^{k,0}_{r,s,a} should be explicitly defined as the value computed by Eq. (15) for the r-th component odIMDP, so that the mixture extension is unambiguous.
  4. [Table 3] The columns 'Min δ', 'Max δ', and 'Mean δ' should be accompanied by a note under the table defining δ = V_odIMDP - V_other, with positive values indicating that the odIMDP method yields a higher satisfaction probability. The text defines this, but a table note would improve readability.
  5. [Table 4] The memory figures for odIMDPs at large |S| (e.g., 59.5 GB for 360k states) are substantial; a brief remark pointing this out would temper the scalability narrative and inform readers about the trade-off between memory and tightness.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the odIMDP memory bound, ambiguity-set containment, and relaxation lower bound are derived in-paper from the diagonal-covariance assumptions; the sole self-citation is a minor proof template, not a reduction of the central claims.

full rationale

No circular step is exhibited. The odIMDP abstraction stores only the marginal bounds by construction of the product ambiguity set (Section 4), giving the memory count 2|S||A|n n-th root |S|. Theorem 4.3 proves the containment Gamma subset of bar-Gamma by multiplying the nonnegative marginal inequalities, and Proposition 6.2 proves that the divide-and-conquer relaxation W_k,s,a in Eqn. (15) is no more conservative than the product-interval IMDP value; both proofs are self-contained inequalities from the paper's definitions, with no parameter fitted to the quantities being predicted. Theorem 6.1 proves the relaxation is a lower bound on the exact multilinear minimization in Eqn. (14). The abstraction soundness theorem (Theorem 6.3) is sketched by induction 'similarly to [29, Theorem 4]', a preprint by co-author Laurenti; this is a minor self-citation used as a proof template for a standard result, and it does not reduce the paper's novel memory or tightness claims to that citation. The paper's own Section 8 limitation states that 'exactly and efficiently solving the multi-linear problem of Eqn.(14) is still an open problem for which we employed relaxations', which undercuts the abstract's optimality wording; that is a correctness/overclaim concern, not a circularity, because the relaxation bound is still proven to dominate the IMDP bound. The empirical benchmarks are external case studies, and no fitted input is renamed as a prediction.

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

No data-fitted or hand-tuned constants enter the central derivation; partition sizes and benchmark model parameters are user inputs, not calibrated to achieve the reported results. No new physical entities are postulated; odIMDP is a mathematical abstraction model.

assumptions (5)
  • domain assumption The transition kernel of the concrete system is a mixture of Gaussians with diagonal covariance per component (Eqn. (2)), so that conditioned on the component, dimensions are independent.
    Introduced in Section 2, Eqn. (2), and used throughout Section 5 to construct product-form marginal ambiguity sets. If false, the odIMDP abstraction is unsound.
  • domain assumption The mean, covariance, and mixture weight functions are continuous in x over each grid cell, so interval bounds [mu_i, mu_i] and [Sigma_i, Sigma_i] exist (Eqn. (6)).
    Used in Section 5.1 to justify computing marginal probability intervals via optimization over compact intervals.
  • standard math The O-maximization algorithm solves the interval ambiguity set linear program exactly and in O(m log m) time.
    Relied on in Section 6 for each node of the recursion; correctness is taken from Givan et al. [20] and Lahijanian et al. [28].
  • standard math Probability measure existence for system (1) follows from the stochastic kernel via the construction in Bertsekas and Shreve.
    Stated in Section 2 when defining the induced probability measure.
  • domain assumption The region of interest is hyperrectangular and partitioned as a product grid; reach and avoid sets align with the partition or are over-approximated.
    Used in Section 5 to define the grid and in Section 6.1 for the mapping theorem; misalignment is noted but not fully resolved.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Scalable control synthesis for stochastic systems via structural IMDP abstractions." pith.science (2026). https://pith.science/paper/ZCQXLG5G

@misc{pith2026241111803,
  author       = {Pith},
  title        = {Pith review of: Scalable control synthesis for stochastic systems via structural IMDP abstractions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZCQXLG5G}},
  note         = {Machine review of arXiv:2411.11803}
}
read the original abstract

This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. The focus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a class of robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form. We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systems that, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memory complexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of our methods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results.

Figures

Figures reproduced from arXiv: 2411.11803 by the authors.

Figure 1
Figure 1. An example of an odIMDP where, given a source [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. On the left, for the green state, we report two mar [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. An example of the recursive structure for the pro [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Comparing 𝜀 for a varying number of regions on the abstraction (assuming a uniform partition of the state space) and time horizons for both SySCoRe [51] and odIMDPs. Regions per axis 0 50 100 150 Error (log s c ale) 0.001 0.010 0.100 1.000 Car parking Regions per axis …
Figure 5
Figure 5. Figure 5: Mean error and 95% confidence interval, with re￾spect to a uniform distribution of initial conditions, for vari￾ous sizes of partitions for the car parking and building au￾tomation system benchmarks. MDP-based approaches and, as illustrated in [PITH_FULL_IMAGE:figures…
Figure 6
Figure 6. Figure 6: One (pessimistic) Bellman update on the example in [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems

    eess.SY 2025-07 accept novelty 7.0 of 10

    Set-valued MDP abstractions are sound and dominate interval-based abstractions in tightness for any fixed state and disturbance partition, while supporting LP-free control synthesis.

  2. ARCH-COMP25 Category Report: Stochastic Models

    cs.LO 2025-06 conditional novelty 5.0 of 10

    The ARCH-COMP25 stochastic models report introduces new benchmarks and compares six tools for verification and policy synthesis of stochastic systems.

Reference graph

Works this paper leans on

61 extracted references · 47 canonical work pages · cited by 2 Pith papers

  1. [29]

    Luca Laurenti and Morteza Lahijanian. 2023. Unifying Safety Approaches for Sto- chastic Systems: From Barrier Functions to Uncertain Abstractions via Dynamic Programming. arXiv preprint arXiv:2310.01802 (2023)

    arXiv 2023

  2. [1]

    Blom, Nathalie Cauchi, Joanna Delicaris, Arnd Hart- manns, Mahmoud Khaled, Abolfazl Lavaei, Carina Pilch, Anne Remke, and More Authors

    Alessandro Abate, H.A.P. Blom, Nathalie Cauchi, Joanna Delicaris, Arnd Hart- manns, Mahmoud Khaled, Abolfazl Lavaei, Carina Pilch, Anne Remke, and More Authors. 2020. ARCH-COMP20 Category Report: Stochastic Models. In EPiC Series in Computing

    work page 2020

  3. [2]

    Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. 2010. Approximate model checking of stochastic hybrid systems. European Journal of Control 16, 6 (2010), 624–641

    work page 2010

  4. [3]

    Steven Adams, Morteza Lahijanian, and Luca Laurenti. 2022. Formal control synthesis for stochastic neural network dynamic models. IEEE Control Systems Letters 6 (2022), 2858–2863

    work page 2022

  5. [4]

    Steven Adams, Andrea Patane, Morteza Lahijanian, and Luca Laurenti. 2024. Finite Neural Networks as Mixtures of Gaussian Processes: From Provable Error Bounds to Prior Selection. arXiv e-prints (2024), arXiv–2407

    work page 2024

  6. [5]

    Thom Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A Poon- awala, Marielle Stoelinga, and Nils Jansen. 2023. Robust control for dynamical systems with non-gaussian noise via formal abstractions. Journal of Artificial Intelligence Research 76 (2023), 341–391

    work page 2023

  7. [6]

    Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking . The MIT Press

    work page 2008

  8. [7]

    Barto, Richard S

    Andrew G. Barto, Richard S. Sutton, and Charles W. Anderson. 1983. Neu- ronlike adaptive elements that can solve difficult learning control problems. IEEE Transactions on Systems, Man, and Cybernetics SMC-13, 5 (1983), 834–846. https://doi.org/10.1109/TSMC.1983.6313077

    arXiv 1983

Show all 61 references
  1. [8]

    Dimitri P Bertsekas and Steven E Shreve. 2004. Stochastic Optimal Control: the Discrete-time Case. Athena Scientific

    2004

  2. [9]

    Jeff Bezanson, Stefan Karpinski, Viral B Shah, and Alan Edelman. 2012. Julia: A fast dynamic language for technical computing. arXiv preprint arXiv:1209.5145 (2012)

    2012 arXiv

  3. [10]

    El-Kébir Boukas. 2007. Stochastic switching systems: analysis and design . Springer Science & Business Media

    2007

  4. [11]

    Craig Boutilier, Richard Dearden, and Moisés Goldszmidt. 2000. Stochastic dynamic programming with factored representations. Artificial Intelligence 121, 1 (2000), 49–107. https://doi.org/10.1016/S0004-3702(00)00033-3

    2000 doi

  5. [12]

    Ashwin Carvalho, Yiqi Gao, Stéphanie Lefevre, and Francesco Borrelli. 2014. Stochastic predictive control of autonomous vehicles in uncertain environments. In 12th international symposium on advanced vehicle control , Vol. 9

    2014

  6. [13]

    Nathalie Cauchi, Kurt Degiorgio, and Alessandro Abate. 2019. StocHy: automated verification and synthesis of stochastic processes. arXiv:1901.10287 [cs.SY] https://arxiv.org/abs/1901.10287

    2019 arXiv

  7. [14]

    Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, and Luca Cardelli. 2019. Efficiency through uncertainty: Scalable formal synthesis for stochastic hybrid systems. In Proceedings of the 22nd ACM international conference on hybrid systems:...

    2019

  8. [15]

    Krishnendu Chatterjee, Koushik Sen, and Thomas A Henzinger. 2008. Model- checking𝜔-regular properties of interval Markov chains. In Foundations of Software Science and Computational Structures: 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Con...

    2008

  9. [16]

    Steve A. Chien. 2022. Formal Methods for Trusted Space Autonomy: Boon or Bane?. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham, 3–13

    2022

  10. [17]

    Cormen, Charles E

    Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein

  11. [18]

    Delft High Performance Computing Centre. 2024. DelftBlue Supercomputer (Phase 2). https://www.tudelft.nl/dhpc/ark:/44463/DelftBluePhase2

    2024

  12. [19]

    Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar. 2016. Dynamic Bayesian networks for formal verification of structured stochastic processes. Acta Informatica 54, 2 (Dec. 2016), 217–242. https://doi.org/10.1007/ s00236-016-0287-9

    2016

  13. [20]

    Robert Givan, Sonia Leach, and Thomas Dean. 2000. Bounded-parameter Markov decision processes. Artificial Intelligence 122, 1-2 (2000), 71–109

    2000

  14. [21]

    Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns, and Khaled Elbassioni. 2017. Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. In Dependable Software Engineering. Theories, Tools, and Ap- plications, Kim Guldstrand Larsen, Oleg Sokols...

    2017

  15. [22]

    Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. 2021. The probabilistic model checker Storm. International Journal on Software Tools for Technology Transfer 24, 4 (July 2021), 589–610. https://doi.org/10.1007/s10009-021-00633-z

    2021 doi

  16. [23]

    John Jackson, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2020. Towards Data-driven Verification of Unknown Dynamical Systems. In 2nd RSS Workshop on Robust Autonomy: Tools for Safety in Real-World Uncertain Environments (RSS 2020)

    2020

  17. [24]

    John Jackson, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2021. Formal verification of unknown dynamical systems via Gaussian process regression. arXiv preprint arXiv:2201.00655 (2021)

    2021 arXiv

  18. [25]

    Jesse Jiang, Ye Zhao, and Samuel Coogan. 2022. Safe learning for uncertainty- aware planning via interval MDP abstraction. IEEE Control Systems Letters 6 (2022), 2641–2646

    2022

  19. [26]

    Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Veri- fication of probabilistic real-time systems. In Computer Aided Verification: 23rd International Conference. Springer, 585–591

    2011

  20. [27]

    Morteza Lahijanian. 2021. bmdp-tool. https://github.com/aria-systems-group/ bmdp-tool Standalone software

    2021

  21. [28]

    Morteza Lahijanian, Sean B Andersson, and Calin Belta. 2015. Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Automat. Control 60, 8 (2015), 2031–2045

    2015

  22. [30]

    Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Luca Cardelli, and Marta Kwiatkowska. 2020. Formal and efficient synthesis for continuous-time linear stochastic hybrid processes. IEEE Trans. Automat. Control 66, 1 (2020), 17–32

    2020

  23. [31]

    Abolfazl Lavaei, Sadegh Soudjani, Alessandro Abate, and Majid Zamani. 2022. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica 146 (2022), 110617

    2022

  24. [32]

    Abolfazl Lavaei, Sadegh Soudjani, and Majid Zamani. 2021. Compositional abstraction-based synthesis of general MDPs via approximate probabilistic rela- tions. Nonlinear Analysis: Hybrid Systems 39 (2021), 100991. https://doi.org/10. 1016/j.nahs.2020.100991

    2021

  25. [33]

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J Kochenderfer, et al. 2021. Algorithms for verifying deep neural networks. Foundations and Trends in Optimization (2021)

    2021

  26. [34]

    Jun Liu and Necmiye Ozay. 2014. Abstraction, discretization, and robustness in temporal logic control of dynamical systems. In Proceedings of the 17th interna- tional conference on Hybrid systems: computation and control

    2014

  27. [35]

    Ryan Luna, Morteza Lahijanian, Mark Moll, and Lydia E. Kavraki. 2014. Fast stochastic motion planning with optimality guarantees using local policy re- configuration. In 2014 IEEE International Conference on Robotics and Automation (ICRA). 3013–3019. https://doi.org/10.1109/IC...

    2014

  28. [36]

    Calvert, and Luca Laurenti

    Frederik Baymler Mathiesen, Simeon C. Calvert, and Luca Laurenti. 2023. Safety Certification for Stochastic Systems via Neural Barrier Functions. IEEE Control Systems Letters 7 (2023), 973–978. https://doi.org/10.1109/LCSYS.2022.3229865

    2023

  29. [37]

    Frederik Baymler Mathiesen, Morteza Lahijanian, and Luca Laurenti. 2024. Inter- valMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes. arXiv:2401.04068 [eess.SY] https://arxiv.org/abs/2401.04068

    2024 arXiv

  30. [38]

    Calvert, Alessandro Abate, and Luca Laurenti

    Frederik Baymler Mathiesen, Licio Romao, Simeon C. Calvert, Alessandro Abate, and Luca Laurenti. 2023. Inner Approximations of Stochastic Programs for Data-Driven Stochastic Barrier Function Design. In 2023 62nd IEEE Conference on Decision and Control (CDC) . 3073–3080. https:...

    2023

  31. [39]

    Rayan Mazouz, Frederik Baymler Mathiesen, Luca Laurenti, and Morteza Lahija- nian. 2024. Piecewise Stochastic Barrier Functions. arXiv:2404.16986 [cs.RO] https://arxiv.org/abs/2404.16986

    2024 arXiv

  32. [40]

    Rayan Mazouz, Karan Muvvala, Akash Ratheesh Babu, Luca Laurenti, and Morteza Lahijanian. 2022. Safety guarantees for neural network dynamic sys- tems via stochastic barrier functions. Advances in Neural Information Processing Systems 35 (2022), 9672–9686

    2022

  33. [41]

    Vassili Nestoridis, Sebastian Schmutzhard, and Vangelis Stefanopoulos. 2011. Universal series induced by approximate identities and some relevant applications. Journal of Approximation Theory (2011)

    2011

  34. [42]

    Petter Nilsson, Sofie Haesaert, Rohan Thakker, Kyohei Otsu, Cristian Ioan Vasile, Ali-Akbar Agha-Mohammadi, Richard M Murray, and Aaron D Ames. 2018. Toward Specification-Guided Active Mars Exploration for Cooperative Robot Teams.. In Robotics: Science and systems , Vol. 14. 1–9

    2018

  35. [43]

    Andrea Patane, Arno Blaas, Luca Laurenti, Luca Cardelli, Stephen Roberts, and Marta Kwiatkowska. 2022. Adversarial robustness guarantees for gaussian pro- cesses. Journal of Machine Learning Research 23, 146 (2022), 1–55

    2022

  36. [44]

    Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2007. A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates. IEEE Trans. Automat. Control 52, 8 (2007), 1415–1428. https://doi.org/10.1109/TAC. 2007.902736

    2007

  37. [45]

    Robert Reed, Luca Laurenti, and Morteza Lahijanian. 2023. Promises of deep kernel learning for control synthesis. IEEE Control Systems Letters (2023)

    2023

  38. [46]

    Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani, and Majid Zamani. 2021. Data- Driven Safety Verification of Stochastic Systems via Barrier Certificates. IFAC- PapersOnLine 54, 5 (2021), 7–12. https://doi.org/10.1016/j.ifacol.2021.08.466 7th IFAC Conference on Analysis and Desi...

    2021 doi

  39. [47]

    Cesar Santoyo, Maxence Dutreix, and Samuel Coogan. 2021. A barrier function approach to finite-time stochastic system verification and control. Automatica 125 (2021), 109439. https://doi.org/10.1016/j.automatica.2020.109439 HSCC ’25, May 6–9, 2025, Irvine, CA, USA Frederik Bay...

    2021

  40. [48]

    John Skovbekk, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2023. Formal Abstraction of General Stochastic Systems via Noise Partitioning. IEEE Control Systems Letters (2023)

    2023

  41. [49]

    Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. 2014. Aggregation and control of populations of thermostatically controlled loads by formal abstractions. IEEE Transactions on Control Systems Technology 23, 3 (2014), 975–990

    2014

  42. [50]

    Marnix Suilen, Thom Badings, Eline M Bovy, David Parker, and Nils Jansen

  43. [51]

    Birgit Van Huijgevoort, Oliver Schön, Sadegh Soudjani, and Sofie Haesaert. 2023. SySCoRe: Synthesis via stochastic coupling relations. In Proceedings of the 26th ACM international conference on hybrid systems: Computation and control

    2023

  44. [52]

    van Huijgevoort and Sofie Haesaert

    Birgit C. van Huijgevoort and Sofie Haesaert. 2022. Similarity quantification for linear stochastic systems: A coupling compensator approach. Automatica 144 (2022), 110476. https://doi.org/10.1016/j.automatica.2022.110476

    2022

  45. [53]

    B. C. van Huijgevoort, S. Weiland, and S. Haesaert. 2023. Temporal Logic Control of Nonlinear Stochastic Systems Using a Piecewise-Affine Abstraction. IEEE Control Systems Letters (2023). https://doi.org/10.1109/LCSYS.2022.3230765

    2023

  46. [54]

    Vinod, Joseph D

    Abraham P. Vinod, Joseph D. Gleason, and Meeko M. K. Oishi. 2019. SReachTools: A MATLAB Stochastic Reachability Toolbox. , 33 – 38 pages. https://sreachtools. github.io

    2019

  47. [55]

    Christopher Williams and Carl Rasmussen. 1995. Gaussian processes for regres- sion. Advances in neural information processing systems 8 (1995)

    1995

  48. [56]

    Ben Wooding and Abolfazl Lavaei. 2024. IMPaCT: Interval MDP Parallel Construc- tion for Controller Synthesis of Large-Scale STochastic Systems. In Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems

    2024

  49. [57]

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. 2020. Automatic perturbation analysis for scalable certified robustness and beyond. In Proceedings of the 34th International Conference on Neural Informat...

    2020

  50. [58]

    Majid Zamani, Alessandro Abate, and Antoine Girard. 2015. Symbolic models for stochastic switched systems: A discretization and a discretization-free approach. Automatica 55 (2015), 183–196. https://doi.org/10.1016/j.automatica.2015.03.004

    2015 doi

  51. [59]

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient neural network robustness certification with general activation func- tions. In Proceedings of the 32nd International Conference on Neural Information Processing Systems. Scalable control s...

    2018

  52. [2001]

    The MIT Press

    Introduction to Algorithms (2 ed.). The MIT Press

  53. [2024]

    In Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III

    Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet. In Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III . Springer, 126–154

Pith tools

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