pith. machine review for the scientific record. sign in

arxiv: 2604.24440 · v1 · submitted 2026-04-27 · 💻 cs.FL · cs.SY· eess.SY

Recognition: unknown

Minimum Reachability Probabilities in Rectangular Automata with Random Clocks

Joanna Delicaris , Erika \'Abrah\'am , Anne Remke
Authors on Pith no claims yet

Pith reviewed 2026-05-07 17:09 UTC · model grok-4.3

classification 💻 cs.FL cs.SYeess.SY
keywords rectangular automatarandom clocksreachability probabilitieslower boundsprophetic schedulinghybrid systemssafety verificationcyber-physical systems
0
0 comments X

The pith

Lower bounds on reachability probabilities can now be computed for rectangular automata with random clocks by separating stochastic and nondeterministic choices.

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

The paper establishes a method for calculating the smallest possible probability that executions in rectangular automata with random clocks reach target states under prophetic scheduling. These models describe cyber-physical systems that combine continuous physical behavior with stochastic timing uncertainty. Existing analysis only produces upper bounds, which support optimistic best-case safety checks. The new technique yields lower bounds instead, which are required to prove that safety holds even under the most adverse choices. The method works by making an explicit split between random clock events and nondeterministic scheduling decisions when exploring reachable executions.

Core claim

Lower bounds on reachability probabilities are obtained by a reachability analysis that explicitly separates stochastic and nondeterministic choices along executions in rectangular automata with random clocks under prophetic scheduling, providing worst-case guarantees that complement the upper-bound results already available for the same model class.

What carries the argument

Explicit separation of stochastic and nondeterministic choices along executions, which constructs a structure from which minimum probabilities can be derived without loss of completeness.

If this is right

  • Safety-critical cyber-physical systems can obtain guaranteed minimum probabilities of reaching safe or unsafe states.
  • The electric vehicle charging example shows that the method produces meaningful numerical worst-case guarantees in practice.
  • Both upper and lower bounds become available, allowing the actual probability to be bracketed.
  • Formal analysis now supports reliable control decisions when continuous dynamics and stochastic uncertainty are both present.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The separation technique could be adapted to other hybrid automata classes if similar disentanglement of choices remains feasible.
  • Pairing the new lower bounds with existing upper bounds would give interval estimates on reachability probabilities.
  • The implemented procedure could be incorporated into existing model checkers for probabilistic hybrid systems.

Load-bearing premise

That an explicit separation of stochastic and nondeterministic choices along executions can be performed while preserving completeness and without introducing assumptions absent from the original model.

What would settle it

A concrete rectangular automaton with random clocks for which the method produces a numerical lower bound that exceeds the true minimum reachability probability under some prophetic schedule.

Figures

Figures reproduced from arXiv: 2604.24440 by Anne Remke, Erika \'Abrah\'am, Joanna Delicaris.

Figure 1
Figure 1. Figure 1: Computation of minimum reachability probabilities (within the gray box). view at source ↗
Figure 2
Figure 2. Figure 2: Running Example: RAC model with reachable state space in view at source ↗
Figure 3
Figure 3. Figure 3: Operational semantics for a RAC R. We call |π| = n the length of π, define last(π) = σn and let RunsR be the set of all runs of R. We call π initial if ν0 ∈ Init(ℓ0), (ν0)r = 0, and (s0)r ∈ supp(Distr (r)) for all r ∈ Lab. Let Runs Init R be the set of all initial runs of R. A state σ = (ℓ, ν, s) is reachable in R if there exists an initial run π with last(π) = σ. The above semantics is dedicated for RAC w… view at source ↗
Figure 4
Figure 4. Figure 4: Running Example: Reach tree and enabling prophecies. view at source ↗
Figure 5
Figure 5. Figure 5: Additional fragments of RAC that cause different branchings. view at source ↗
Figure 6
Figure 6. Figure 6: Steps of the minimum approach, detailing the gray box in Figure 1. view at source ↗
Figure 7
Figure 7. Figure 7: Running Example: Exposing the choice to stay in view at source ↗
Figure 8
Figure 8. Figure 8: Running Example: Splitting of a mixed branching at view at source ↗
Figure 9
Figure 9. Figure 9: Computation times for the rectangular variant of view at source ↗
Figure 10
Figure 10. Figure 10: Mixed branching at node i with three children j1, j2, j3, where j1 and j3 are reached by competing random events r and q view at source ↗
Figure 11
Figure 11. Figure 11: Separating and splitting of enabling prophecies. view at source ↗
Figure 12
Figure 12. Figure 12: Reduced illustrations for RAC RA, RB, RC and RD, which omit Init(ℓ0) = 0d , and the flow of x ∈ Var if Flow(ℓ)x = 0 view at source ↗
Figure 13
Figure 13. Figure 13: RAC for the CAR case study view at source ↗
read the original abstract

