Pith. sign in

REVIEW 2 major objections 5 minor 29 references

Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems

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

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

Pith's one-line read For a fixed partition of the state and disturbance spaces, set-valued MDPs are sound, linear-programming-free abstractions that yield reach-avoid guarantees at least as tight as any interval-based abstraction, including multi-interval…

desk verdict A genuinely useful abstraction paper with a clean containment proof and an LP-free synthesis result, but the headline tightness theorem has an unproven upper-bound step that needs fixing before the paper is publishable. read the letter →

arxiv 2507.02213 v1 pith:63XIQJ5J submitted 2025-07-03 eess.SY cs.SY

Ibon Gracia , Morteza Lahijanian This is my paper · ORCID
classification eess.SYcs.SY
keywords stochasticsystemsfiniteabstractionintervalMDPsset-valuedmulti-intervalrobustdynamicprogrammingreach-avoidsynthesisuncertain
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 show that standard interval-valued abstractions of stochastic systems, which bound transition probabilities region by region, are unnecessarily loose, and that a different accounting of uncertainty is both tighter and cheaper. It introduces multi-interval MDPs, which bound probabilities of landing in overlapping clusters of regions, and set-valued MDPs, which give each cluster a fixed transition probability equal to the probability of the corresponding noise cell and let an adversary place the successor inside the cluster. The central claim is that, for any fixed partitions of state and disturbance spaces, the set-valued abstraction is sound and dominates every interval-based abstraction in tightness, while its synthesis recursion avoids linear programming. If correct, this gives a practical way to compute reach-avoid controllers with formal guarantees for nonlinear, non-Gaussian stochastic systems without trading tightness for tractability.

What carries the argument

The load-bearing object is the cluster transition q_{s,a,c} := {s' in S : s' intersect Reach(s,a,c) is nonempty}, paired with the fixed transition probability P_W(c) into that cluster and an adversarial conditional distribution over its states. This object carries the argument: the fixed mass per cluster is exactly the noise cell probability, which interval models only bound, and the adversarial conditional distribution inside the cluster is what lets robust dynamic programming terminate at each step by evaluating the minimum current value over the states of the cluster. It also determines the SMDP's space complexity O(N_q |S||A||C|) and its linear-programming-free synthesis algorithm.

What would settle it

Take any concrete system with a fixed partition S and C, build the SMDP and an MI-MDP with the same informed clusters, and compute the ambiguity sets: a single distribution admitted by the SMDP but forbidden by the MI-MDP would refute Theorem 2, and a single state whose SMDP reach-avoid interval is not contained in the MI-MDP interval would refute Theorem 4. The paper's own Example 3 shows the expected direction; the check is to search for the reverse inclusion anywhere.

Watch

Extended reading notes

Core claim

The paper establishes a dominance order among abstraction classes. Given the same partition S of the state space and C of the disturbance space, the SMDP abstraction's ambiguity set is a subset of the MI-MDP's ambiguity set for every choice of MI-MDP clusters (Theorem 2), which makes the SMDP sound (Theorem 1) and ensures that the robust reach-avoid guarantee interval computed on the SMDP is contained in the interval computed on the MI-MDP (Theorem 4). Because IMDPs and 2I-MDPs are special cases of MI-MDPs, the SMDP is at least as tight as all of them. The mechanism is that each noise cell c carries a fixed probability P_W(c) of driving the next state into the cluster of regions that intersect Reach(s,a,c), and only the conditional placement inside that cluster is adversarial; interval models instead constrain sums of per-region probabilities by counting reachable-set intersections, which leaves spurious distributions that the SMDP excludes. The paper also proves that this structure reduces the inner robust dynamic programming minimization to a finite search over each cluster, eliminating linear programming.

Load-bearing premise

The whole construction assumes a one-step reachable-set oracle for each region, action, and noise cell that covers every possible next state; if that oracle is unsound, the abstraction is unsound, and if it is too coarse, the tightness advantage shrinks.

Editorial extensions

