Pith. sign in

REVIEW 3 major objections 3 minor 36 references

For models with unbounded timers, resampling collapses time-sensitive importance functions to ordinary distance metrics, while a global-age timer prunes doomed simulation runs.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-01 16:33 UTC pith:YFGDBNZP

load-bearing objection Solid theory, shaky empirics: the collapse theorem and taxonomy are worth keeping, but the m_s depth-limit and m_l ground truth need fixes. the 3 major comments →

arxiv 2607.17939 v1 pith:YFGDBNZP submitted 2026-07-20 stat.ME cs.LOcs.PF

A Taxonomy of Distance Metrics for Time-Sensitive Importance Splitting: Timer Bounds, Resampling, and the Global Age

Gabriel Dengler , Carlos E. Budde , Laura Carnevali This is my paper
classification stat.ME cs.LOcs.PF
keywords importance splittingrare event simulationnon-Markovian modelstime-sensitive importance functionstimer resamplingglobal agedistance metricsstate classes
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Rare-event simulation by importance splitting needs an importance function (IFUN) that estimates how far a simulation state is from the target. In non-Markovian models—systems with non-exponential timers—the authors make IFUNs time-sensitive by using concrete timer values, but then a state looks important only when specific timer samples line up, so most runs are wasted. This paper proposes two fixes: resampling timers conditioned on how long they have already run, so importance is judged by the whole set of feasible timer values, and tracking the global age (the remaining time budget) as an artificial timer, so runs that cannot reach the target are pruned early. The central result is a theorem stating that in models with unbounded timer domains, the order-based time-sensitive metric under resampling equals the ordinary distance metric, making the cheaper metric sufficient. A taxonomy orders the resulting metrics by how much information they use, and experiments on repairable fault trees and a tandem queue show improved estimator accuracy.

Core claim

The paper establishes a collapse theorem: for every state s, d(s) = d_r^O(s) when every timer has domain [0,∞). Here d is the ordinary distance metric counting the minimum number of transitions to the target, and d_r^O is the ordered time-sensitive distance evaluated after resampling, which asks for the minimum distance over any timer values consistent with the elapsed times and ignores exact timer bounds except their order. Because resampling can always perturb an unbounded timer to fit any ordering, the time dimension adds no information; the cheaper ordinary metric is enough. The paper also introduces a global-age timer recording the remaining time budget, extends each metric to time-boun

What carries the argument

The central object is the state class, a set of timer evaluations in a location encoded as a difference-bound matrix (DBM) zone; distance metrics are computed by backwards reachability over a graph of such classes. For resampling, the elapsed time of each timer induces a state class of feasible resampled values, so importance is the minimum distance over that class. For unbounded timers, each DBM zone can be replaced by elementary state classes storing only the order in which timers fire, indexed by a permutation code; this gives the ordered metric d^O. The load-bearing identity is Theorem 1, d(s)=d_r^O(s), together with a partial order d_A ⪰ d_B meaning a finer metric gives distances at lea

Load-bearing premise

The experimental demonstration of improved accuracy on the small fault tree assumes that a backwards search depth of 12 covers every state relevant to the target, a heuristic used because the full graph did not terminate within five minutes; if deeper states matter, the reported gains could be artifacts of truncation, unlike the two other models where the full graph is built.

What would settle it

For Theorem 1, take a small model with all unbounded timers and compute d and d_r^O at every reachable state by exhaustive search; any state with unequal values refutes the collapse. For the experimental claim, rebuild the small fault tree's backwards graph with depth exceeding 12 and re-run the splitting; if relative errors or the ranking of importance functions change materially, the depth-12 truncation affected the conclusions.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Practitioners with unbounded timers can compute the ordinary distance metric instead of the ordered time-sensitive one under resampling, saving the cost of DBM-zone search without changing the importance values.
  • The granularity partial order predicts relative efficiency: a finer metric, such as a timed metric with bounds, cannot underestimate distance relative to a coarser one, so it may direct splitting better but costs more to compute; the paper's comparisons respect this order.
  • Global-age pruning increases the number of simulation runs that can be completed within a fixed budget when a time bound makes many states unreachable, and can shrink the backwards reachability graph.
  • Under resampling, all initial states share the same elapsed-time information, so threshold selection no longer needs rejection sampling of low-importance initial states.
  • Experiments support these predictions: on fault trees with bounded timers, timed metrics outperformed order metrics; on the unbounded-timer model, resampling produced the largest gains; on the symmetric queue, pruning helped most.