Control applications for cyber-physical systems must make reliably safe control decisions in the presence of continuous dynamics as well as stochastic uncertainty. Providing safety guarantees for such systems requires formal modeling and analysis techniques that capture these aspects. For modeling, in this paper we consider rectangular automata with random clocks under prophetic scheduling. For this model class, existing methods can compute only upper bounds on reachability probabilities, enabling optimistic, best-case safety reasoning. We complement this view by introducing a novel method to compute lower bounds, thereby enabling worst-case analysis that is essential for safety-critical applications. Although both upper and lower bounds rely on reachability analysis, they are not dual: computing lower bounds requires an explicit separation of stochastic and nondeterministic choices along executions. We implement our approach and demonstrate its practical feasibility on an electric vehicle charging scenario, showing that meaningful worst-case guarantees can be obtained.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces a method to compute lower bounds on reachability probabilities for rectangular automata with random clocks under prophetic scheduling. The key idea is an explicit separation of stochastic clock resolutions from nondeterministic rectangular dynamics (derivative intervals, guards, invariants) along executions, which is claimed to enable worst-case analysis. The approach is implemented and demonstrated on an electric vehicle charging scenario, showing that meaningful worst-case guarantees can be obtained.

Significance. If the separation is shown to preserve the infimum over all measurable prophetic schedulers, the work would usefully complement existing upper-bound techniques for hybrid systems with stochastic elements, supporting full interval-based safety reasoning in cyber-physical systems. The practical implementation on a realistic EV charging scenario is a concrete strength, as is the focus on prophetic scheduling for safety-critical applications.

major comments (1)
  1. [Abstract and method description] Abstract and method description: The central claim that explicit separation of stochastic and nondeterministic choices computes the true infimum reachability probability requires a formal argument that the construction (product or unfolding) preserves all measurable history-dependent schedulers, including those that correlate nondeterministic choices with exact random-clock values in the continuous state space. Without such an argument or a proof that no adversarial power is lost, the reported lower bounds may apply only to a restricted scheduler class and could be strictly larger than the true minimum.
minor comments (2)
  1. [Abstract] The abstract states that 'both upper and lower bounds rely on reachability analysis' but does not clarify how the lower-bound procedure reuses or differs from the upper-bound reachability engine in implementation details.
  2. [Implementation and evaluation] The demonstration on the electric vehicle charging scenario reports 'meaningful worst-case guarantees' but provides no quantitative comparison to upper bounds, no error bounds on the computed probabilities, and no discussion of scalability beyond the single scenario.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of our manuscript and for the constructive feedback. We appreciate the positive remarks on the practical demonstration and the relevance to safety-critical applications. We address the single major comment below.