If this is right

  • Reach-avoid guarantees computed on an SMDP are never looser than those from IMDP, 2I-MDP, or MI-MDP abstractions built from the same partitions, regardless of how the MI-MDP clusters are chosen.
  • Synthesis on SMDPs avoids linear programming: each robust value-iteration step reduces to picking the minimum current value over each cluster, so per-iteration cost is O(|S||A| N_q |C|) finite searches.
  • Because clusters are defined automatically by intersection with reachable sets, the user no longer has to hand-tune cluster structure; the noise partition C alone determines the abstraction.
  • In benchmarks, SMDPs give the tightest satisfaction bounds and the shortest abstraction times across 2D and 3D unicycle and multi-room temperature examples, with synthesis times that become competitive as partitions are refined.
  • The resulting controller is provably correct for the original system: the reach-avoid probability of the closed loop lies inside the interval computed on the abstraction (Theorem 3).

Reading between the lines

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

  • The same cluster semantics could absorb data-driven estimates of P_W: replacing the true cell probabilities with confidence intervals on P_W(c) would yield a sound SMDP abstraction from samples, an extension the paper lists as future work.
  • Because refining C tightens SMDP guarantees without changing the state partition, one could derive convergence rates for the guarantee interval as the noise partition is refined; the 3D unicycle benchmark shows a monotone trend but no rate is claimed.
  • The dominance proof suggests that the many interval constraints of IMDPs and 2I-MDPs are redundant once fixed cluster probabilities are enforced; a practical follow-up is an algorithm that synthesizes the coarsest C achieving a target tightness, avoiding the hand-tuning of partitions.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 5 minor

Summary. The paper proposes two finite abstractions for continuous-state stochastic control systems: multi-interval MDPs (MI-MDPs), which generalize IMDPs and 2I-MDPs by allowing multiple, possibly overlapping clusters of successor states, and set-valued MDPs (SMDPs), in which the probability of entering a disturbance-cell-induced cluster is fixed but the conditional distribution inside the cluster is adversarial. The authors prove soundness of both abstractions, prove that the SMDP ambiguity set is contained in any MI-MDP ambiguity set for the same partitions, give an LP-based synthesis algorithm for MI-MDPs and a finite-search algorithm for SMDPs, and validate the approach on three benchmarks.

Significance. The paper contains several correct and useful components: Theorem 1 establishes soundness of the SMDP abstraction, Theorem 2 proves the ambiguity-set containment Γ_SMDP ⊆ Γ_MIMDP for arbitrary MI-MDP clusters, and Theorem 5 correctly reduces the inner minimization in robust dynamic programming for SMDPs to finite minimum searches over clusters. These contributions, together with the extensive benchmark study, make the framework practically appealing. However, the central advertised dominance result, Theorem 4, is false as stated: the proof only establishes lower-bound monotonicity, and the upper-bound containment does not follow from ambiguity-set containment when the robust strategy is re-optimized. The paper's headline claim that SMDP guarantee intervals are contained in MI-MDP guarantee intervals therefore needs substantial revision.

major comments (2)
  1. [Section 6.1, Theorem 4] The upper-bound containment in Theorem 4 is not a consequence of Γ_SMDP ⊆ Γ_MIMDP and is false as stated. The upper bound p̄ is computed in [14, Eq. 6.5] as the optimistic value under the robust strategy σ*, and σ* is an argmax of the lower-bound Bellman operator. When the argmax differs between the two models, monotonicity of the max over Γ is lost. A concrete counterexample with states {T, I, D}, where T is the target and the other states have value 0, gives induced marginal ambiguity sets for the target probability: Γ_SMDP(a)={0.8}, Γ_SMDP(b)={0.755}, Γ_MIMDP(a)=[0.7,0.9], Γ_MIMDP(b)=[0.75,0.76]. Then p_SMDP=0.8 with σ*_SMDP=a, while p_MIMDP=0.75 with σ*_MIMDP=b; consequently p̄_SMDP=0.8 and p̄_MIMDP=0.76, so [0.8,0.8] ⊄ [0.75,0.76]. These ambiguity sets are realizable within Definitions 5 and 6: for action a, cells of total weight 0.8 reach only T, a cell of weight 0.1 reaches I∪D, and the remaining mass reaches D; for action b the analogous weights are 0.755 and 0.005, with cluster sets {T, I} and {I}. The proof's sentence 'The same reasoning shows...' is therefore invalid; the maximum over Γ is monotone only when the action is fixed.
  2. [Abstract, Introduction, Section 8] The advertised claim that SMDPs are 'at least as tight' as MI-MDPs rests entirely on the interval containment of Theorem 4. Since the upper bound is not monotone under ambiguity-set containment when strategies are re-optimized, the main theoretical contribution is overstated. What the first part of the proof of Theorem 4 actually establishes is only the lower-bound dominance p_SMDP ≥ p_MIMDP. The authors should either restrict all tightness claims to lower bounds, or change the definition of the upper bound to a quantity that is monotone in the ambiguity set, such as the global optimistic value max_σ max_ξ, and then check that Theorem 3 and the reported p̄ values remain valid. Table 1 and the eavg metric should be revisited, because they currently mix the correct lower-bound improvement with the unsupported upper-bound containment.