Where Pith is reading between the lines

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

  • If the collapse theorem extends to other importance heuristics, the practical role of time-sensitive IFUNs may be confined to bounded timer domains; for unbounded domains, resampling alone could be the main lever, potentially simplifying future implementations.
  • The depth-12 truncation used for the small fault tree means its reported accuracy improvements are conditional; a natural robustness check is to re-run with the backwards graph built to larger depth and see if the ranking of IFUNs survives.
  • A mixture scheme that resamples only a subset of timers, mentioned as future work in the paper, could interpolate between full simulation and state-class analysis, potentially giving tighter variance bounds on the experimental improvements.
  • The taxonomy's granularity order could serve as a design guide for automated importance-function synthesis: choose the coarsest metric that still separates states on the path to the target, trading information depth against computational overhead.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 3 minor

Summary. The paper studies importance splitting for non-Markovian rare-event simulation. It introduces resampling of timers conditioned on elapsed time and a global-age timer for time-bounded reachability, leading to a taxonomy of distance metrics (time-agnostic vs. order vs. timed; with/without resampling; with/without global age). The main theoretical result (Theorem 1) states that for models with unbounded timer domains, the order-based distance under resampling equals the ordinary time-agnostic distance. Theorem 2 establishes a granularity partial order among the metrics. The experimental section compares 13 IFUNs on two fault trees and a tandem queue, reporting relative errors of 95% confidence intervals from 20-minute runs.

Significance. The taxonomy is a useful conceptual clarification of a previously ad-hoc area, and Theorem 1, if correct, has immediate practical value: under resampling and unbounded timers, practitioners can use the cheaper ordinary distance metric. The proof in Appendix C is concise and largely self-contained. The paper also ships an artifact (DOI) and reports detailed per-run tables. However, the experimental validation currently contains two load-bearing reporting gaps—the unsupported ground truth for m_l and the unproven depth truncation for m_s—so the quantitative claims should be read with caution.

major comments (3)
  1. [Sec. 6.3 / Table 3 (m_l)] The text states φ_mℓ≈2.2e-8 from a 12-hour CMC run, but Table 3's m_l CMC row reports 1.71e7 runs, a non-zero runs ratio of 0, and no center/half-width. A zero-success CMC run does not support a point estimate of 2.2e-8; the expected number of successes under that probability is only ≈0.38. Unless a different, unreported CMC run (or external computation) produced 2.2e-8, every relative error in the m_l panel is normalized by an unsupported constant. Please report the actual CMC result used, with sample count and successes, or remove the quantitative claims for m_l.
  2. [App. E.4 / Sec. 6.3 (m_s)] For m_s the full timed SC graph ω_T does not terminate in five minutes, so the authors cap expansion depth at 12 using a 'high-level perspective' that at most 10 transitions are needed. This is a heuristic, not a proof, and Sec. 4 itself states that an unbiased result requires the SC graph to be fully constructed. If any state reachable within T=1248 has true distance >12, it is treated as unreachable, and the relative-error advantage of tsen_timed over tsen_order in Fig. 7 could be an artifact of truncation. Please either prove the bound for this model, construct the full graph with a longer budget, or provide an empirical completeness check (e.g., inspect the frontier of the truncated graph).
  3. [App. C, proof of Theorem 2(1)] The proof of d_r^OG≡d_r^OEG asserts that 'a simulation run can always stay in a target state infinitely long (as no upper bounds on the timers exist)'. Definition 1 does not guarantee that target locations are absorbing; timers enabled in the target location may have positive probability of firing before the time bound, and the global-age timer is fixed and not resampled. The argument needs a rigorous treatment of the target location's timers and of the exact-transient semantics, or the statement should be restricted to models where the target is absorbing. This does not affect Theorem 1, but it is a gap in the taxonomy's equivalence claim.
minor comments (3)
  1. [Section 3.1, Def. 10] The statement 'trivially, there exist |T_l|! elementary SCs' ignores ties in timer values; the permutation is not unique on measure-zero boundaries. A remark that boundary overlap does not affect distances for continuous distributions would clarify.
  2. [Section 4, Def. 11 and Example 3] The global-age timer is first described as 'recording the remaining time budget', but Example 3's constraints (e.g., 9.8≤τ(t_age) and 9.8≤τ(t_age)-τ(t_u_x)) indicate τ(t_age) counts elapsed time from the start. The sign convention should be made consistent, or the definition should explicitly say that the remaining budget is t_max_age - τ(t_age).
  3. [Fig. 7] The upper panel's axis labels and legend are difficult to read, and the CMC bar for m_l is uninformative given the zero-success run in Table 3. Please improve figure clarity and note this limitation in the caption.