read point-by-point responses

  1. Referee: Abstract and method description: The central claim that explicit separation of stochastic and nondeterministic choices computes the true infimum reachability probability requires a formal argument that the construction (product or unfolding) preserves all measurable history-dependent schedulers, including those that correlate nondeterministic choices with exact random-clock values in the continuous state space. Without such an argument or a proof that no adversarial power is lost, the reported lower bounds may apply only to a restricted scheduler class and could be strictly larger than the true minimum.

    Authors: We agree that a rigorous formal argument is required to establish that the separation construction computes the true infimum over all measurable prophetic schedulers. The current manuscript provides an informal justification based on the explicit separation along executions and the rectangular dynamics, but this is insufficient to fully address the concern regarding history-dependent schedulers that may correlate nondeterministic decisions with precise random-clock values. In the revised version we will add a dedicated proof subsection showing that the product/unfolding construction preserves the infimum: any measurable history-dependent prophetic scheduler can be simulated by a scheduler in the separated model without loss of power, by lifting decisions to the augmented state that tracks clock resolutions explicitly. This leverages the independence of clock sampling and the rectangular invariants/guards to ensure equivalence. revision: yes

Circularity Check

0 steps flagged

No circularity: lower-bound method relies on explicit separation independent of upper bounds

full rationale

The abstract states that lower bounds require an explicit separation of stochastic and nondeterministic choices along executions, and that this is not dual to the upper-bound techniques. No equations, fitted parameters, self-citations, or ansatzes are exhibited in the provided text that would make the claimed minimum reachability probability reduce to its inputs by construction. The derivation is presented as a novel, self-contained construction for the model class, with no load-bearing reliance on prior author results that themselves lack independent verification.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard properties of rectangular automata, random clocks, and reachability analysis under prophetic scheduling; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Rectangular automata with random clocks admit reachability analysis that can be decomposed by separating stochastic and nondeterministic transitions.
    Invoked when stating that lower-bound computation requires explicit separation of choices.