minor comments (5)
  1. [Definition 5] The text uses 'MI-IMDP' in Definition 5; this should be 'MI-MDP' for consistency with the rest of the paper.
  2. [Definition 6] The line defining ΓSMDP_s,a uses 'sunsafe' while the rest of the paper uses 'savoid'; the notation should be unified.
  3. [Figure 1 caption] The caption refers to '1d' twice; the last sentence should refer to Figure 1e for the SMDP abstraction.
  4. [Section 5.2 and Section 6.2] The complexity expressions are missing parentheses: Proposition 4 states 'Op|S||A|Nq|C|q' instead of O(|S||A|N_q|C|), and the ratio in Section 6.2 is similarly garbled.
  5. [Lemma 1] Lemma 1 is imported from [27] without proof, and the measurability assumption in footnote 3 is stated only in passing; the assumption should be made explicit in the lemma statement.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular reduction: SMDP tightness is proven from reachability plus set inclusion; the only concerns are minor self-citations and a non-circular proof gap in the upper-bound half of Theorem 4.

full rationale

The central derivation chain is not circular. Theorem 1 proves SMDP soundness directly from the law of total probability and the cluster construction q_{s,a,c}, without assuming any tightness conclusion. Theorem 2 then proves Gamma_SMDP subset of Gamma_MIMDP by checking the defining inequalities of Definition 5 against the conditional distributions in Definition 6; this is a self-contained set-inclusion proof and does not invoke Theorem 4 or the synthesis results. Theorem 4's lower-bound half follows from monotonicity of max-min over a smaller ambiguity set, and the MI-MDP soundness in Corollary 1 follows from Theorem 1 plus Theorem 2. The paper does cite prior work by the same group: Lemma 1 from [27] supplies the reach-set transition bounds used in Definition 5, and Proposition 3 plus the strategy construction from [14] supply the robust dynamic programming machinery used in Section 6. Those are parameter-free supporting theorems about reachability bounds and general UMDPs, respectively, and neither contains the SMDP-versus-MI-MDP containment result, so the citations are independent support rather than a circular premise. The one flagged weakness is the upper-bound half of Theorem 4, which is asserted with 'The same reasoning shows that pbar_SMDP(s) <= pbar_MIMDP(s)' without proving monotonicity of the optimistic value under the differing maximin strategies; this is a correctness or omitted-proof concern, not a circularity. Because no prediction is fitted to the quantity it claims to predict and no conclusion is assumed inside the construction, the circularity score is 2 only for the minor self-citation ledger, not for a circular derivation.

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

The theorems do not fit parameters to data. They depend on a set of explicitly stated modeling assumptions and on cited results about interval bounds and robust dynamic programming from prior work, some co-authored. We list those as axioms rather than treating the paper as fully self-contained.

