Pith. sign in

REVIEW 4 major objections 5 minor 38 references

Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata

T0 review · 4 major / 5 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 The paper claims that stochastic Simulink subsystems can be transformed into stochastic hybrid automata, enabling formal quantitative analysis of safety and performance under uncertainty.

desk verdict A useful, well-scoped extension of Simulink-to-SHA transformation, but the missing semantics-preservation proof leaves the central formal claim only conditionally supported. read the letter →

arxiv 2506.14581 v1 pith:LGU74S4Z submitted 2025-06-17 eess.SY cs.SY

Pauline Blohm , Felix Schulz , Lisa Willemsen , Anne Remke , Paula Herber This is my paper · ORCID
classification eess.SYcs.SY
keywords SimulinkStochasticHybridAutomataUncertaintyStatisticalModelCheckingSafetyanalysisPerformancetransformationHAwK
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

Simulink is widely used for embedded control design, but its semantics are informal and its models usually ignore uncertainty such as sensor noise, aging, and failures. This paper tries to close that gap by providing six parameterizable Simulink subsystems that inject stochastic behavior, and by giving transformation rules that turn each subsystem into a stochastic hybrid automaton (SHA) template. The templates compose with an existing Simulink-to-SHA transformation, so the resulting formal model can be analyzed with statistical model checking and reachability analysis rather than by expensive simulation alone. On two small case studies, the SHA-based analysis produces confidence intervals that agree with Simulink simulation while running orders of magnitude faster. If the transformation is faithful, engineers could get formal, probabilistic safety and performance guarantees for Simulink models that include realistic uncertainties.

What carries the argument

The central object is the HAwK, a hybrid automaton with stochastic kernels: delay kernels sample the expiration time of each random clock, and reset kernels stochastically reassign continuous variables at discrete steps. On top of this, the paper defines HAwKsync templates, which add sending and receiving labels and separate input from output variables, so each Simulink subsystem becomes a small automaton. The load-bearing templates are the stochastic timer (a location where the output decreases at rate $-1$ and a self-loop resamples the output from the configured distribution) and the stochastic switch (two random clocks, one per input, whose expiration decides which input is passed to the output). The lifted parallel-composition rules combine templates: for synchronized edges the delay kernel comes from the sending edge and the reset kernels from all involved edges are merged, which is well-defined because each template owns its output variables. This machinery is what lets a composed SHA inherit both the continuous dynamics and the probabilistic behavior of the original Simulink model.

What would settle it

Feed the same distribution parameters to the stochastic timer block in Simulink and to the corresponding HAwK template, run both with the same input for many repetitions, and compare the empirical distribution of expiration times: the Simulink falling-edge re-trigger and the template's immediate self-loop resampling should produce identical timer-value traces if the semantics match. A more direct test is to run the automatic transformation end-to-end without the hand-optimizations described in the evaluation and check whether the confidence intervals for the energy-unit property $P(\lozenge\, total \geq 16000)$ still overlap those from Simulink, since that is the property where the current results only partially overlap.

Watch

Extended reading notes

Core claim

The paper's central claim is that the stochastic Simulink subsystems it defines have exact formal counterparts as HAwK templates, and that composing these templates with the lifted parallel-composition rules yields a monolithic stochastic hybrid automaton whose quantitative behavior matches the Simulink model. The paper presents templates for a stochastic timer, a stochastic switch, stochastic sampling, stochastic noise, and discrete and continuous aging, including variants with and without explicit repair signals. The delay and reset kernels of HAwK encode the random expiration times and the stochastic reassignments of variables, respectively. The evaluation compares statistical model checking on the automaton with simulation of the original Simulink models for a temperature control system with sensor loss and an energy measurement unit with stochastic switching. For most properties the confidence intervals from the automaton lie within those from Simulink simulation, with much smaller computational cost, and the paper concludes that this enables formal reasoning about safety and performance under uncertainty.

Load-bearing premise

The load-bearing premise is that each SHA template faithfully formalizes the semantics of its Simulink subsystem, especially the stochastic timer's immediate self-loop resampling and the stochastic switch's two-timer edge delays, and the paper gives no equivalence proof to back that premise.

Editorial extensions

