Pith. sign in

REVIEW 2 major objections 4 minor 59 references

ARCH-COMP25 Category Report: Stochastic Models

T0 review · 2 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read This report claims that the 2025 stochastic-models competition produced a reproducible comparison of six verification and synthesis tools, anchored by a new water-distribution network benchmark and a suite of reduced benchmarks.

desk verdict Useful benchmarking infrastructure with an honest disclosure culture; the CS2 ambiguity must be resolved before the comparison table can be trusted. read the letter →

arxiv 2506.17602 v1 pith:AEQ45GTX submitted 2025-06-21 cs.LO cs.SYeess.SY

Alessandro Abate , Omid Akbarzadeh , Henk A.P. Blom , Sofie Haesaert , Sina Hassani , Abolfazl Lavaei , Frederik Baymler Mathiesen , Rahul Misra
show 9 more authors
Amy Nejati Mathis Niehage Fie {O}rum Anne Remke Behrad Samari Ruohan Wang Rafal Wisniewski Ben Wooding Mahdieh Zaker
This is my paper · ORCID
classification cs.LOcs.SYeess.SY
keywords stochastichybridsystemsformalverificationpolicysynthesisbenchmarksuitewaterdistributionnetworkintervalMarkovdecisionprocessesbarriercertificatesrare-eventsimulation
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 report is the outcome of a friendly annual comparison of software tools for formal verification and policy synthesis of stochastic systems. It claims that the 2025 edition now provides a reliable and reproducible map of which tools can solve which problems, thanks to three first-time participants and a deliberately broadened benchmark suite. The centerpiece is a new water-distribution network benchmark in which a water tower must be kept between 28 L and 155 L under random consumption; the task is to synthesize or verify a controller that guarantees safety with a stated probability. To make tools with very different model classes comparable, the organizers added simplified versions of patrol robot, autonomous vehicle, and building automation benchmarks. If the report's results hold, the community gains a shared testbed for stochastic safety analysis and a clearer picture of the current state of the art.

What carries the argument

The central supporting object is the water-tower volume-balance model: Eq. (2), the forward-Euler discretization $V(t+t_s)=V(t)+t_s\sum_i q_i(t)-t_s\sum_i d_i(t)$, together with the pump-power equation $P_i(t)=\frac{1}{\eta_i} q_i(t)\left(r_{f,i}|q_i(t)|q_i(t)+r_{f,\Sigma}|q_\Sigma(t)|q_\Sigma(t)+\rho_w g_0(h_V(t)+h_i)\right)$ and the box constraint $28\,\mathrm{L}\le V(t)\le155\,\mathrm{L}$. This model turns infrastructure safety into a concrete stochastic synthesis problem. The second mechanism is the suite of reduced benchmarks—patrol robot, autonomous vehicle, building automation—designed so tools that discretize state space and struggle with high dimensions can still be evaluated on the same specifications. The comparison mechanism across tools is a mix of formal guarantees: barrier-certificate bounds (PRoTECT), interval value iteration over IMDP abstractions (IMPaCT, IntervalMDP.jl), stochastic coupling relations (SySCoRe), and symbolic state-space construction combined with statistical model checking (hpnmg).

What would settle it

Resample the Bjerringbro consumption data at one-minute resolution and recompute the certified safety probability for the same controller; if the re-verified probability falls materially below the reported guarantee, the constant-flow discretization assumption is the point of failure. Alternatively, compare simulated tower volumes against measured volumes over the 88-day dataset.

Watch

Extended reading notes

Core claim

On the report's own terms, the central result is not a new theorem but a usable, reproducible comparison infrastructure. Three first-time tools—PRoTECT, IMPaCT, and IntervalMDP.jl—are shown solving safety, reachability, and reach-while-avoid specifications on a common set of benchmarks, while established tools SySCoRe, hpnmg, and AMYTISS extend their coverage to simplified benchmark variants. The new water-distribution benchmark models a tower whose volume evolves as $V(t+t_s)=V(t)+t_s\sum_{i=1}^{N_q} q_i(t)-t_s\sum_{i=1}^{N_d} d_i(t)$, with pump power and consumption noise, and asks for a probabilistic safety guarantee that the volume stays within $28\,\mathrm{L}\le V(t)\le155\,\mathrm{L}$. The report also documents a lane-change collision scenario in which an interacting-particle rare-event estimator returns probabilities around $10^{-7}$ where Monte Carlo simulation returns zero, and a hpnmg guided-simulation engine whose rare-event confidence intervals overlap those of earlier tools while running much faster.