assumptions (6)
  • domain assumption A sound forward reachable set operator Reach(s,a,c), or a sound overapproximation, is available for every region s, action a, and noise cell c.
    Invoked in Definition 4 and all abstraction constructions in Section 4. The tightness claims are conditional on the quality of this oracle; footnote 2 explicitly allows overapproximation.
  • domain assumption The disturbance process is i.i.d. with known distribution PW and a finite partition C of W is fixed with exact cell probabilities PW(c).
    State in Section 2 and used in Lemma 1 and Definition 6 to assign exact cluster probabilities PW(c); unknown or misspecified PW would break the guarantees.
  • domain assumption Measurability of f in w and of reachable-set intersections with Borel regions, e.g., Lipschitz continuity of f in w uniformly over x.
    Assumed in footnote 3 after Definition 4 and attributed to [16, Assump. 2.1]; needed so the sums in Lemma 1 are well-defined probabilities.
  • standard math Lemma 1 (Theorem 1 of [27]) bounding transition probabilities by noise-cell reachable-set containments and intersections.
    Imported from a published source rather than re-proved; used for all MI-MDP constraints in Definition 5 and in the proof of Theorem 2.
  • standard math Robust dynamic programming convergence and existence of stationary optimal robust strategies from [14, Theorems 6.2 and 6.4].
    Used in Section 6 to justify the recursion (7), the optimal robust strategy, and the upper-bound recursion from [14, Eq. 6.5]. Not re-proved here.
  • domain assumption The state partition S is phi-conservative: safe regions are inside Xsafe, savoid contains Xavoid, and Sreach is a maximal subset of safe regions inside Xreach.
    Definition 1; needed to translate the continuous reach-avoid property into a finite abstraction objective.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems." pith.science (2026). https://pith.science/paper/63XIQJ5J

@misc{pith2026250702213,
  author       = {Pith},
  title        = {Pith review of: Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/63XIQJ5J}},
  note         = {Machine review of arXiv:2507.02213}
}
read the original abstract

This work addresses the general problem of control synthesis for continuous-space, discrete-time stochastic systems with probabilistic guarantees via finite abstractions. While established methods exist, they often trade off accuracy for tractability. We propose a unified abstraction framework that improves both the tightness of probabilistic guarantees and computational efficiency. First, we introduce multi-interval MDPs (MI-MDPs), a generalization of interval-valued MDPs (IMDPs), which allows multiple, possibly overlapping clusters of successor states. This results in tighter abstractions but with increased computational complexity. To mitigate this, we further propose a generalized form of MDPs with set-valued transition probabilities (SMDPs), which model transitions as a fixed probability to a state cluster, followed by a non-deterministic choice within the cluster, as a sound abstraction. We show that control synthesis for MI-MDPs reduces to robust dynamic programming via linear optimization, while SMDPs admit even more efficient synthesis algorithms that avoid linear programming altogether. Theoretically, we prove that, given the partitioning of the state and disturbance spaces, both MI-MDPs and SMDPs yield tighter probabilistic guarantees than IMDPs, and that SMDPs are tighter than MI-MDPs. Extensive experiments across several benchmarks validate our theoretical results and demonstrate that SMDPs achieve favorable trade-offs among tightness, memory usage, and computation time.

Figures

Figures reproduced from arXiv: 2507.02213 by the authors.