Circularity Check

0 steps flagged

No significant circularity: the main theorem and taxonomy follow from the paper's own definitions, and the experimental claims are measured against CMC ground truth rather than fitted to the conclusions.

full rationale

Theorem 1 is derived, not assumed: d(s) is the location-level distance, d_O(s) is the order-based metric over elementary SCs, and d_r^O(s) is the minimum of d_O over the induced SC Sigma_selp. For unbounded timers, Sigma_selp is the full orthant [0,infinity)^n for every elapsed-time vector, so it intersects every elementary SC; the proof in App. C then shows the minimum equals omega(l). This is a genuine consequence of the definitions, not a restatement of the conclusion. The granularity statements in Theorem 2 are monotonicity arguments based on adding restrictions, again following from the definitions. The experimental results are measured: relative errors are computed against 12-hour CMC ground-truth estimates, and no parameter is fitted to force the reported comparison. The depth-limited SC graph used for m_s (App. E.4) is a heuristic justified partly by the authors' prior work [12]; if the depth bound were violated, the tsen_timed distances could be inaccurate, but this is an acknowledged completeness/risk issue, not a circular step in which an output equals an input by construction. The paper itself flags the partial empirical view (Sec. 6.3) and defers theoretical performance guarantees to future work (Sec. 7). Self-citations to [12] supply the base method and background calculations, but the new claims are not justified solely by those citations.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 1 invented entities

The central theorems do not depend on the listed free parameters; these are experiment configuration choices. The axioms are standard background assumptions plus the unproven unbiasedness of the resampling/pruning scheme. The global age timer is the only invented entity, and it is fully determined by simulation time.

free parameters (4)
  • threshold_selection_n = 1000
    Number of initial states sampled to find low-importance states (Sec 3.2).
  • threshold_selection_k = 10
    Number of lowest-importance states used to define the initial importance range (Sec 3.2).
  • rejection_sampling_attempts = 20
    Maximum attempts when resampling truncated distributions; falls back to the old sample (App. B).
  • max_expansion_depth_ms = 12
    Depth limit for SC graph construction in model m_s because full timed metric construction did not terminate (App. E.4).
axioms (4)
  • domain assumption IOSA model semantics and DBM zone operations are correct
    Backwards reachability and SC calculations from [12] are assumed sound.
  • standard math Residual timer distribution given elapsed time e is (X | X >= e) - e
    Used to justify resampling; standard probability theory.
  • domain assumption ISPLIT with resampling and pruning yields unbiased estimators
    Argued in Sec 3/App. B; not formally proven in the paper.
  • domain assumption Ground truth probabilities approximated by 12h CMC are reliable
    Used to compute relative errors; for m_ℓ the shown CMC run had zero hits.
invented entities (1)
  • global age timer t_age independent evidence
    purpose: Artificial state variable recording remaining time budget; enables pruning of unreachable branches and age-aware distance metrics
    t_age is a deterministic function of simulation time, so its value is fixed and checkable; no external physical evidence needed.

pith-pipeline@v1.3.0-alltime-deepseek · 33091 in / 15876 out tokens · 129007 ms · 2026-08-01T16:33:41.666199+00:00 · methodology

0 comments
read the original abstract

Importance splitting (ISPLIT) evaluates the probabilities of rare events in non-Markovian models. It requires a heuristic importance function (IFUN) that estimates the distance to the target. While including timer evaluations in the IFUN can substantially improve the effectiveness of ISPLIT, the existing time-sensitive IFUNs evaluate simulation states with respect to single sampled timer values. Thus, reaching highly important states requires simultaneously sampling specific combinations of timer values, yielding several unproductive simulation runs. In this paper, we revisit time-sensitive ISPLIT with the goal of steering simulation runs towards important states. First, we study how timer values can be resampled conditioned on the elapsed time. The importance can be evaluated by considering the set of feasible timer values, decoupling importance estimation from timer samples. Second, we exploit the global age of a simulation to identify and prune the executions that can no longer reach the target within the remaining time budget. Together, these ideas lead to a taxonomy of distance metrics clarifying the role of timer bounds, resampling, and the global age. In particular, for models with unbounded timers, we show that time-sensitive IFUNs collapse to ordinary IFUNs under resampling. Experiments demonstrate that the proposed formulations substantially improve the accuracy of ISPLIT estimators.