If this is right

  • If the templates are faithful, safety properties such as 'the temperature never drops below 20' can be checked on the SHA with statistical model checking, and the resulting probability estimates transfer to the Simulink model.
  • Engineers can use the parameterizable subsystem library to inject aging, noise, sensor loss, or stochastic switching into existing Simulink models and still obtain formal, quantitative guarantees, instead of relying on the idealized model.
  • Because the SHA analysis ran in about 0.3 seconds versus 30 minutes for the temperature case and 12 minutes for the energy case, the approach makes it practical to run far more samples and obtain tighter confidence intervals.
  • The same composed SHA is not limited to statistical model checking; it is also a candidate for reachability analysis, so the paper's transformation opens the door to analysis techniques beyond simulation.

Reading between the lines

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

  • If the template semantics are later proved or validated, the same template pattern could be extended to other stochastic Simulink constructs such as Poisson arrivals, discrete random walks, or correlated noise, turning the library into a general uncertainty modeling language.
  • The evaluation's hand-optimized automata suggest that the automatic composition may currently produce larger or less efficient models; an automated end-to-end pipeline with equivalence checking would be needed before industrial deployment.
  • The rare-event property where the confidence intervals only partially overlap indicates that very small probabilities may be sensitive to the sampling tick or scheduler choice; rare-event simulation techniques could be combined with the SHA to sharpen those estimates.
  • A direct comparison between statistical model checking and a reachability analysis on the same SHA would test whether the stochastic guarantees extend beyond the SMC setting the paper evaluates.
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

4 major / 5 minor

Summary. The paper presents an approach for modeling uncertainties in Simulink by providing a library of stochastic subsystems (Stochastic Timer, Switching, Sampling, Noise, Discrete Aging, Continuous Aging) and formalizing them as stochastic hybrid automata (SHA). The authors extend a previously proposed Simulink-to-SHA transformation by lifting the parallel composition rules from LHACsync to HAwKsync and by giving SHA templates, called HAwK templates, for each stochastic subsystem. The approach is intended to enable quantitative analysis, such as statistical model checking, of Simulink models under uncertainty. The evaluation applies the resulting automata to two case studies, a temperature control system with sensor loss and an energy measurement unit with stochastic switching, comparing confidence intervals obtained from the modes statistical model checker with confidence intervals computed from Simulink simulation.

Significance. If the transformation rules are correct, the paper addresses a real and practically important gap: bringing stochastic uncertainties in Simulink models into a formal framework that supports quantitative verification. The proposed subsystem library is well motivated, the paper includes concrete HAwK templates for each subsystem, and the two case studies demonstrate a significant runtime advantage for the SHA-based analysis. The authors provide an artifact with models and scripts, which is a definite strength. The main limitation is that the central formalization claim is currently not substantiated: no correctness statement or proof links the semantics of the stochastic Simulink subsystems to the HAwK templates, and the empirical evaluation uses hand-optimized automata rather than the automatic transformation output. One quantitative result in Table 1 is also inconsistent with the accompanying text. These issues affect the load-bearing claim that quantitative results on the SHA transfer back to the original Simulink models.