Load-bearing premise

The forward-Euler balance equation is treated as exact, which requires pump flows and consumption to stay constant over each 15-minute sampling interval; real consumption fluctuates within that interval, so the benchmark's safety probabilities may not describe the true water network.

Editorial extensions

If this is right

  • Safety certificates for the water network: the benchmark gives tool developers a concrete target—probabilistic safety for a 28–155 L tower subject to demand noise—so new synthesis algorithms can be tested against published numbers.
  • Comparable tool rankings: the reduced benchmark suite lets tools that previously applied to disjoint models be evaluated on the same specifications, making head-to-head comparison possible for the first time.
  • Rare-event reachability: the lane-change results show that importance-splitting estimation can produce collision probabilities around $10^{-7}$ where plain Monte Carlo returns zero, giving a practical way to certify very small risk.
  • Faster rare-event checking: hpnmg's guided simulation matches the confidence intervals of conventional simulation tools on the sewage benchmark in less time, suggesting a scalable route for rare-event verification.
  • Reproducibility baseline: because the benchmark code and repeatability packages were collected, the reported numbers can be re-run and extended by later editions.

Reading between the lines

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

  • The water-network model's safety guarantee is only as good as the constant-consumption-per-interval assumption; re-verifying with sub-15-minute consumption data would show whether the reported probabilities hold under realistic demand fluctuations.
  • The same pump-power equations could turn the benchmark into an energy-versus-safety trade-off study: minimizing pumping cost while keeping the tower within bounds is a natural next synthesis objective.
  • The reduced-benchmark approach could be applied to the new water network itself—for example, a one-pump no-elevation variant—to let tools that cannot handle high-dimensional abstractions compete on an infrastructure-relevant model.
  • Connecting the lane-change rare-event result to the other benchmarks suggests a general pattern: tools that combine symbolic state-space construction with statistical simulation may be the most practical route for $10^{-6}$-level safety claims on hybrid models.
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

2 major / 4 minor

Summary. This manuscript is the ARCH-COMP25 category report for stochastic models. It describes the 2025 friendly competition, introducing three tools (PRoTECT, IMPaCT, IntervalMDP.jl) and reporting new results from them and from SySCoRe, hpnmg, and AMYTISS on established and new benchmarks. It also introduces a water distribution network benchmark and a collection of reduced benchmark variants intended to broaden tool participation, and it discusses scalability and next steps. Results are reported per tool with runtimes, memory usage, and satisfaction probabilities, and the accompanying code is made publicly available.

Significance. If the reported measurements are trustworthy, this report provides a useful snapshot of the current tool landscape and a reusable benchmark suite. Its strengths include public code repositories, candid reporting of a failed abstraction in §5.3.5, and an explicit caveat about the CS2 benchmark definition in §5.3.2. The new water-distribution benchmark targets a practically motivated infrastructure domain, though no tool result is reported on it in this edition. The per-tool results and the honest documentation of negative outcomes are valuable to the verification and synthesis community, provided the comparability concerns raised below are addressed.

major comments (2)
  1. [§5.3.2 and §5.4.1] The CS2 building-automation results are presented as part of a common benchmark comparison, but the report itself states in §5.3.2 that "there is confusion between implementations about which is the correct system (e.g., whether the dynamics are linear or affine, and whether the dynamics include control)." The full dynamics printed there are used for the IntervalMDP.jl experiments, yet §5.4.1 does not state which dynamics, affine term Q, control input, or noise model SySCoRe used for CS2. Given that the two tools report satisfaction numbers differing by many orders of magnitude (a certified lower bound below 1e-10 with mean error above 99.99% versus peak probabilities around 0.96), the reader cannot verify that the two tools solved the same mathematical problem. The authors must either specify the exact model used by each tool and confirm that they coincide, or explicitly mark the CS2 numbers as not comparable.
  2. [§4.3 and §5.2.5/§5.3.4/Table 11] The reduced benchmarks are introduced as a way to make tools comparable, but the subsequent results do not consistently identify which scenario variant is solved. For the reduced patrol robot, §4.3.1 defines four distinct scenarios, yet IMPaCT's run in §5.2.5 is described only as a reachability specification while also mentioning avoid sets, AMYTISS in Table 11 solves reach-while-avoid, and IntervalMDP.jl in §5.3.4 solves both reachability and reach-while-avoid. A reader cannot reconstruct from the text which scenario each tool actually solved, which undermines the claimed comparability of the reduced benchmark suite. A table mapping each tool to the exact specification variant (including horizon, disturbance presence, and discretization) should be added.