Figures

Figures reproduced from arXiv: 2607.17939 by Carlos E. Budde, Gabriel Dengler, Laura Carnevali.

Figure 1
Figure 1. Figure 1: Toy example Example 1 [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Selected SCs from backwards reachability search in the toy example [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Taxonomy of the derived distance metrics [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Changes of domain D3 from [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Experimentation model mℓ (ms) the case study from [12], with 4 PAND gates and uniform fail/re￾pair distributions; (mℓ) the larger sys￾tem from [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Tandem queue Queueing networks. A tandem queue consists of n queues connected in series, with arrivals (departures) from outside via the first (resp. last) queue only. We experiment on the minimal n = 2 case from [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Relative error for ms, mℓ, and mQ (lower is better) [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: DFT experimentation models from Sec. 6 of observing a full system failure, using T = 1248 for ms and T = 4500 for mℓ. The corresponding ground truth failure probabilities—approximated with 12-hours-long CMC runs—are φms ≈ 5.2e-7 and φmℓ ≈ 2.2e-8. All timers that govern failures and repairs in the BEs of ms have (bounded) uni￾form distributions—the concrete bounds can be found in Code 1 and [12]. In con￾tra… view at source ↗

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

36 extracted references · 17 canonical work pages

  1. [1]

    Performance Evaluation70(6), 400–422 (2013)

    Amparore, E.G., Donatelli, S.: A component-based solution for reducible Markov regenerative processes. Performance Evaluation70(6), 400–422 (2013)

    2013

  2. [2]

    Barton, R.R., Schruben, L.W.: Uniform and bootstrap resampling of empirical distributions. In: WSC. pp. 503–508. ACM (1993). https://doi.org/10.1145/256563.256699

    arXiv 1993

  3. [3]

    Blom, H.A., Bakker, G.B., Krystul, J.: Rare event estimation for a large-scale stochastic hybrid system with air traffic application, chap. 9, pp. 193–214. In: Rubino and Tuffin [26] (2009). https://doi.org/10.1002/9780470745403.ch9

    work page doi:10.1002/9780470745403.ch9 2009

  4. [4]

    Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Automated composi- tional importance splitting. Sci. Comput. Program.174, 90–108 (2019). https://doi.org/10.1016/J.SCICO.2019.01.006

    work page doi:10.1016/j.scico.2019.01.006 2019

  5. [5]

    STTT24(5), 821–841 (2022)

    Budde, C.E., D’Argenio, P.R., Monti, R.E., Stoelinga, M.: Analysis of non- Markovian repairable fault trees through rare event simulation. STTT24(5), 821–841 (2022). https://doi.org/10.1007/S10009-022-00675-X

    work page doi:10.1007/s10009-022-00675-x 2022

  6. [6]

    Queueing Syst

    Buijsrogge, A., de Boer, P.T., Scheinhardt, W.R.W.: Importance sampling for non-Markovian tandem queues using subsolutions. Queueing Syst. Theory Appl. 93(1-2), 31–65 (2019). https://doi.org/10.1007/S11134-019-09623-0

    work page doi:10.1007/s11134-019-09623-0 2019

  7. [7]

    IEEE Transactions on Software Engineering48(12), 4762–4788 (2021)

    Carnevali, L., German, R., Santoni, F., Vicario, E.: Compositional analysis of hierarchical UML Statecharts. IEEE Transactions on Software Engineering48(12), 4762–4788 (2021). https://doi.org/10.1109/TSE.2021.3125720

    arXiv 2021

  8. [8]

    Statistics and computing22(3), 795–808 (2012) 18 G

    Cérou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Statistics and computing22(3), 795–808 (2012) 18 G. Dengler et al

    2012

  9. [9]

    IEEE Transactions on software engineering20(7), 506–515 (1994)

    Ciardo, G., German, R., Lindemann, C.: A characterization of the stochastic process underlying a stochastic Petri net. IEEE Transactions on software engineering20(7), 506–515 (1994). https://doi.org/10.1109/32.297939

    work page doi:10.1109/32.297939 1994

  10. [10]

    In: ICTAC

    D’Argenio, P.R., Monti, R.E.: Input/output stochastic automata with urgency: Confluence and weak determinism. In: ICTAC. LNCS, vol. 11187, pp. 132–152. Springer (2018). https://doi.org/10.1007/978-3-030-02508-3_8

    doi:10.1007/978-3-030-02508-3_8 2018

  11. [11]

    In: 17th Nordic Workshop on Programming Theory

    David, A.: Merging DBMs efficiently. In: 17th Nordic Workshop on Programming Theory. pp. 54–56. DIKU University of Copenhagen (2005)

    2005

  12. [12]

    In: QEST+FORMATS

    Dengler, G., Budde, C.E., Carnevali, L., Hartmanns, A.: Time-sensitive importance splitting. In: QEST+FORMATS. LNCS, vol. 16143, pp. 21–41. Springer (2025). https://doi.org/10.1007/978-3-032-05792-1_2

    work page doi:10.1007/978-3-032-05792-1_2 2025

  13. [13]

    In: QEST+FORMATS

    Dengler, G., Carnevali, L., Budde, C.E., Vicario, E.: Transient evaluation of non- Markovian models by stochastic state classes and simulation. In: QEST+FORMATS. LNCS, vol. 14996 (2024). https://doi.org/10.1007/978-3-031-68416-6_13

    work page doi:10.1007/978-3-031-68416-6_13 2024

  14. [14]

    Nuclear Power Engineering42(5), 173–177 (2021)

    Dongliang, Z., Kaiwen, Z., Chaofan, Z.: Reliability modeling and analysis of reactor protection system based on FPGA. Nuclear Power Engineering42(5), 173–177 (2021). https://doi.org/10.13832/j.jnpe.2021.05.0173

    work page doi:10.13832/j.jnpe.2021.05.0173 2021

  15. [15]

    Garvels, M.J.J.: The splitting method in rare event simulation. Ph.D. thesis, University of Twente (2000),http://eprints.eemcs.utwente.nl/14291/

    2000

  16. [16]

    In: PNPM

    German, R., Logothetis, D., Trivedi, K.S.: Transient analysis of Markov regenerative stochastic Petri nets: A comparison of approaches. In: PNPM. pp. 103–112. IEEE (1995),https://dlnext.acm.org/doi/10.5555/826033.826790

    arXiv 1995

  17. [17]

    Operations Research47(4), 585–600 (1999), http://www.jstor.org/stable/223163

    Glasserman, P., Heidelberger, P., Shahabuddin, P., Zajic, T.: Multilevel splitting for estimating rare event probabilities. Operations Research47(4), 585–600 (1999), http://www.jstor.org/stable/223163

    1999

  18. [18]

    In: TACAS

    Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS. LNCS, vol. 8413, pp. 593–598. Springer (2014). https://doi.org/10.1007/978-3-642-54862-8_51

    doi:10.1007/978-3-642-54862-8_51 2014

  19. [19]

    Horváth, A., Paolieri, M., Ridi, L., Vicario, E.: Transient analysis of non-Markovian models using stochastic state classes. Perform. Evaluation69(7-8), 315–335 (2012). https://doi.org/10.1016/J.PEVA.2011.11.002

    work page doi:10.1016/j.peva.2011.11.002 2012

  20. [20]

    ACM Trans

    L’Ecuyer, P., Blanchet, J.H., Tuffin, B., Glynn, P.W.: Asymptotic robustness of estimators in rare-event simulation. ACM Trans. Model. Comput. Simul.20(1) (2010). https://doi.org/10.1145/1667072.1667078

    arXiv 2010

  21. [21]

    L’Ecuyer, P., Le Gland, F., Lezaud, P., Tuffin, B.: Splitting Tech- niques, chap. 3, pp. 39–61. In: Rubino and Tuffin [26] (2009). https://doi.org/10.1002/9780470745403.ch3

    work page doi:10.1002/9780470745403.ch3 2009

  22. [22]

    In: Proceed- ings of Symposia in Applied Mathematics

    Lehmer, D.H.: Teaching combinatorial tricks to a computer. In: Proceed- ings of Symposia in Applied Mathematics. pp. 179–193. AMS (1960). https://doi.org/10.1090/psapm/010/0113289

    work page doi:10.1090/psapm/010/0113289 1960

  23. [23]

    In: LPAR

    Monti, R.E., Budde, C.E., D’Argenio, P.R.: A compositional semantics for repairable fault trees with general distributions. In: LPAR. EPiC Series in Computing, vol. 73, pp. 354–372. EasyChair (2020). https://doi.org/10.29007/P16V

    work page doi:10.29007/p16v 2020

  24. [24]

    In: QEST

    Reijsbergen, D., de Boer, P.T., Scheinhardt, W.R.W., Haverkort, B.R.: Automated rare event simulation for stochastic Petri nets. In: QEST. LNCS, vol. 8054, pp. 372–388. Springer (2013). https://doi.org/10.1007/978-3-642-40196-1_31

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

  25. [25]

    Robert L., J.: Analysis of phase-type stochastic Petri nets with discrete and contin- uous timing. Tech. rep. (2000),https://ntrs.nasa.gov/citations/20000120040

    arXiv 2000

  26. [26]

    (eds.): Rare Event Simulation Using Monte Carlo Methods

    Rubino, G., Tuffin, B. (eds.): Rare Event Simulation Using Monte Carlo Methods. Wiley (2009). https://doi.org/10.1002/9780470745403 A Taxonomy of Distance Metrics for Time-Sensitive ISPLIT 19

    work page doi:10.1002/9780470745403 2009

  27. [27]

    Computer science review15, 29–62 (2015)

    Ruijters, E., Stoelinga, M.: Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Computer science review15, 29–62 (2015)

    2015

  28. [28]

    In: FTCS

    Sullivan, K.J., Dugan, J.B., Coppit, D.: The Galileo fault tree analysis tool. In: FTCS. pp. 232–235 (1999),https://dl.acm.org/doi/10.5555/795672.796973

    arXiv 1999

  29. [29]

    IEEE TSE27(8), 728–748 (2001)

    Vicario, E.: Static analysis and dynamic steering of time-dependent systems. IEEE TSE27(8), 728–748 (2001). https://doi.org/10.1109/32.940727

    work page doi:10.1109/32.940727 2001

  30. [30]

    IEEE Transactions on Software Engineering35(5), 703–719 (2009)

    Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantita- tive evaluation of dense-time reactive systems. IEEE Transactions on Software Engineering35(5), 703–719 (2009). https://doi.org/10.1109/TSE.2009.36

    work page doi:10.1109/tse.2009.36 2009

  31. [31]

    Queueing, Performance and Control in ATM (ITC-13) pp

    Villén-Altamirano, M., Villén-Altamirano, J.: RESTART: a method for accelerating rare event simulations. Queueing, Performance and Control in ATM (ITC-13) pp. 71–76 (1991)

    1991

  32. [32]

    Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV. LNCS, vol. 2404, pp. 223–235. Springer (2002). https://doi.org/10.1007/3-540-45657-0_17

    work page doi:10.1007/3-540-45657-0_17 2002

  33. [33]

    In: HSCC

    Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: HSCC. pp. 217–226. ACM (2012). https://doi.org/10.1145/2185632.2185665 A Backwards Reachability Calculations with State Classes We recall the calculations of predecessor SCs in an IOSA from [12]. Target SCs.For each target locationl′, we build the largest poss...

    arXiv 2012

  34. [34]

    Inverse of newly activating:Letτ′ :=⟨t′ 2,...,t ′ n+m⟩ andt′ n+1,...,t ′ n+m∈T ′ be them newly activated timers inl′. We limit each such timer by its lower bound (as no time elapses from new activation to entrance inΣ′), obtaining τa :=⟨t a 2,...,t a n,ta n+1,...,t a n+m⟩=τ ′|t ′ n+1,...,t′ n+m∈T ′, 20 G. Dengler et al. with support Da =D′∩{ai≤τ(t′ i)∀i∈{...

  35. [35]

    Inverse of time advancement:We increase the timers by the timer expiring first inΣ, sayt b 1, obtaining τc :=⟨t c 1,...,t c n⟩=⟨t b 1,tb 2 +tb 1,...,t b n +tb 1⟩ with support: Dc ={⟨τ(t b 1),τ(t b 2),...,τ(t b n)⟩ s.t.τ(t b 1)∈[0,∞) s.t.⟨τ(t b 2)−τ(t b 1),...,τ(t b n)−τ(t b 1)⟩∈D b}

  36. [36]

    PAND1"; 2

    Applying upper bounds of timers:After normalizingDc, we limit each active timer by its upper bound (to guarantee the timer does not exceed the bound due to the time retardation), obtaining τ:=⟨t 1,...,t n⟩=τ c|t c i≤b i∀i∈{1,...,n} with the final domain (which is finally normalized, similarly to the previous passages): D=D c∩{τ(t c i)≤b i∀i∈{1,...,n}} Not...