major comments (4)
  1. [Sec. 4.2, Figs. 6-8] The paper states that the SHA templates 'formalize' the stochastic Simulink subsystems, but it gives no equivalence statement or proof. For instance, the stochastic timer template in Fig. 6a replaces the Simulink falling-edge re-trigger with an immediate self-loop resampling, and the stochastic switch template in Fig. 6b collapses two interacting timers into edge delays. It is not shown that the stochastic process induced by the HAwK is equivalent to the stochastic process induced by the corresponding masked Simulink subsystem, in either a distributional or a trace-based sense. This is load-bearing for the abstract's claim that the approach 'allows us to formally argue about safety and performance under uncertainty', because results obtained on the SHA can be transferred to the Simulink model only if the transformation is semantics-preserving. Please provide a precise correctness theorem (e.g., equivalence of reachability probabilities or of the induced stochastic processes) and its proof, or a clearly stated set of assumptions under which the templates are exact, together with a proof under those assumptions.
  2. [Sec. 5, Tables 1-2] The evaluation does not exercise the proposed transformation. The text says that the HAwKs shown in Figs. 10 and 12 have been hand-optimized to eliminate redundant or unused variables, locations and edges, so the confidence intervals in Tables 1 and 2 validate only those hand-built automata, not the automatic transformation rules of Sec. 4. Furthermore, Table 1 contradicts the accompanying sentence that all modes CIs lie within the Simulink CIs: for P(◇ tmp ≤ 20), modes reports [0.0497, 0.05885] while Simulink reports [0.0652, 0.0795], and the two intervals are disjoint. This is precisely the kind of discrepancy that would signal a semantic mismatch between the SHA and the Simulink model, and the paper does not discuss it. Please either run the unoptimized automatic transformation in the evaluation, or give a semantics-preservation argument for the applied optimizations, and in either case address the non-overlapping interval in Table 1.
  3. [Sec. 4.2, Fig. 6b] In the stochastic switch template, the expiration time of the clock that is currently inactive is sampled at the initial state or at the previous switch and then frozen, because the inactive random clock has rate 0. In the Simulink subsystem of Fig. 3b, the expiration time of the other timer is sampled anew at the instant the active timer expires. For the constant, state-independent distributions U(low,high) and N≥0 considered in the paper, the two mechanisms yield the same dwell-time distribution, but this equivalence is neither stated nor proved, and it fails if the delay kernels are made state-dependent, which the HAwK definition (Def. 2) allows. Please state explicitly that the templates are intended only for state-independent delay distributions and give the distributional equivalence argument, or modify the template so that resampling occurs at the correct state.
  4. [Appendix A.3, Definitions 5-6] The lifted composition rules for HAwKsync do not specify how the label of the resulting synchronized edge is chosen, nor how the random clock of a receiving edge is eliminated. In a HAwK, delay kernels are indexed by labels and each label has exactly one random clock; after synchronizing edges with different delay kernels, the receiving edge's clock must be handled consistently, and labels must be renamed so that the guard-disjointness condition for equal labels is preserved. Without this detail, the composed object is not unambiguously a HAwK, and the claim in Sec. 4.1 of a seamless integration into the existing transformation is not fully substantiated. The rules should be completed and, preferably, accompanied by a correctness argument for the composition itself.
minor comments (5)
  1. [Appendix A.3, Definition 4] The sentence 'Init assigns a pair of initial state and condition to each location l in Loc for each v in Varoutput' appears to mean that Init assigns the pair to each location, not to each variable; please rephrase.
  2. [Appendix A.3, Definition 6] Item 5 uses the undefined symbols Lsync,i and Lcomp; these should likely be Synci and Acomp, respectively.
  3. [Sec. 4.1] For synchronized edges, the text says the delay kernel from the sending edge is assigned to the new edge, but it does not state what happens to the delay kernels of the receiving edges; please clarify whether they are discarded and why this is correct.
  4. [Fig. 7b and Sec. 4.2] The text describing the stochastic noise template refers to edges e0-e3 while the figure appears to use e1-e3 inconsistently; please align the figure and the text.
  5. [Sec. 5, Tables 1-2] Please report the number of modes runs for the energy measurement case study as well, and state the seeds and schedulers used for both case studies, so that the experiments are fully reproducible.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the SHA templates are proposed formalizations and the modes-vs-Simulink comparison is a consistency check, not a fitted prediction.

full rationale

The paper's derivation chain runs from stochastic Simulink subsystems (Sec. 3) to HAwK templates (Sec. 4.2) and lifted composition rules (Sec. 4.1), then to SMC results with modes (Sec. 5). None of the target quantities, i.e., the safety and performance probabilities in Tables 1 and 2, are used to define the templates or their kernels; the distributions are taken from the subsystem masks and stated explicitly, e.g., 'The delay kernel is defined as Ψe0(σ)∼Dist1, Ψe1(σ)∼Dist2' for the stochastic switch. The CI comparison is an external consistency check against independent Simulink simulation, not a fit of parameters to data. The paper does rely on the authors' own earlier transformation [8] and DHA semantics [34,35], but these are prior formal definitions with stated assumptions that do not include the present case-study probabilities, so this is ordinary incremental self-citation rather than a load-bearing circular chain. The main weaknesses are validation gaps, not circularity: Sec. 5 states that the analyzed HAwKs are hand-optimized ('we have applied some optimizations to eliminate redundant or unused variables, locations and edges'), and Sec. 4.2 provides no equivalence proof between templates and Simulink subsystems (the stochastic switch template, Fig. 6b, initializes both clocks at zero and does not resample the inactive timer exactly as described in Sec. 3). An unproven or even incorrect template would be a correctness problem, not a tautology, so no circular step is exhibited and the score is 0.

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