minor comments (4)
  1. [§4.2 / Table 7] The statement that Table 7 "underscores the superiority of the IPS-FAS algorithm over MC simulation" overstates what the table shows; zero estimates from crude Monte Carlo for rare events are an expected artifact of finite sampling, and no confidence intervals or variance estimates are reported for either estimator. Please rephrase to a factual statement, e.g., that IPS-FAS yields nonzero estimates where crude MC returns zero.
  2. [§4.1.1 / Eq. (2)] The forward-Euler discretization is exact only under the stated constancy assumption on flows, and the paper acknowledges this. Since Figure 1 shows consumption varying within the 15-minute sampling interval, please add a sentence quantifying or explicitly bounding the resulting discretization error, or state clearly that the benchmark model is an approximation of the continuous-time balance.
  3. [§5.3.5] The automated-vehicle result is reported with a certified satisfaction probability that is trivially zero due to grid misalignment with the target set. This is honest, but it should be labeled as a setup artifact rather than a benchmark outcome, so that it is not read as evidence about the tool's capability on the AV benchmark.
  4. [§5.4.1] The sentence "We have updated the output to be only the temperature in zone one for CS1" changes the benchmark's output mapping and should be reflected explicitly in the specification description; as written, the reader must infer that the SySCoRe CS1 result is not for the original output.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the report's results are measured tool executions on shared benchmarks, and self-citations are provenance, not load-bearing.

full rationale

This is a benchmark competition report, not a derivation of a formal result. Its central outputs are measurements from running tools (runtime, memory, probability bounds) on models defined in Sections 3 and 4. No reported tool result is obtained by assuming the conclusion it is supposed to demonstrate. The water distribution network model in Section 4.1 is an input benchmark, not a derived prediction; the forward-Euler discretization in Eq. (2) is presented with its exactness condition explicitly stated ('for the discretization to be exact, the consumption di(t) and the pump station flow qi(t)... must remain constant over each sampling interval'), so it is a transparent modeling assumption rather than a fitted parameter relabeled as a prediction. The reduced patrol robot and reduced autonomous vehicle benchmarks are 'Taken from [11]' and 'Borrowed from [11], [52]', where [11] is a paper by two of the report's authors and describes IMPaCT. This is a self-citation, but it is used only as provenance for the benchmark dynamics and discretization parameters; the tool results on those benchmarks are recomputed and reported in Sections 5.2, 5.3, and 5.6, so the self-citation is not load-bearing for the benchmarking claims. No uniqueness theorem, ansatz, or known result is imported from the authors' prior work to force a conclusion. The one acknowledged limitation is the CS2 building automation benchmark in Section 5.3.2: 'there is confusion between implementations about which is the correct system (e.g., whether the dynamics are linear or affine, and whether the dynamics include control)'. This is a genuine threat to the reproducibility/comparability of the two CS2 tool entries, and it should be weighed as a correctness and benchmarking-validity concern, not as circularity: neither tool's computed probability is equivalent by construction to the benchmark definition or to the other tool's output. Overall, the paper does not fit any of the circularity patterns: there is no self-definitional reduction, no fitted input called a prediction, no load-bearing self-citation chain, and no renaming of a known result as a new one.

Assumptions & free parameters 4 free parameters · 3 assumptions · 0 invented entities

The central benchmarking results rest on well-established tool theory and the benchmark models described in the text. The main free choices are the hand-picked constants of the water distribution model and the tuned barrier certificate parameters.