pith-pipeline@v0.9.0 · 5451 in / 1267 out tokens · 65198 ms · 2026-05-07T17:09:42.500719+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references · 17 canonical work pages

  1. [1]

    Theoretical Computer Science138(1), 3–34 (1995).https://doi.org/10.1016/ 0304-3975(94)00202-T

    Alur, R., Courcoubetis, C.A., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science138(1), 3–34 (1995).https://doi.org/10.1016/ 0304-3975(94)00202-T

    1995

  2. [2]

    In: Proc

    Ballarini, P., Bertrand, N., Horv´ ath, A., Paolieri, M., Vicario, E.: Transient analysis of networks of stochastic timed automata using stochastic state classes. In: Proc. of the 10th Int. Conf. on Quantitative Evaluation of Systems. LNCS, vol. 8054, pp. 355–371. Springer (2013).https://doi.org/10.1007/978-3-642-40196-1_30

    work page doi:10.1007/978-3-642-40196-1_30 2013

  3. [3]

    Logical Methods in Computer Science10(4), 1–73 (2014).https://doi.org/10.2168/LMCS-10(4:6)2014 Minimum Reachability Probabilities in RAC 21

    Bertrand, N., Bouyer, P., Brihaye, T., Menet, Q., Baier, C., Gr¨ oßer, M., Jurdzinski, M.: Stochastic timed automata. Logical Methods in Computer Science10(4), 1–73 (2014).https://doi.org/10.2168/LMCS-10(4:6)2014 Minimum Reachability Probabilities in RAC 21

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

  4. [4]

    IEEE Transac- tions on Software Engineering32(10), 812–830 (2006).https://doi.org/10.1109/ TSE.2006.104

    Bohnenkamp, H., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: A com- positional modeling formalism for hard and softly timed systems. IEEE Transac- tions on Software Engineering32(10), 812–830 (2006).https://doi.org/10.1109/ TSE.2006.104

    2006

  5. [5]

    In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S.E., Thomas, W

    Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S.E., Thomas, W. (eds.) Au- tomata, Languages and Programming, 36th Int. Colloquium. LNCS, vol. 5556, pp. 103–114. Springer (2009).https://doi.org/10.1007/978-3-642-02930-1_9

    work page doi:10.1007/978-3-642-02930-1_9 2009

  6. [6]

    In: Proc

    Cauchi, N., Abate, A.: StocHy: Automated verification and synthesis of stochas- tic processes. In: Proc. of the 25th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19). pp. 247–264. Springer (2019). https://doi.org/10.1145/3302504.3313349

    work page doi:10.1145/3302504.3313349 2019

  7. [7]

    In: Proc

    D’Argenio, P.R., Gerhold, M., Hartmanns, A., Sedwards, S.: A Hierarchy of Scheduler Classes for Stochastic Automata. In: Proc. of 21st Int. Conference on Foundations of Software Science and Computation Structures (FOSSACS 2018). LNCS, vol. 10803, pp. 384–402. Springer (2018).https://doi.org/10. 1007/978-3-319-89366-2_21

    2018

  8. [8]

    Delicaris, J., Remke, A., ´Abrah´ am, E., Schupp, S., St¨ ubbe, 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

    work page doi:10.1016/j.scico.2024.103213 2025

  9. [9]

    In: Proc

    Delicaris, J., Schupp, S., ´Abrah´ am, E., Remke, A.: Maximizing reachability probabilities in rectangular automata with random clocks. In: Proc. of the 17th Int. Symp. on Theoretical Aspects of Software Engineering (TASE’23). LNCS, vol. 13931, pp. 164–182. Springer (2023).https://doi.org/10.1007/ 978-3-031-35257-7_10

    2023

  10. [10]

    In: Proc

    Delicaris, J., St¨ ubbe, J., Schupp, S., Remke, A.: RealySt: A C++ tool for optimiz- ing reachability probabilities in stochastic hybrid systems. In: Proc. of the 16th EAI Int. Conf. on Performance Evaluation Methodologies and Tools. LNCS, vol. 539, pp. 170–182. Springer (2023).https://doi.org/10.1007/978-3-031-48885-6_11

    work page doi:10.1007/978-3-031-48885-6_11 2023

  11. [11]

    org/10.5281/zenodo.18990721

    Delicaris, J., ´Abrah´ am, E., Remke, A.: Artifact for: Minimum reachability prob- abilities in rectangular automata with random clocks (Mar 2026).https://doi. org/10.5281/zenodo.18990721

    work page doi:10.5281/zenodo.18990721 2026

  12. [12]

    Formal Meth- ods in System Design43(2), 191–232 (2013).https://doi.org/10.1007/ s10703-012-0167-z

    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Meth- ods in System Design43(2), 191–232 (2013).https://doi.org/10.1007/ s10703-012-0167-z

    2013

  13. [13]

    https://doi.org/10.1006/jcss.1998.1581

    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hy- brid automata? Journal of Computer and System Sciences57(1), 94–124 (1998). https://doi.org/10.1006/jcss.1998.1581

    work page doi:10.1006/jcss.1998.1581 1998

  14. [14]

    IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans38(2), 385–396 (2008).https://doi.org/10.1109/TSMCA

    Koutsoukos, X.D., Riley, D.: Computational methods for verification of stochastic hybrid systems. IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans38(2), 385–396 (2008).https://doi.org/10.1109/TSMCA. 2007.914777

    work page doi:10.1109/tsmca 2008

  15. [15]

    In: Proc

    Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Proc. of the 11th Int. Conf. on Concurrency Theory. LNCS, vol. 1877, pp. 123–137. Springer (2000). https://doi.org/10.1007/3-540-44618-4_11

    work page doi:10.1007/3-540-44618-4_11 2000

  16. [16]

    Information and Computation205(7), 1027–1077 (2007).https://doi.org/https://doi.org/10.1016/j.ic.2007.01.004 22 J

    Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Information and Computation205(7), 1027–1077 (2007).https://doi.org/https://doi.org/10.1016/j.ic.2007.01.004 22 J. Delicaris et al

    work page doi:10.1016/j.ic.2007.01.004 2007

  17. [17]

    Jour- nal of Computational Physics27(2), 192–203 (1978).https://doi.org/10.1016/ 0021-9991(78)90004-9

    Lepage, G.P.: A new algorithm for adaptive multidimensional integration. Jour- nal of Computational Physics27(2), 192–203 (1978).https://doi.org/10.1016/ 0021-9991(78)90004-9

    1978

  18. [18]

    Niehage, M.: SMC-Based Learning meets Simulation on a Symbolic State-Space in Hybrid Petri Nets. Ph.D. thesis, University of M¨ unster, M¨ unster, Germany (2025)

    2025

  19. [19]

    In: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design

    Niehage, M., Hartmanns, A., Remke, A.: Learning optimal decisions for stochastic hybrid systems. In: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design. pp. 44–55. ACM (2021).https://doi.org/10. 1145/3487212.3487339

    work page arXiv 2021

  20. [20]

    Master’s thesis, University of M¨ unster, M¨ unster, Germany

    Petri, A.: Computing Minimal Reachability Probabilities for Rectangular Hybrid Automata with Random Clocks through Backwards Partition Refinement. Master’s thesis, University of M¨ unster, M¨ unster, Germany

  21. [21]

    In: Proc

    Pilch, C., Schupp, S., Remke, A.: Optimizing reachability probabilities for a re- stricted class of stochastic hybrid automata via flowpipe-construction. In: Proc. of the 18th Int. Conference on Quantitative Evaluation of Systems (QEST’21). pp. 435–456 (2021).https://doi.org/10.1007/978-3-030-85172-9_23

    work page doi:10.1007/978-3-030-85172-9_23 2021

  22. [22]

    In: 12th International Symposium on NASA Formal Methods

    Pilch, C., Krause, M., Remke, A., ´Abrah´ am, E.: A transformation of hybrid petri nets with stochastic firings into a subclass of stochastic hybrid automata. In: 12th International Symposium on NASA Formal Methods. pp. 381–400. LNCS, Springer (2020).https://doi.org/10.1007/978-3-030-55754-6_23

    work page doi:10.1007/978-3-030-55754-6_23 2020

  23. [23]

    In: Stochastic Hybrid Systems: Theory and Safety Critical Applica- tions, LNCS, vol

    Prandini, M., Hu, J.: A stochastic approximation method for reachability com- putations. In: Stochastic Hybrid Systems: Theory and Safety Critical Applica- tions, LNCS, vol. 337, pp. 107–139. Springer (2006).https://doi.org/10.1007/ 11587392_4

    2006

  24. [24]

    In: Proc

    Schupp, S., ´Abrah´ am, E., Makhlouf, I.B., Kowalewski, S.: HyPro: A C++ library of state set representations for hybrid systems reachability analysis. In: Proc. of NFM’17, vol. 10227, pp. 288–294. Springer (2017).https://doi.org/10.1007/ 978-3-319-57288-8_20

    2017

  25. [25]

    ACM Trans

    da Silva, C., Schupp, S., Remke, A.: Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe construction. ACM Trans. Model. Comput. Simul.33(4), 18:1–18:27 (2023).https://doi.org/10. 1145/3607197

    2023

  26. [26]

    In: Proc

    Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST2: Formal Abstractions of Uncountable-STate STochastic processes. In: Proc. of the 21st Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15). LNCS, vol. 9035, pp. 272–286. Springer (2015).https://doi.org/10.1007/ 978-3-662-46681-0_23

    2015

  27. [27]

    In: Proc

    Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Proc. of the 6th Int. Symp. on Formal Techniques in Real-Time and Fault- Tolerant Systems (FTRTFT’00). LNCS, vol. 1926, pp. 31–45. Springer (2000). https://doi.org/10.1007/3-540-45352-0_5

    work page doi:10.1007/3-540-45352-0_5 1926

  28. [28]

    Sproston, J.: Verification and control for probabilistic hybrid automata with finite bisimulations. J. Log. Algebraic Methods Program.103, 46–61 (2019).https: //doi.org/10.1016/j.jlamp.2018.11.001

    work page doi:10.1016/j.jlamp.2018.11.001 2019

  29. [29]

    In: 27th Int

    St¨ ubbe, J., Remke, A., ´Abrah´ am, E.: Scaling up reachability analysis for rectan- gular automata with random clocks. In: 27th Int. Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2025). pp. 21–29 (2025). https://doi.org/10.1109/SYNASC69064.2025.00011 Minimum Reachability Probabilities in RAC 23 A Appendix A.1 Reach Tree D...

    work page doi:10.1109/synasc69064.2025.00011 2025