The approach's contribution is exactly the set of templates and composition rules; the ledger shows that everything beyond the standard automata/probability theory is either assumed (Simulink semantics, composition correctness) or introduced by the paper (HAwKsync, the subsystems) without independent evidence.

assumptions (4)
  • domain assumption The informal semantics of Simulink blocks (integrator, relay, random number generator, triggered subsystems) are as implemented by MathWorks and are correctly captured by the proposed SHA templates.
    Sec. 2.1 and Sec. 3 describe the Simulink behavior informally; Sec. 4.2 maps it to templates without a proof of equivalence.
  • standard math The HAwK/DHA formalism and its semantics from Willemsen et al. [34,35] are correct and applicable.
    The paper builds on and extends this formalism (Sec. 2.2, Def. 2-3); if the underlying semantics were flawed, the transformation would inherit the flaw.
  • ad hoc to paper The lifted parallel composition rules for HAwKsync (Appendix A.3, Def. 5-6) preserve the behavior of the composed stochastic templates.
    The rules are stated without a correctness or compositionality proof; they are new in this paper.
  • ad hoc to paper The hand-optimized HAwK used in the evaluation (Figs. 10 and 12) are faithful instantiations of the automated transformation applied to the corresponding Simulink models.
    Sec. 5 states the authors "applied some optimizations to eliminate redundant or unused variables, locations and edges", so the link to the automated transformation is assumed, not demonstrated.
invented entities (2)
  • HAwKsync
    purpose: A synchronization-aware variant of HAwK with input/output variables and send/receive labels, used to define SHA templates that can be composed.
    Introduced in Sec. 4.1 and Appendix A.3; its only validation is the paper's own case studies.
  • Stochastic Simulink subsystems (Timer, Switching, Sampling, Noise, Discrete Aging, Continuous Aging)
    purpose: Reusable masked Simulink blocks that model uncertainties such as random delays, random switching, noise, and aging.
    Presented in Sec. 3; their semantics are defined only through the SHA templates in Sec. 4, with no external validation beyond the paper's two case studies.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata." pith.science (2026). https://pith.science/paper/LGU74S4Z

@misc{pith2026250614581,
  author       = {Pith},
  title        = {Pith review of: Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LGU74S4Z}},
  note         = {Machine review of arXiv:2506.14581}
}
read the original abstract

Simulink is widely used in industrial design processes to model increasingly complex embedded control systems. Thus, their formal analysis is highly desirable. However, this comes with two major challenges: First, Simulink models often provide an idealized view of real-life systems and omit uncertainties such as, aging, sensor noise or failures. Second, the semantics of Simulink is only informally defined. In this paper, we present an approach to formally analyze safety and performance of embedded control systems modeled in Simulink in the presence of uncertainty. To achieve this, we 1) model different types of uncertainties as stochastic Simulink subsystems and 2) extend an existing formalization of the Simulink semantics based on stochastic hybrid automata (SHA) by providing transformation rules for the stochastic subsystems. Our approach gives us access to established quantitative analysis techniques, like statistical model checking and reachability analysis. We demonstrate the applicability of our approach by analyzing safety and performance in the presence of uncertainty for two smaller case studies.

Figures

Figures reproduced from arXiv: 2506.14581 by the authors.