free parameters (4)
  • Water tower elevations h1, h2 = 2.0 m, 1.5 m
    Chosen arbitrarily given laboratory limitations (Section 4.1.3), affecting the water distribution benchmark dynamics.
  • Pump station efficiencies eta1, eta2 = 0.90, 0.80
    Chosen arbitrarily given laboratory limitations (Section 4.1.3).
  • Water consumption prediction profile = Mean of the 88-day dataset in 15-minute intervals
    Section 4.1.4 uses the empirical mean flow as the prediction model; this is a fit to the measured consumption data and is not independently derived.
  • PRoTECT level set parameters gamma, lambda, c = Varies per benchmark (e.g., AS: gamma=1.01e-6, lambda=2.0e-4, c=1.25e-6)
    Tuned in Section 5.1 to achieve the desired confidence level; these are tool parameters, not physical constants.
assumptions (3)
  • domain assumption Forward Euler discretization of the volume balance is exact when flows are constant over the sampling interval.
    Stated in Section 4.1.1 after Eq. (2); if real consumption or pump flows change faster than the sampling interval, the benchmark model introduces discretization error.
  • domain assumption The GSHS semantics of [50] govern the lane-change model.
    Section 4.2 relies on the general stochastic hybrid system definition from [50] without re-deriving it.
  • standard math Barrier certificate conditions imply safety with the stated confidence.
    PRoTECT results in Section 5.1 rely on stochastic barrier certificate theory from [7],[8], treated as established.

how reviews work

0 comments
Cite this review

Pith. "Pith review of ARCH-COMP25 Category Report: Stochastic Models." pith.science (2026). https://pith.science/paper/AEQ45GTX

@misc{pith2026250617602,
  author       = {Pith},
  title        = {Pith review of: ARCH-COMP25 Category Report: Stochastic Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AEQ45GTX}},
  note         = {Machine review of arXiv:2506.17602}
}
read the original abstract

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year's edition of the competition. In particular, this report introduces three recently developed software tools, a new water distribution network benchmark, and a collection of simplified benchmarks intended to facilitate further comparisons among tools that were previously not directly comparable. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2025.

Figures

Figures reproduced from arXiv: 2506.17602 by the authors.