Figure 1
Figure 1. 1a–1d illustrate the setup and the different abstrac [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. (a) Setup of Example 3. The SMDP abstraction is [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. 2D-unicycle benchmark: background color indicate probabilistic guarantee ppxq from each initial state, and the green lines are sample trajectories of the closed-loop system from the same initial state. The results correspond to rows 1-4 in [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: 2D-unicycle benchmark: effect of the granularity of the partition S (rows 1-16 in [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]
Figure 5
Figure 5. Figure 5: 3D-unicycle benchmark: effect of the granularity of the partition C (rows 17-28 in [PITH_FULL_IMAGE:figures/full_fig_p014_5.png]
Figure 6
Figure 6. Figure 6: 3D-unicycle benchmark results: effect of the granularity of the disturbance partition [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]
Figure 7
Figure 7. Figure 7: Room temperature benchmark results: effect of increasing the dimension [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 24 canonical work pages

  1. [1]

    Formal control synthesis for stochastic neural network dynamic models

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

    work page 2022

  2. [2]

    Set propagation techniques for reachability analysis

    Matthias Althoff, Goran Frehse, and Antoine Girard. Set propagation techniques for reachability analysis. Annual Review of Control, Robotics, and Autonomous Systems , 4(1):369–395, 2021

    work page 2021

  3. [3]

    Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates

    Thom Badings, Wietze Koops, Sebastian Junges, and Nils Jansen. Learning-based verification of stochastic dynamical systems with neural network policies. arXiv preprint arXiv:2406.00826, 2024

    work page Pith review arXiv 2024

  4. [4]

    Probabilities are not enough: Formal controller synthesis for stochastic dynamical models with epistemic uncertainty

    Thom Badings, Licio Romao, Alessandro Abate, and Nils Jansen. Probabilities are not enough: Formal controller synthesis for stochastic dynamical models with epistemic uncertainty. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 14701–14710, 2023

    work page 2023

  5. [5]

    Sampling-based robust control of autonomous systems with non-gaussian noise

    Thom S Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A Poonawala, and Marielle Stoelinga. Sampling-based robust control of autonomous systems with non-gaussian noise. InProceedings of the AAAI Conference on Artificial Intelligence, volume 36, pages 9669–9678, 2022

    work page 2022

  6. [6]

    Stochastic optimal control: the discrete-time case, volume 5

    Dimitri Bertsekas and Steven E Shreve. Stochastic optimal control: the discrete-time case, volume 5. Athena Scientific, 1996. 15

    work page 1996

  7. [7]

    Efficiency through uncertainty: Scalable formal synthesis for stochastic hybrid systems

    Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, and Luca Cardelli. Efficiency through uncertainty: Scalable formal synthesis for stochastic hybrid systems. InProceedings of the 22nd ACM international conference on hybrid systems: computation and control, pages 240–251, 2019

    work page 2019

  8. [8]

    A learner-verifier framework for neural network controllers and certificates of stochastic systems

    Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner, and Ðorđe Žikelić. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 3–25. Springer, 2023

    work page 2023

Show all 29 references
  1. [9]

    Data-driven interval mdp for robust control synthesis

    Rudi Coppola, Andrea Peruffo, Licio Romao, Alessandro Abate, and Manuel Mazo Jr. Data-driven interval mdp for robust control synthesis. arXiv preprint arXiv:2404.08344, 2024

    2024 arXiv

  2. [10]

    Efficient verification for stochastic mixed monotone systems

    Maxence Dutreix and Samuel Coogan. Efficient verification for stochastic mixed monotone systems. In2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS), pages 150–161. IEEE, 2018

    2018

  3. [11]

    Abstraction-based synthesis for stochastic systems with omega-regular objectives

    Maxence Dutreix, Jeongmin Huh, and Samuel Coogan. Abstraction-based synthesis for stochastic systems with omega-regular objectives. Nonlinear Analysis: Hybrid Systems, 45:101204, 2022

    2022

  4. [12]

    Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes

    Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems, 12(2):921–956, 2013

    2013

  5. [13]

    Bounded- parameter markov decision processes.Artificial Intelligence, 122(1-2):71–109, 2000

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

    2000

  6. [14]

    Efficientstrategysynthesisfor switched stochastic systems with distributional uncertainty

    Ibon Gracia, Dimitris Boskos, Morteza Lahijanian, Luca Laurenti,andManuelMazoJr. Efficientstrategysynthesisfor switched stochastic systems with distributional uncertainty. Nonlinear Analysis: Hybrid Systems, 55:101554, 2025

    2025

  7. [15]

    Data-driven strategy synthesis for stochastic systems with unknown nonlinear disturbances

    Ibon Gracia, Dimitris Boskos, Luca Laurenti, and Morteza Lahijanian. Data-driven strategy synthesis for stochastic systems with unknown nonlinear disturbances. In6th Annual Learning for Dynamics & Control Conference, pages 1633–

  8. [16]

    Temporal logic control for nonlinear stochastic systems under unknown disturbances

    Ibon Gracia, Luca Laurenti, Manuel Mazo Jr, Alessandro Abate, and Morteza Lahijanian. Temporal logic control for nonlinear stochastic systems under unknown disturbances. arXiv preprint arXiv:2412.11343, 2024

    2024 arXiv

  9. [17]

    Formal verification and synthesis for discrete-time stochastic systems

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

    2015

  10. [18]

    A unifying perspective for safety of stochastic systems: From barrier functions to finite abstractions

    Luca Laurenti and Morteza Lahijanian. A unifying perspective for safety of stochastic systems: From barrier functions to finite abstractions. arXiv preprint arXiv:2310.01802, 2023

    2023 arXiv

  11. [19]

    Formal and efficientsynthesisforcontinuous-timelinearstochastichybrid processes

    Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Luca Cardelli, and Marta Kwiatkowska. Formal and efficientsynthesisforcontinuous-timelinearstochastichybrid processes. IEEE Transactions on Automatic Control , 66(1):17–32, 2020

    2020

  12. [20]

    Constructing mdp abstractions using data with formal guarantees.IEEEControlSystemsLetters , 7:460–465, 2022

    Abolfazl Lavaei, Sadegh Soudjani, Emilio Frazzoli, and Majid Zamani. Constructing mdp abstractions using data with formal guarantees.IEEEControlSystemsLetters , 7:460–465, 2022

    2022

  13. [21]

    Scalable control synthesis for stochastic systems via structural imdp abstractions

    Frederik Baymler Mathiesen, Sofie Haesaert, and Luca Laurenti. Scalable control synthesis for stochastic systems via structural imdp abstractions. arXiv preprint arXiv:2411.11803, 2024

    2024 arXiv

  14. [22]

    Intervalmdp

    Frederik Baymler Mathiesen, Morteza Lahijanian, and Luca Laurenti. Intervalmdp. jl: Accelerated value iteration for interval markov decision processes. IFAC-PapersOnLine, 58(11):1–6, 2024

    2024

  15. [23]

    Adata-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution

    Frederik Baymler Mathiesen, Licio Romao, Simeon C Calvert,LucaLaurenti,andAlessandroAbate. Adata-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution. arXiv preprint arXiv:2410.06662, 2024

    arXiv

  16. [24]

    Safety guarantees for neural network dynamic systems via stochastic barrier functions

    Rayan Mazouz, Karan Muvvala, Akash Ratheesh Babu, Luca Laurenti, and Morteza Lahijanian. Safety guarantees for neural network dynamic systems via stochastic barrier functions. In Advances in Neural Information Processing Systems (NeurIPS), volume 35, pages 9672–9686, New Orlea...

    2022

  17. [25]

    Data-driven yet formal policy synthesis for stochastic nonlinear dynamical systems

    Mahdi Nazeri, Thom Badings, Sadegh Soudjani, and Alessandro Abate. Data-driven yet formal policy synthesis for stochastic nonlinear dynamical systems. arXiv preprint arXiv:2501.01191, 2025

    2025 arXiv

  18. [26]

    Data-driven verification and synthesis of stochasticsystemsthroughbarriercertificates

    Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani, and Majid Zamani. Data-driven verification and synthesis of stochasticsystemsthroughbarriercertificates. arXivpreprint arXiv:2111.10330, 2021

    2021 arXiv

  19. [27]

    Formal abstraction of general stochastic systems via noise partitioning.IEEE Control Systems Letters, 2023

    John Skovbekk, Luca Laurenti, Eric Frew, and Morteza Lahijanian. Formal abstraction of general stochastic systems via noise partitioning.IEEE Control Systems Letters, 2023

    2023

  20. [28]

    Planning under risk and knightian uncertainty

    Felipe W Trevizan, Fabio Gagliardi Cozman, and Leliane Nunes de Barros. Planning under risk and knightian uncertainty. InIJCAI, volume 2007, pages 2023–2028, 2007

    2007

  21. [29]

    Planning with linear temporal logic specifications: Handling quantifiable and unquantifiable uncertainty.arXiv preprint arXiv:2502.19603, 2025

    Pian Yu, Yong Li, David Parker, and Marta Kwiatkowska. Planning with linear temporal logic specifications: Handling quantifiable and unquantifiable uncertainty.arXiv preprint arXiv:2502.19603, 2025. 16

    2025 arXiv

Pith tools

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