Figure 1
Figure 1. Simulink model of a temperature control system. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Simple Temperature Control Unit given as a HAwK. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Simulink Subsystems for Timer and Switching. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (12 more)
Figure 4
Figure 4. Figure 4: Simulink Subsystems for Sampling and Noise. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Simulink Subystems for Discrete and Continuous Aging. [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: SHA Templates for Timer and Switch. extended as follows: For non-synchronized edges we maintain the delay and reset kernels defined for this edge in the SHA templates. For synchronized edges, we assign the continuous kernel from the sending edge for the resulting synch…
Figure 7
Figure 7. Figure 7: SHA Templates for Sampling and Noise. as in2. Switching between these locations depends on the random clocks switch1 and switch2 . Initially, the value of in1 is assigned to out. Once the expiration time for switch1 is reached, the edge to l1 is taken immediately upon …
Figure 8
Figure 8. Figure 8: SHA Templates for Aging without Explicit Repair Signal. [PITH_FULL_IMAGE:figures/full_fig_p012_8.png]
Figure 9
Figure 9. Figure 9: Simulink Model for the Temperature Control System with Loss. [PITH_FULL_IMAGE:figures/full_fig_p013_9.png]
Figure 10
Figure 10. Figure 10: Temperature Control as HAwK. corresponding HAwK is shown in [PITH_FULL_IMAGE:figures/full_fig_p014_10.png]
Figure 12
Figure 12. Figure 12: Energy Measurement Unit as a HAwK. We analyzed whether the total energy consumption and the time spent at max load exceed certain thresholds [PITH_FULL_IMAGE:figures/full_fig_p015_12.png]
Figure 11
Figure 11. Figure 11: Simulink Model for the Energy Measurement System. [PITH_FULL_IMAGE:figures/full_fig_p015_11.png]
Figure 13
Figure 13. Figure 13: SHA Template for Stochastic Noise with Signal as Multiplier. [PITH_FULL_IMAGE:figures/full_fig_p021_13.png]
Figure 14
Figure 14. Figure 14: SHA Template for Stochastic Discrete Aging with Explicit Repair Signal. [PITH_FULL_IMAGE:figures/full_fig_p022_14.png]
Figure 15
Figure 15. Figure 15: SHA Template for Stochastic Continuous Aging with Explicit Repair [PITH_FULL_IMAGE:figures/full_fig_p022_15.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

38 extracted references · 25 canonical work pages

  1. [1]

    In: Bridging the Gap Between AI and Reality

    Adelt, J., Bruch, S., Herber, P., Niehage, M., Remke, A.: Shielded Learning for Resilience and Performance Based on Statistical Model Checking in Simulink. In: Bridging the Gap Between AI and Reality. pp. 94–118. Springer Nature (2024). https://doi.org/10.1007/978-3-031-46002-9_6

    work page doi:10.1007/978-3-031-46002-9_6 2024

  2. [2]

    In: Formal Methods

    Adelt, J., Liebrenz, T., Herber, P.: Formal Verification of Intelligent Hybrid Sys- tems that are modeled with Simulink and the Reinforcement Learning Toolbox. In: Formal Methods. LNCS, vol. 13047, pp. 349–366. Springer (2021). https: //doi.org/10.1007/978-3-030-90870-6_19

    work page doi:10.1007/978-3-030-90870-6_19 2021

  3. [3]

    Theoretical Computer Science 138, 3–34 (1995)

    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid sys- tems. Theoretical Computer Science 138, 3–34 (1995). https://doi.org/10.1016/ 0304-3975(94)00202-T Modeling Uncertainty in Simulink and SHA 23

    work page 1995

  4. [4]

    In: Hybrid systems, pp

    Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: An algo- rithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, pp. 209–229. Springer (1993). https://doi.org/10.1007/3-540-57318-6_30

    doi:10.1007/3-540-57318-6_30 1993

  5. [5]

    International Journal on Software Tools for Technology Transfer21(1), 87–104 (2019)

    Bak, S., Beg, O.A., Bogomolov, S., Johnson, T.T., Nguyen, L.V., Schilling, C.: Hybrid automata: from verification to implementation. International Journal on Software Tools for Technology Transfer21(1), 87–104 (2019)

    work page 2019

  6. [6]

    Logical Methods in Comp

    Bertrand,N.,Bouyer,P.,Brihaye,T.,Menet,Q.,Baier,C.,Grösser,M.,Jurdzinski, M.: Stochastic Timed Automata. Logical Methods in Comp. Science10 (2014). https://doi.org/10.2168/LMCS-10(4:6)2014

    doi:10.2168/lmcs-10(4:6)2014 2014

  7. [7]

    In: Leveraging Applications of Formal Methods, Verification and Validation

    Blohm, P., Fränzle, M., Herber, P., Kröger, P., Remke, A.: Towards probabilis- tic contracts for intelligent cyber-physical systems. In: Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification. pp. 26–47. Springer (2025). https://doi.org/10.1007/978-3-031-75380-0_3

    work page doi:10.1007/978-3-031-75380-0_3 2025

  8. [8]

    In: Integrated Formal Methods

    Blohm,P.,Herber,P.,Remke,A.:Towardsquantitativeanalysisofsimulinkmodels using stochastic hybrid automata. In: Integrated Formal Methods. pp. 172–193. Springer (2025). https://doi.org/10.1007/978-3-031-76554-4_10

    work page doi:10.1007/978-3-031-76554-4_10 2025

Show all 38 references
  1. [9]

    In: 24th Int

    Budde, C.E., D’Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: 24th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 10806, pp. 340–358. Springer (2018). https://doi...

    2018 doi

  2. [10]

    CoRR (2024)

    Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienhöft, P.: Sound statistical model checking for probabilities and expected rewards. CoRR (2024). https://doi.org/10.48550/ARXIV.2411.00559

    2024 doi arXiv

  3. [11]

    In: Provably Correct Systems, pp

    Chen, M., Han, X., Tang, T., Wang, S., Yang, M., Zhan, N., Zhao, H., Zou, L.: MARS: A toolchain for modelling, analysis and verification of hybrid systems. In: Provably Correct Systems, pp. 39–58. Springer (2017). https://doi.org/10.1007/ 978-3-319-48628-4_3

    2017

  4. [13]

    Energies 11, 306 (2018)

    Chiacchio, F., Famoso, F., D’Urso, D., Brusca, S., Aizpurua, J.I., Cedola, L.: Dy- namic performance evaluation of photovoltaic power plant by stochastic hybrid fault tree automaton model. Energies 11, 306 (2018). https://doi.org/10.3390/ en11020306

    2018

  5. [14]

    In: IEEE Trans

    Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verifica- tion. In: IEEE Trans. on Automatic Control. vol. 48(1), pp. 64–75. IEEE (2003). https://doi.org/10.1109/TAC.2002.806655

    2003

  6. [15]

    International Journal on Software Tools for Technology Transfer17(4), 397–415 (2015)

    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal smc tutorial. International Journal on Software Tools for Technology Transfer17(4), 397–415 (2015). https://doi.org/10.1007/s10009-014-0361-y

    2015 doi

  7. [16]

    Delicaris, J., Remke, A., Ábrahám, E., Schupp, S., Stübbe, J.: Maximizing reach- ability probabilities in rectangular automata with random events. Sci. Comput. Program. 240, 103213 (2025). https://doi.org/10.1016/J.SCICO.2024.103213

    2025

  8. [17]

    In: 17th Int

    Delicaris, J., Schupp, S., Ábrahám, E., Remke, A.: Maximizing reachability prob- abilities in rectangular automata with random clocks. In: 17th Int. Symposium on Theoretical Aspects of Software Engineering. LNCS, vol. 13931, pp. 164–182. Springer (2023). https://doi.org/10.100...

    2023 doi

  9. [18]

    In: 16th Int

    Delicaris, J., Stübbe, J., Schupp, S., Remke, A.: Realyst: A C++ tool for optimiz- ing reachability probabilities in stochastic hybrid systems. In: 16th Int. Conf. on 24 P. Blohm et al. Performance Evaluation Methodologies and Tools. vol. 539, pp. 170–182. Springer (2023). htt...

    2023 doi

  10. [19]

    In: International Symposium on Formal Methods

    Filipovikj, P., Mahmud, N., Marinescu, R., Seceleanu, C., Ljungkrantz, O., Lönn, H.: Simulink to uppaal statistical model checker: Analyzing automotive industrial systems. In: International Symposium on Formal Methods. pp. 748–756. Springer (2016). https://doi.org/10.1007/978-...

    2016 doi

  11. [20]

    In: Proceedings of the 16th Int

    Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th Int. Conf. on Hybrid Systems: Computation and Control. p. 203–212. ACM (2013). https://doi.org/10.1145/2461328.2461361

    2013

  12. [21]

    Fulton, N., Mitsch, S., Quesel, J.D., Völp, M., Platzer, A.: KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In: Int. Conference on Automated Deduction. LNCS, vol. 9195, pp. 527–538. Springer (2015). https: //doi.org/10.1007/978-3-319-21401-6_36

    2015 doi

  13. [22]

    In: Verification of digital and hybrid systems, pp

    Henzinger, T.A.: The theory of hybrid automata. In: Verification of digital and hybrid systems, pp. 265–292. Springer (2000). https://doi.org/10.1007/ 978-3-642-59615-5_13

    2000

  14. [23]

    Henzinger,T.A.,Kopke,P.W.,Puri,A.,Varaiya,P.:What’sdecidableabouthybrid automata? Journal of computer and system sciences57(1), 94–124 (1998)

    1998

  15. [24]

    London (2014)

    Klenke, A.: Probability Theory: A Comprehensive Course. London (2014). https: //doi.org/10.1007/978-1-4471-5361-0{_}1

    2014 doi

  16. [25]

    Kuriakose, R.B., Vermaak, H.J.: Customized mixed model stochastic assembly line modelling using simulink. Int. Journal of Simulation Systems Science & Technology 20(1), 61–69 (2019). https://doi.org/10.5013/IJSSST.a.20.S1.06

    2019 doi

  17. [26]

    In: Formal Techniques for Safety-Critical Systems: 4th In- ternational Workshop

    Legay, A., Traonouez, L.M.: Statistical model checking of simulink models with Plasma Lab. In: Formal Techniques for Safety-Critical Systems: 4th In- ternational Workshop. pp. 259–264. Springer (2016). https://doi.org/10.1007/ 978-3-319-29510-7_15

    2016

  18. [27]

    Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X. In: Int. Conference on For- mal Engineering Methods. LNCS, vol. 11232, pp. 89–105. Springer (2018). https: //doi.org/10.1007/978-3-030-02450-5_6

    2018 doi

  19. [28]

    Liebrenz, T., Herber, P., Glesner, S.: A service-oriented approach for decomposing and verifying hybrid system models. In: Int. Conference on Formal Aspects of Component Software. LNCS, vol. 12018, pp. 127–146. Springer (2019). https:// doi.org/10.1007/978-3-030-40914-2_7

    2019 doi

  20. [29]

    European Journal of Control16(6), 583–594 (2010)

    Lygeros, J., Prandini, M.: Stochastic Hybrid Systems: A Powerful Framework for Complex, Large Scale Applications. European Journal of Control16(6), 583–594 (2010). https://doi.org/10.3166/ejc.16.583-594

    2010 doi

  21. [30]

    Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: Int. Conf. on Hybrid Systems: Computation and Control. pp. 93–98. ACM (2016). https://doi.org/10.1145/2883817.2883826

    2016

  22. [31]

    Journal of Automated Reasoning 41(2), 143–189 (2008)

    Platzer, A.: Differential dynamic logic for hybrid systems. Journal of Automated Reasoning 41(2), 143–189 (2008). https://doi.org/10.1007/s10817-008-9103-8

    2008 doi

  23. [32]

    ACM Trans- actions on Modeling and Computer Simulation33(4) (2023)

    da Silva, C., Schupp, S., Remke, A.: Optimizing reachability probabilities for a re- stricted class of stochastic hybrid automata via flowpipe-construction. ACM Trans- actions on Modeling and Computer Simulation33(4) (2023). https://doi.org/10. 1145/3607197

    2023

  24. [33]

    https://de.mathworks.com/products/simulink.html

    The MathWorks: Simulink. https://de.mathworks.com/products/simulink.html

  25. [34]

    In: Quantitative Evaluation of Systems - 20th Modeling Uncertainty in Simulink and SHA 25 Int

    Willemsen, L., Remke, A., Ábrahám, E.: Comparing two approaches to include stochasticity in hybrid automata. In: Quantitative Evaluation of Systems - 20th Modeling Uncertainty in Simulink and SHA 25 Int. Conf. pp. 238–254. Lecture Notes in Computer Science, Springer (2023). ht...

    2023 doi

  26. [35]

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

    Willemsen, L., Remke, A., Ábrahám, E.: (de-)composed and more: Eager and lazy specifications (camels) for stochastic hybrid systems. In: Principles of Verification: Cycling the Probabilistic Landscape : Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthd...

    2025

  27. [36]

    Journal of the American Statistical Association 22(158), 209–212 (1927)

    Wilson, E.: Probable inference, the law of succession, and statistical inference. Journal of the American Statistical Association 22(158), 209–212 (1927). https: //doi.org/10.2307/2276774

    1927 doi

  28. [37]

    Zou, L., Zhan, N., Wang, S., Fränzle, M.: Formal Verification of Simulink/Stateflow Diagrams. In: Int. Symposium on Automated Technology for Verification and Analysis. pp. 464–481. LNCS, Springer (2015). https://doi.org/10.1007/ 978-3-319-47016-0

    2015

  29. [38]

    In: Proceedings of the 15th ACM Int

    Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: Proceedings of the 15th ACM Int. Conf. on Hybrid Systems: Com- putation and Control. p. 217–226. ACM (2012). https://doi.org/10.1145/2185632. 2185665

    2012 doi

  30. [39]

    Formal Methods in System Design pp

    Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow/simulink verification. Formal Methods in System Design pp. 338–367 (2013). https://doi.org/10.1007/s10703-013-0195-3

    2013 doi

Pith tools

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