Figure 1
Figure 1. Current and predicted flow into the consumption group of the water distribution [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Lane-change scenario: The two AVs are denoted by [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. The circumscribed ellipse Om,i around each AV. contributory component whose value does not influence the outcome. Each discrete state component conveys specific behavior or intent, interpreted as follows: • 0: the AV is proceeding straight without initiating a lane change; • 1: the AV is actively changing lanes; • 2: the AV has detected that the other vehicle is attempting a lane change; • −1: the AV is reversing it… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Transition graphs of the GSHS models for AVs [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 51 canonical work pages

  1. [1]

    The ARCH-COMP friendly verification competition for continuous and hybrid systems,

    A. Abate, M. Althoff, L. Bu, et al., “The ARCH-COMP friendly verification competition for continuous and hybrid systems,” in Proceedings of International TOOLympics Challenge , Springer, 2024, pp. 1–37

    work page 2024

  2. [2]

    Automated verification and synthesis of stochastic hybrid systems: A survey,

    A. Lavaei, S. Soudjani, A. Abate, and M. Zamani, “Automated verification and synthesis of stochastic hybrid systems: A survey,” Automatica, vol. 146, 2022

    work page 2022

  3. [3]

    Tools at the frontiers of quantitative verification - QComp 2023 competition report,

    R. Andriushchenko et al., “Tools at the frontiers of quantitative verification - QComp 2023 competition report,” in International TOOLympics Challenge , 2024, pp. 90–146

    work page 2023

  4. [4]

    Protect: Parallelized construction of safety barrier certificates for nonlinear polynomial systems,

    B. Wooding, V. Horbanov, and A. Lavaei, “Protect: Parallelized construction of safety barrier certificates for nonlinear polynomial systems,” arXiv preprint arXiv:2404.14804 , 2024

    arXiv 2024

  5. [5]

    Protect: Parallel construction of barrier certificates for safety verification of polynomial systems,

    B. Wooding, V. Horbanov, and A. Lavaei, “Protect: Parallel construction of barrier certificates for safety verification of polynomial systems,” in 16th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS) , 2025, pp. 1–3

    work page 2025

  6. [6]

    Yuan, SumOfSquares.py

    C. Yuan, SumOfSquares.py. [Online]. Available: https://github.com/yuanchenyang/ SumOfSquares.py. 26 ARCH-COMP25 Stochastic Models Abate et. al

    work page

  7. [7]

    Compositional construction of control barrier certificates for large-scale interconnected stochastic systems,

    M. Anand, A. Lavaei, and M. Zamani, “Compositional construction of control barrier certificates for large-scale interconnected stochastic systems,” IFAC-PapersOnLine, vol. 53, no. 2, pp. 1862–1867, 2020

    work page 2020

  8. [8]

    Compositional construction of control barrier functions for networks of continuous-time stochastic systems,

    A. Nejati, S. Soudjani, and M. Zamani, “Compositional construction of control barrier functions for networks of continuous-time stochastic systems,”IFAC-PapersOnLine, vol. 53, no. 2, pp. 1856–1861, 2020

    work page 2020

Show all 59 references
  1. [9]

    ApS, Mosek optimizer api for python , 2022

    M. ApS, Mosek optimizer api for python , 2022

    2022

  2. [10]

    CVXOPT: A Python package for convex optimization,

    M. S. Andersen, J. Dahl, L. Vandenberghe, et al. , “CVXOPT: A Python package for convex optimization,” Available at cvxopt.org, vol. 54, 2013

    2013

  3. [11]

    IMPaCT: Interval MDP parallel construction for controller synthesis of large-scale stochastic systems,

    B. Wooding and A. Lavaei, “IMPaCT: Interval MDP parallel construction for controller synthesis of large-scale stochastic systems,” in International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems , Springer, 2024, pp. 249–267

    2024

  4. [12]

    IMPaCT: A parallelized software tool for IMDP construction and controller synthesis with convergence guarantees,

    B. Wooding and A. Lavaei, “IMPaCT: A parallelized software tool for IMDP construction and controller synthesis with convergence guarantees,” in Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , 2024, pp. 1–2

    2024

  5. [13]

    Interval iteration algorithm for MDPs and IMDPs,

    S. Haddad and B. Monmege, “Interval iteration algorithm for MDPs and IMDPs,” Theoretical Computer Science, vol. 735, pp. 111–131, 2018

    2018

  6. [14]

    SYCL beyond OpenCL: The Architecture, Current State and Future Direction of HipSYCL,

    A. Alpay and V. Heuveline, “SYCL beyond OpenCL: The Architecture, Current State and Future Direction of HipSYCL,” in Proceedings of the International Workshop on OpenCL , 2020

    2020

  7. [15]

    One Pass to Bind Them: The First Single-Pass SYCL Compiler with Unified Code Representation Across Backends,

    A. Alpay and V. Heuveline, “One Pass to Bind Them: The First Single-Pass SYCL Compiler with Unified Code Representation Across Backends,” in Proceedings of the 2023 International Workshop on OpenCL , 2023

    2023

  8. [16]

    [Online]

    The HDF Group, Hierarchical Data Format, version 5 , 1997-2023. [Online]. Available: https://www.hdfgroup.org/HDF5/

    1997

  9. [17]

    Data-driven abstractions via binary- tree gaussian processes for formal verification,

    O. Sch¨ on, S. Naseer, B. Wooding, and S. Soudjani, “Data-driven abstractions via binary- tree gaussian processes for formal verification,” IFAC-PapersOnLine, vol. 58, no. 11, pp. 115–122, 2024

    2024

  10. [18]

    IntervalMDP.jl: accelerated value iteration for interval markov decision processes,

    F. B. Mathiesen, M. Lahijanian, and L. Laurenti, “IntervalMDP.jl: accelerated value iteration for interval markov decision processes,” IFAC-PapersOnLine, vol. 58, no. 11, pp. 1–6, 2024, 8th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2024, issn: 2405-8963. do...

    2024 doi

  11. [19]

    Scalable control synthesis for stochastic systems via structural IMDP abstractions,

    F. B. Mathiesen, S. Haesaert, and L. Laurenti, “Scalable control synthesis for stochastic systems via structural IMDP abstractions,” arXiv preprint arXiv:2411.11803 , 2024

    2024 arXiv

  12. [20]

    Strategy synthesis for partially- known switched stochastic systems,

    J. Jackson, L. Laurenti, E. Frew, and M. Lahijanian, “Strategy synthesis for partially- known switched stochastic systems,” in Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control , ser. HSCC ’21, 2021, isbn: 9781450383394. doi: 10.1145/3...

    2021

  13. [21]

    Hpnmg: A C++ Tool for Model Checking Hybrid Petri Nets with General Transitions,

    J. H¨ uls, H. Niehaus, and A. Remke, “Hpnmg: A C++ Tool for Model Checking Hybrid Petri Nets with General Transitions,” in 12th International NASA Formal Methods Symposium, NFM 2020, Springer, 2020. 27 ARCH-COMP25 Stochastic Models Abate et. al

    2020

  14. [22]

    Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes,

    J. H¨ uls and A. Remke, “Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes,” in 19th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 , ser. LNCS, vol. 11535, Cham: Spr...

    2019

  15. [23]

    State-Space Construction of Hybrid Petri Nets with Multiple Stochastic Firings,

    J. H¨ uls, C. Pilch, P. Schinke, J. Delicaris, and A. Remke, “State-Space Construction of Hybrid Petri Nets with Multiple Stochastic Firings,” in 16th International Conference on Quantitative Evaluation of Systems, QEST 2019 , ser. LNCS, vol. 11785, Cham, Switzerland: Springer...

    2019

  16. [24]

    Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro,

    J. H¨ uls, S. Schupp, A. Remke, and E.´Abrah´ am, “Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro,” in 11th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2017 , ACM, 2018, pp. 178–185

    2017

  17. [25]

    HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis,

    S. Schupp, E. ´Abrah´ am, I. B. Makhlouf, and S. Kowalewski, “HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis,” in NASA Formal Methods, C. Barrett, M. Davies, and T. Kahsai, Eds., vol. 10227, Cham: Springer, 2017, pp. 288–294

    2017

  18. [26]

    A new algorithm for adaptive multidimensional integration,

    G. P. Lepage, “A new algorithm for adaptive multidimensional integration,” Journal of Computational Physics, vol. 27, no. 2, pp. 192–203, 1978

    1978

  19. [27]

    State-space Construction of Hybrid Petri Nets with Multiple Stochastic Firings,

    J. H¨ uls, C. Pilch, P. Schinke, H. Niehaus, J. Delicaris, and A. Remke, “State-space Construction of Hybrid Petri Nets with Multiple Stochastic Firings,” ACM Transactions on Modeling and Computer Simulation , vol. 31, no. 3, pp. 1–37, 2021

    2021

  20. [28]

    Rare event simulation for stochastic hybrid systems using symbolic importance functions,

    M. Niehage, A. Hartmanns, and A. Remke, “Rare event simulation for stochastic hybrid systems using symbolic importance functions,” ser. LNICST, vol. 539, Springer, 2023, pp. 61–81. doi: 10.1007/978-3-031-48885-6\_5

    2023 doi

  21. [29]

    Symbolic state-space exploration meets statistical model checking,

    M. Niehage and A. Remke, “Symbolic state-space exploration meets statistical model checking,” Performance Evaluation, vol. 167, p. 102 449, 2025. doi: 10.1016/J.PEVA. 2024.102449

    2025

  22. [30]

    HYPEG: Statistical Model Checking for hybrid Petri nets: Tool Paper,

    C. Pilch and A. Remke, “HYPEG: Statistical Model Checking for hybrid Petri nets: Tool Paper,” in Proceedings of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools, ser. VALUETOOLS 2017, Venice, Italy: ACM, 2017, pp. 186–191

    2017

  23. [31]

    Statistical Model Checking for hybrid Petri nets with multiple general transitions,

    C. Pilch and A. Remke, “Statistical Model Checking for hybrid Petri nets with multiple general transitions,” in Proceedings of the 47th IEEE/IFIP International Conference on Dependable Systems and Networks , IEEE, 2017, pp. 475–486

    2017

  24. [32]

    Learning optimal decisions for stochastic hybrid systems,

    M. Niehage, A. Hartmanns, and A. Remke, “Learning optimal decisions for stochastic hybrid systems,” in MEMOCODE ’21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Virtual Event, China, November 20 - 22, 2021, S. Arun-Kumar, D. M´ ery, I...

    2021

  25. [33]

    Learning that grid-convenience does not hurt resilience in the presence of uncertainty,

    M. Niehage and A. Remke, “Learning that grid-convenience does not hurt resilience in the presence of uncertainty,” in Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings, S. Bogomolov a...

    2022 doi

  26. [34]

    Rare event simulation for stochastic hybrid systems using symbolic importance functions,

    M. Niehage and A. Remke, “Rare event simulation for stochastic hybrid systems using symbolic importance functions,” in To appear in 17th International NASA Formal Methods Symposium, NFM 2025 , Springer, 2025

    2025

  27. [35]

    Syscore 2.0: Toolset for formal control synthesis of continuous-state stochastic systems and temporal logic specifications,

    B. van Huijgevoort, M. H. W. Engelaar, S. Soudjani, and S. Haesaert, “Syscore 2.0: Toolset for formal control synthesis of continuous-state stochastic systems and temporal logic specifications,” Nonlinear Analysis: Hybrid Systems , vol. 58, p. 101 607, 2025

    2025

  28. [36]

    Syscore: Synthesis via stochastic coupling relations,

    B. van Huijgevoort, O. Sch¨ on, S. Soudjani, and S. Haesaert, “Syscore: Synthesis via stochastic coupling relations,” in Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control , ser. HSCC ’23, San Antonio, TX, USA: Association for Compu...

    2023

  29. [37]

    Verification of general Markov decision processes by approximate similarity relations and policy refinement,

    S. Haesaert, S. Soudjani, and A. Abate, “Verification of general Markov decision processes by approximate similarity relations and policy refinement,” SIAM Journal on Control and Optimization, vol. 55, no. 4, pp. 2333–2367, 2017

    2017

  30. [38]

    Abstracting linear stochastic systems via knowledge filtering,

    M. H. W. Engelaar, L. Romao, Y. Gao, M. Lazar, A. Abate, and S. Haesaert, “Abstracting linear stochastic systems via knowledge filtering,” in 2023 62nd IEEE Conference on Decision and Control (CDC) , IEEE, 2023, pp. 3049–3054

    2023

  31. [39]

    AMYTISS: Parallelized automated controller synthesis for large-scale stochastic systems,

    A. Lavaei, M. Khaled, S. Soudjani, and M. Zamani, “AMYTISS: Parallelized automated controller synthesis for large-scale stochastic systems,” in 32nd International conference on computer aided verification (CAV) , ser. LNCS, Springer, 2020, pp. 461–474

    2020

  32. [40]

    AMYTISS: A parallelized tool on automated controller synthesis for large-scale stochastic systems,

    A. Lavaei, M. Khaled, S. Soudjani, and M. Zamani, “AMYTISS: A parallelized tool on automated controller synthesis for large-scale stochastic systems,” in Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control , 2020, pp. 1–2

    2020

  33. [41]

    pFaces: an acceleration ecosystem for symbolic control,

    M. Khaled and M. Zamani, “pFaces: an acceleration ecosystem for symbolic control,” in Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019, pp. 252–257

    2019

  34. [42]

    Abstraction-based synthesis of stochastic hybrid systems,

    A. Lavaei, “Abstraction-based synthesis of stochastic hybrid systems,” in Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , 2024, pp. 1–11

    2024

  35. [43]

    Automated verification and control of large-scale stochastic cyber-physical systems: Compositional techniques,

    A. Lavaei, “Automated verification and control of large-scale stochastic cyber-physical systems: Compositional techniques,” Ph.D. dissertation, PhD Dissertation, Technische Universit¨ at M¨ unchen, 2019

    2019

  36. [44]

    StocHy: Automated verification and synthesis of stochastic processes,

    N. Cauchi and A. Abate, “StocHy: Automated verification and synthesis of stochastic processes,” in 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , 2019

    2019

  37. [45]

    From dissipativity theory to compositional synthesis of large- scale stochastic switched systems,

    A. Lavaei and M. Zamani, “From dissipativity theory to compositional synthesis of large- scale stochastic switched systems,” IEEE Transactions on Automatic Control , vol. 67, no. 9, pp. 4422–4437, 2022

    2022

  38. [46]

    Scalable synthesis of finite MDPs for large-scale stochastic switching systems,

    A. Lavaei and E. Frazzoli, “Scalable synthesis of finite MDPs for large-scale stochastic switching systems,” in 2022 IEEE 61st Conference on Decision and Control (CDC) , 2022, pp. 7510–7515

    2022

  39. [47]

    Arch-comp23 category report: Stochastic models,

    A. Abate, H. Blom, N. Cauchi, et al., “Arch-comp23 category report: Stochastic models,” in 10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023, EasyChair, 2023, pp. 126–150. 29 ARCH-COMP25 Stochastic Models Abate et. al

    2023

  40. [48]

    Rare collision risk estimation of autonomous vehicles with multi-agent situation awareness,

    M. Zaker, H. A. Blom, S. Soudjani, and A. Lavaei, “Rare collision risk estimation of autonomous vehicles with multi-agent situation awareness,” in Proceedings of the 27th International Conference on Intelligent Transportation Systems (ITSC) , IEEE, 2024, pp. 4108–4115

    2024

  41. [49]

    Path planning using a dynamic vehicle model,

    R. Pepy, A. Lambert, and H. Mounier, “Path planning using a dynamic vehicle model,” in Proceedings of the 2nd International Conference on Information & Communication Technologies, IEEE, vol. 1, 2006, pp. 781–786

    2006

  42. [50]

    Toward a general theory of stochastic hybrid systems,

    M. L. Bujorianu and J. Lygeros, “Toward a general theory of stochastic hybrid systems,” Stochastic hybrid systems: theory and safety critical applications , pp. 3–30, 2006

    2006

  43. [51]

    Interacting particle system based estimation of reach probability of general stochastic hybrid systems,

    H. Ma and H. A. Blom, “Interacting particle system based estimation of reach probability of general stochastic hybrid systems,” Nonlinear Analysis: Hybrid Systems , vol. 47, 2023

    2023

  44. [52]

    Feedback refinement relations for the synthesis of symbolic controllers,

    G. Reissig, A. Weber, and M. Rungger, “Feedback refinement relations for the synthesis of symbolic controllers,” IEEE Transactions on Automatic Control , vol. 62, no. 4, pp. 1781– 1796, 2016

    2016

  45. [53]

    Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems,

    A. Nejati, S. Soudjani, and M. Zamani, “Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems,” European Journal of Control, vol. 57, pp. 82– 94, 2021

    2021

  46. [54]

    ARCH-COMP18 category report: Stochastic modelling,

    A. Abate, H. Blom, N. Cauchi, et al. , “ARCH-COMP18 category report: Stochastic modelling,” in ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems , ser. EPiC Series in Computing, vol. 54, EasyChair, 2018, pp. 71–103. doi: 10 . 29007 / 7...

    2018

  47. [55]

    ARCH-COMP19 category report: Stochastic modelling,

    A. Abate, H. Blom, N. Cauchi, et al. , “ARCH-COMP19 category report: Stochastic modelling,” in ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems , ser. EPiC Series in Computing, vol. 61, EasyChair, 2019, pp. 62–102. doi: 10 . 29007 / f...

    2019

  48. [56]

    Arch-comp20 category report: Stochastic models,

    A. Abate, H. Blom, N. Cauchi, et al., “Arch-comp20 category report: Stochastic models,” in ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20) , G. Frehse and M. Althoff, Eds., ser. EPiC Series in Computing, vol. 74, EasyChair, ...

    2020 doi

  49. [57]

    ARCH-COMP22 Category Report: Stochastic Models,

    A. Abate, H. Blom, J. Delicaris, et al., “ARCH-COMP22 Category Report: Stochastic Models,” vol. 90, EasyChair, Dec. 2022, pp. 113–141. doi: 10 . 29007 / LSVC. [Online]. Available: https://gitlab.com/goranf/ARCH-COMP

    2022

  50. [58]

    Efficiency through uncertainty: Scalable formal synthesis for stochastic hybrid systems,

    N. Cauchi, L. Laurenti, M. Lahijanian, A. Abate, M. Kwiatkowska, and L. Cardelli, “Efficiency through uncertainty: Scalable formal synthesis for stochastic hybrid systems,” in 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), arXiv: 1901.01576, 2019

    1901 arXiv

  51. [59]

    Arch-comp21 category report: Stochastic mod- els,

    A. Abate, H. Blom, M. Bouissou, et al., “Arch-comp21 category report: Stochastic mod- els,” in 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21) , G. Frehse and M. Althoff, Eds., ser. EPiC Series in Computing, vol. 80, EasyChair, 2021...

    2021 doi

Pith tools

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