Pith. sign in

REVIEW 3 major objections 5 minor 56 references

Time-Sensitive Importance Splitting

T0 review · 3 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 a timer-aware distance metric, computed by backwards reachability over state classes, lets importance splitting steer simulation toward rare events whose probability depends on ordered timer expirations in…

desk verdict Genuinely new IF heuristic via backwards reachability over timer zones, but the backward calculus is unproved and the experiments are a single-case study; worth refereeing, not yet fully convincing. read the letter →

arxiv 2506.19568 v1 pith:F7YGUGAB submitted 2025-06-24 cs.LO cs.NAmath.NA

Gabriel Dengler , Carlos E. Budde , Laura Carnevali , Arnd Hartmanns This is my paper · ORCID
classification cs.LOcs.NAmath.NA
keywords time-sensitiveimportancesplittingrareeventsimulationnon-Markovianmodelsstochasticstateclassesbackwardsreachabilitydifferenceboundmatricesrepairabledynamicfaulttrees
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

The paper claims that importance splitting can be made time-sensitive: instead of measuring a state's importance only by how many transitions separate it from the target, measure it by a distance that also reads the remaining values of active timers. It shows how to compute that distance by running state-class reachability backwards from target locations, using lower and upper bounds of timer supports to build the weakest timer domain that can still reach the target. For a repairable dynamic fault tree with PAND gates, where the top event requires four components to fail in order, the resulting estimator finds a probability near the independently measured ground truth of about $5.24\times 10^{-7}$, with confidence intervals narrower than those of crude Monte Carlo or time-agnostic importance splitting. If correct, this removes a known blind spot of rare event simulation for non-Markovian models: events whose rareness comes from unusual timer constellations rather than from the discrete state alone.

What carries the argument

The engine is the backwards state class graph. A state class $\langle l,D\rangle$ is a location together with a set of timer valuations, represented as a difference bound matrix; normally it is computed forwards from the initial state. The paper's construction starts from the target states with the largest timer domain compatible with them, then repeatedly computes weakest preconditions: given an incoming transition and a target state class, produce the largest predecessor timer domain such that every state in it reaches the target through that transition. Three inverse operations, undoing newly activated timers, undoing time advancement, and applying upper bounds, generate these predecessors, and the distance metric $d(s)=\min_{\Sigma\ni s}\omega(\Sigma)$ is read off the resulting graph. Keeping domains as difference bound matrices makes the encoding and all operations polynomial in the number of active timers.

What would settle it

For a small model, enumerate all timer valuations on a fine grid, decide reachability of the target within a bounded transition count by direct simulation or symbolic analysis, and compare the true reachable set with the state-class domain the backwards method outputs; any valuation inside the domain that cannot reach the target, or outside the domain that can, disproves the exactness claim. A direct check in the paper's own toy example is whether the boundary valuation $\tau(t_{uf})=10.2$, $\tau(t_{af})=20$, whose difference is $-9.8$, really can trigger the target path under the model's sampling semantics.

Watch

Extended reading notes

Core claim

The paper's central discovery is that the full timer valuation, not just the discrete location, can be folded into the importance function of importance splitting. It defines a distance $d(s)$ from a state to the target as the minimum, over all state classes containing $s$, of the state class distance $\omega(\Sigma)$, where the state class graph is grown backwards from the target locations. The backwards step inverts the three operations of forward state-class analysis: it removes newly activated timers by imposing their lower bounds, undoes time advancement by adding back the first-expiring timer, and applies upper bounds to all active timers. Domains are represented as difference bound matrices, so each manipulation costs polynomial time in the number of active timers. The experiments show that the timer-aware importance function with exploration depth 10 estimates the studied probability with a confidence interval that contains the ground truth and is noticeably narrower than the intervals produced by crude Monte Carlo and by time-agnostic importance splitting; with only 50,000 runs, crude Monte Carlo and time-agnostic splitting observe no failure at all, while the timer-aware runs produce useful intervals.

Load-bearing premise

The load-bearing premise is that the backwards computation recovers the exact set of timer values that can reach the target, neither too large nor too small, because the paper does not prove this and the entire importance metric inherits any error in it.

Editorial extensions

If this is right

  • Rare event simulation becomes applicable to non-Markovian systems whose rare event is caused by the order of timer expirations, not by an unlikely sequence of discrete choices.
  • The time-sensitive importance function slots into existing importance splitting algorithms such as fixed effort and RESTART, so the scheme inherits their threshold-selection machinery with at most minor changes.
  • For the PAND-gate dynamic fault tree studied, 50,000 simulation runs suffice to produce a confidence interval containing the true probability, whereas crude Monte Carlo and time-agnostic splitting observe zero failures in the same budget.
  • Exploration depth of the backwards graph is a tunable resource: shallow depths keep precomputation cheap, while depths far beyond the event horizon waste splitting effort, as seen in the depth-22 slowdown in the fixed-runtime experiments.
  • The same backwards state-class computation can be extended with a global elapsed-time timer, so that the importance function can also account for whether the target is still reachable before a time bound expires.

Reading between the lines

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

  • A formal correctness proof of the predecessor rules could likely be recovered by showing that each inverse of a forward state-class operation is exact on difference bound matrix domains; the paper leaves this at the level of assertion, and until then the heuristic's safety rests on the non-negativity condition on timer differences.
  • A natural stress test beyond the paper is to replace uniform timers with truncated heavy-tailed distributions: since the method truncates infinite supports at quantile bounds, the bias introduced by that truncation is measurable and could be compared against the variance gain of the timer-aware importance function.
  • Because the distance metric is used only to steer simulation, the backwards graph could deliberately be under-approximated or over-approximated, trading precomputation cost against variance; the depth-22 degradation in the experiments hints that the optimal depth lies near the event's transition horizon, a relationship the paper does not formalize.
  • The technique transfers naturally from decreasing timers to increasing clocks in the style of timed automata, where zone-based backwards reachability is already standard; the paper mentions this as future work, but the transfer appears mechanical rather than conceptual.
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

3 major / 5 minor

Summary. The paper proposes time-sensitive importance splitting (ISPLIT) for rare-event simulation of non-Markovian models. Instead of the standard time-agnostic importance function based only on locations, the authors compute a timed distance metric by a backwards reachability analysis over stochastic state classes (SCs) represented as difference bound matrices (DBMs). The distance of a concrete state is the minimum, over all SCs containing that state, of the number of transitions needed to reach a target SC; the importance function is then the standard linear transformation of that distance. The method is implemented as a prototype in the Modest Toolset and evaluated on a repairable dynamic fault tree with PAND gates, where it estimates a probability of about 5.24e-7 with confidence intervals narrower than those of crude Monte Carlo and of time-agnostic importance splitting. The paper argues this is the first ISPLIT formulation whose importance metric depends on concrete timer valuations.

Significance. If the predecessor-SC construction of Section 3 is exact, the contribution is novel and potentially useful: it gives a principled way to make the importance function depend on timer values, a case where location-only heuristics provably fail. The paper is honest about its limitations: the evaluation is on a single synthetic DFT with uniform distributions, the state-space explosion is acknowledged and mitigated only by truncating the backward expansion, and the confidence intervals used are normal-approximation intervals. The artifact and reproduction package are a clear strength, as are the ablation over expansion depth and the comparison against both crude Monte Carlo and a time-agnostic ISPLIT baseline. However, the central algorithmic step, the exact computation of predecessor state classes, is asserted rather than proved, and the treatment of urgent (T=∅) transitions is missing. These are load-bearing points, so the significance is conditional on the correctness of the backward analysis.

major comments (3)
  1. [§3, Steps 1–3]
  2. [§3, Step 2; §4.2, Code 1]
  3. [§4.3, Table 1; §3, Optimizations]
minor comments (5)
  1. [§3, Step 2]
  2. [§4.1]
  3. [§4.2]
  4. [§4.3, Table 1b]
  5. [§5]

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity found.

full rationale

The paper's derivation chain is self-contained. The time-sensitive importance function is computed by a backwards reachability search over state classes, using only the model's structure (locations, timers, bounds, transitions) and a graph distance to target state classes. No parameter of this importance function is fitted to the target probability: the rare-event estimate is obtained by running ISPLIT with the fixed importance function, and the ground truth is independently estimated by crude Monte Carlo. The time-agnostic baseline from earlier work by some of the same authors serves as a comparison, not as an input that forces the result. The expansion-depth choice is a tuning parameter, not a fitted quantity. The paper's main unproven premise is the exactness of the predecessor state-class computation in Sec. 3, but that is a correctness risk, not a circularity: the backward operations are not defined in terms of the simulation output, and the distance metric is not equivalent to the target probability by construction. Self-citations (e.g., to prior work on time-agnostic importance splitting, SSC transient analysis, and DFT semantics) are motivational or comparative and are not load-bearing in the derivation of the new time-sensitive importance function. Thus no circular step can be exhibited from the paper's own equations or citations.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

No new physical or ontological entities are introduced. The time-sensitive importance function is a new derived object built from existing model semantics, not a postulated entity. The free-parameter count is kept minimal; the main tunable is the backwards expansion depth, which the authors select by ablation rather than fit to the target probability.

free parameters (1)
  • backwards expansion depth d = 10 (best in the ablation over 6, 10, 14, 18, 22)
    Controls how much of the state class graph is enumerated for the importance function. The authors select d=10 as the best result after inspecting Table 1a and 1b, a post hoc choice, and the paper notes depths above 10 create irrelevant layers (Sec. 4.2 and Sec. 4.3).
assumptions (5)
  • standard math Forward SC successor computation (conditioning, time advancement, timer activation) correctly captures the semantics of IOSA timer evolution.
    Relying on established state class theory [53] as summarized in Sec. 2.2.
  • domain assumption Each location has a unique set of enabled timers (weak determinism), so the SC expansion is well-defined.
    Assumed from IOSA with urgency semantics [21], Sec. 2.1. A footnote notes the general case needs an extra initial forwards analysis.
  • domain assumption The repairable DFT models considered can be represented without explicit timer deactivation, so the backward SC derivation can omit the deactivation step.
    Sec. 2.2: 'the repairable DFT scenarios considered in this paper can be modeled in IOSA without deactivation of timers [40]'.
  • ad hoc to paper The three inverse operations in the predecessor SC computation produce the largest timer domain from which a transition leads to the target SC.
    Sec. 3, 'Predecessor SC': asserted as the definition of the computation, without a formal proof of exactness. This is the load-bearing unproven step.
  • standard math Initial timer domains are hyper-rectangles with rational bounds, guaranteeing finitely many SCs.
    Sec. 2.2, footnote 2, citing [33, Lemma 3.2].

how reviews work

0 comments
Cite this review

Pith. "Pith review of Time-Sensitive Importance Splitting." pith.science (2026). https://pith.science/paper/F7YGUGAB

@misc{pith2026250619568,
  author       = {Pith},
  title        = {Pith review of: Time-Sensitive Importance Splitting},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/F7YGUGAB}},
  note         = {Machine review of arXiv:2506.19568}
}
read the original abstract

State-of-the-art methods for rare event simulation of non-Markovian models face practical or theoretical limits if observing the event of interest requires prior knowledge or information on the timed behavior of the system. In this paper, we attack both limits by extending importance splitting with a time-sensitive importance function. To this end, we perform backwards reachability search from the target states, considering information about the lower and upper bounds of the active timers in order to steer the generation of paths towards the rare event. We have developed a prototype implementation of the approach for input/output stochastic automata within the Modest Toolset. Preliminary experiments show the potential of the approach in estimating rare event probabilities for an example from reliability engineering.

Figures

Figures reproduced from arXiv: 2506.19568 by the authors.

Figure 1
Figure 1. Toy example We start by studying a small repairable DFT ex￾ample in [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. DFT with sequen￾tial failures and repairs 1 toplevel "PAND1"; 2 "PAND1" pand "BE1" "PAND2"; 3 "PAND2" pand "BE2" "PAND3"; 4 "PAND3" pand "BE3" "BE4"; 5 "BE1" fail~ uniform(1198,1218) repair~ uniform(10,15); 6 "BE2" fail~ uniform(530,595) repair~ uniform(10,45); 7 "BE3" fail~ uniform(385,465) repair~ uniform(10,45); 8 "BE4" fail~ uniform(1105,1205) repair~ uniform(10,15); 9 "RBOX" rbox prio "BE1" "BE2" "BE3" "BE4"; C… view at source ↗
Figure 3
Figure 3. Behavior of DFT in Code 2 [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Created STA for the UPS BE in Fig. 1/Code 1 [PITH_FULL_IMAGE:figures/full_fig_p011_4.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

56 extracted references · 35 canonical work pages

  1. [1]

    ACM Trans

    Ajmone Marsan, M., Conte, G., Balbo, G.: A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Trans. Comput. Syst. 2(2), 93–122 (1984). https://doi.org/10.1145/190.191

    doi:10.1145/190.191 1984

  2. [2]

    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)

    work page 2013

  3. [3]

    MIT Press (2008)

    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

    2008

  4. [4]

    IEEE transactions on software engineering17(3), 259 (1991)

    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE transactions on software engineering17(3), 259 (1991)

    work page 1991

  5. [5]

    Bertrand, N., Bouyer, P., Brihaye, T., Menet, Q., Baier, C., Größer, M., Jurdz- inski, M.: Stochastic Timed Automata. Log. Methods Comput. Sci. 10(4) (2014). https://doi.org/10.2168/LMCS-10(4:6)2014, https://doi.org/10.2168/ LMCS-10(4:6)2014

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

  6. [6]

    In: Bertrand, N., Bortolussi, L

    Biagi, M., Carnevali, L., Paolieri, M., Papini, T., Vicario, E.: Exploiting Non- deterministic Analysis in the Integration of Transient Solution Techniques for Markov Regenerative Processes. In: Bertrand, N., Bortolussi, L. (eds.) Quantitative EvaluationofSystems-14thInternationalConference,QEST2017,Berlin,Germany, September 5-7, 2017, Proceedings. Lectur...

    work page doi:10.1007/978-3-319-66335-7_2 2017

  7. [7]

    Transportation Research Part C: Emerging Technolo- gies 82, 314–336 (2017)

    Biagi, M., Carnevali, L., Paolieri, M., Vicario, E.: Performability evaluation of the ERTMS/ETCS – Level 3. Transportation Research Part C: Emerging Technolo- gies 82, 314–336 (2017). https://doi.org/https://doi.org/10.1016/j.trc.2017.07.002, https://www.sciencedirect.com/science/article/pii/S0968090X17301833

    work page doi:10.1016/j.trc.2017.07.002 2017

  8. [8]

    Bouyer, P.: An introduction to timed automata.http://www.lsv.fr/~bouyer/ files/mpri1112.pdf (2011), accessed: 2025-04-18

    work page 2011

Show all 56 references
  1. [9]

    Budde, C.E.: Automation of Importance Splitting Techniques for Rare Event Simulation. Ph.D. thesis (05 2017)

    2017

  2. [10]

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

    2019 doi

  3. [11]

    Budde, C.E., D’Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf. 22(6), 759–780 (2020). https://doi.org/10.1007/S10009-020-00563-2

    2020 doi

  4. [12]

    In: EPEW

    Budde, C.E., D’Argenio, P.R., Hermanns, H.: Rare event simulation with fully automated importance splitting. In: EPEW. Lecture Notes in Computer Science, vol. 9272, pp. 275–290. Springer (2015). https://doi.org/10.1007/978-3-319-23267- 6_18

    2015 doi

  5. [13]

    Budde, C.E., D’Argenio, P.R., Monti, R.E., Stoelinga, M.: Analysis of non- Markovian repairable fault trees through rare event simulation. Int. J. Softw. Tools Technol. Transf.24(5), 821–841 (2022). https://doi.org/10.1007/S10009-022- 00675-X 18 G. Dengler et al

    2022 doi

  6. [14]

    In: TACAS 2025

    Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienhöft, P.: Sound Statistical Model Checking for Probabilities and Expected Rewards. In: TACAS 2025. LNCS, Springer (2025), to appear, preprint available at DOI 10.48550/arXiv.2411.00559

    2025 doi arXiv

  7. [15]

    In: QEST

    Budde, C.E., Ruijters, E., Stoelinga, M.: The dynamic fault tree rare event simulator. In: QEST. Lecture Notes in Computer Science, vol. 12289, pp. 233–238. Springer (2020). https://doi.org/10.1007/978-3-030-59854-9_17

    2020 doi

  8. [16]

    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)

    2021

  9. [17]

    Sto- chastic Analysis and Applications25(2), 417–443 (2007)

    Cérou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Sto- chastic Analysis and Applications25(2), 417–443 (2007)

    2007

  10. [18]

    Performance evaluation20(1-3), 337–357 (1994)

    Choi, H., Kulkarni, V.G., Trivedi, K.S.: Markov regenerative stochastic Petri nets. Performance evaluation20(1-3), 337–357 (1994)

    1994

  11. [19]

    D’Argenio, P.R., Katoen, J.: A theory of stochastic systems part I: Stochastic auto- mata. Inf. Comput.203(1), 1–38 (2005). https://doi.org/10.1016/J.IC.2005.07.001, https://doi.org/10.1016/j.ic.2005.07.001

    2005 doi

  12. [20]

    In: FORMATS

    D’Argenio, P.R., Lee, M.D., Monti, R.E.: Input/Output Stochastic Automata - compositionality and determinism. In: FORMATS. LNCS, vol. 9884, pp. 53–68. Springer (2016). https://doi.org/10.1007/978-3-319-44878-7_4

    2016 doi

  13. [21]

    In: ICTAC 2018

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

    2018 doi

  14. [22]

    In: Gopalakrishnan, G., Qadeer, S

    David, A., Larsen, K.G., Legay, A., Mikucionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceed...

    2011 doi

  15. [23]

    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. Lecture Notes in Computer Science, vol. 14996, pp. 213–232. Springer (2024). https://doi.org/10.1007/978-3-031-68416-6_13

    2024 doi

  16. [24]

    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

    2021 doi

  17. [25]

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

    2000

  18. [26]

    In: Proceedings 8th International Workshop on Petri Nets and Performance Models (Cat

    German, R., Telek, M.: Formal relation of Markov renewal theory and supplementary variables in the analysis of stochastic Petri nets. In: Proceedings 8th International Workshop on Petri Nets and Performance Models (Cat. No.PR00331). pp. 64–73 (1999). https://doi.org/10.1109/PN...

    1999

  19. [27]

    Performance Evalu- ation 44(1-4), 51–72 (2001)

    German, R.: Iterative analysis of Markov regenerative models. Performance Evalu- ation 44(1-4), 51–72 (2001)

    2001

  20. [28]

    German, R., Lindemann, C.: Analysis of Stochastic Petri Nets by the Method of Supplementary Variables. Perform. Evaluation 20(1-3), 317–335 (1994). https://doi.org/10.1016/0166-5316(94)90020-5,https://doi.org/10.1016/ 0166-5316(94)90020-5 Time-Sensitive Importance Splitting 19

    1994 doi

  21. [29]

    European Journal of Opera- tional Research 1(6), 396–402 (1977)

    Grassmann, W.: Transient solutions in Markovian queues: An algorithm for finding them and determining their waiting-time distributions. European Journal of Opera- tional Research 1(6), 396–402 (1977). https://doi.org/10.1016/0377-2217(77)90049- 2

    1977 doi

  22. [31]

    CoRR abs/2208.11928 (2022)

    Hartmanns, A., Kohlen, B.: Backwards reachability for probabilistic timed automata: A replication report. CoRR abs/2208.11928 (2022). ht- tps://doi.org/10.48550/ARXIV.2208.11928, https://doi.org/10.48550/arXiv. 2208.11928

    2022 doi arXiv

  23. [32]

    In: Proceedings of the Seventh Annual Symposium on Logic in Com- puter Science (LICS ’92), Santa Cruz, California, USA, June 22-25, 1992

    Henzinger,T.A.,Nicollin,X.,Sifakis,J.,Yovine,S.:Symbolicmodelcheckingforreal- time systems. In: Proceedings of the Seventh Annual Symposium on Logic in Com- puter Science (LICS ’92), Santa Cruz, California, USA, June 22-25, 1992. pp. 394–

    1992

  24. [33]

    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, https://doi.org/10.1016/j.peva. 2011.11.002

    2012 doi

  25. [34]

    ACM Trans

    Hüls, J., Pilch, C., Schinke, P., Niehaus, H., Delicaris, J., Remke, A.: State-space Construction of Hybrid Petri Nets with Multiple Stochastic Firings. ACM Trans. Model. Comput. Simul.31(3), 13:1–13:37 (2021). https://doi.org/10.1145/3449353, https://doi.org/10.1145/3449353

    2021 doi

  26. [35]

    In: Fränzle, M., Kapur, D., Zhan, N

    Jégourel, C., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Importance sampling for stochastic timed automata. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposiu...

    2016 doi

  27. [36]

    Information and Computation205(7), 1027– 1077 (2007)

    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, https:// www.sciencedirect.com/science/article/pii/S08...

    2007 doi

  28. [37]

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

    2009 doi

  29. [38]

    L’Ecuyer, P., Mandjes, M., Tuffin, B.: Importance Sampling in Rare Event Simulation, chap. 2, pp. 17–38. In: Rubino and Tuffin [50] (2009). ht- tps://doi.org/10.1002/9780470745403.ch2

    2009 doi

  30. [39]

    In: ESREL

    Lee, J., Mitici, M.: Predictive aircraft maintenance: Modeling and analysis using stochastic Petri nets. In: ESREL. pp. 146–153 (2021). https://doi.org/10.3850/978- 981-18-2016-8_050-cd

    2021 doi

  31. [40]

    In: LPAR 2020

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

    2020 doi

  32. [41]

    IEEE Transactions on Reliability50(3), 246–264 (2001)

    Nicola, V., Shahabuddin, P., Nakayama, M.: Techniques for fast simulation of models of highly dependable systems. IEEE Transactions on Reliability50(3), 246–264 (2001). https://doi.org/10.1109/24.974122 20 G. Dengler et al

    2001 doi

  33. [42]

    Niehage, M., Remke, A.: Symbolic state-space exploration meets stat- istical model checking. Perform. Evaluation 167, 102449 (2025). ht- tps://doi.org/10.1016/J.PEVA.2024.102449, https://doi.org/10.1016/j.peva. 2024.102449

    2025

  34. [43]

    In: NASA Formal Methods - 17th International Symposium, NFM 2025, Williamsburg, Virginia, USA, June 11-13, 2025, Proceedings

    Niehage, M., da Silva, C., Remke, A., Hartmanns, A.: Rare event simulation for stochastic hybrid systems using symbolic importance functions. In: NASA Formal Methods - 17th International Symposium, NFM 2025, Williamsburg, Virginia, USA, June 11-13, 2025, Proceedings. Lecture N...

    2025

  35. [44]

    John Wiley & Sons, Ltd (2011)

    O’Connor, P.D.T., Kleyner, A.: Practical Reliability Engineering. John Wiley & Sons, Ltd (2011). https://doi.org/10.1002/9781119961260

    2011 doi

  36. [45]

    IEEE Trans

    Paolieri, M., Biagi, M., Carnevali, L., Vicario, E.: The ORIS Tool: Quantitative Evaluation of Non-Markovian Systems. IEEE Trans. Software Eng.47(6), 1211–1225 (2021). https://doi.org/10.1109/TSE.2019.2917202

    2021

  37. [46]

    Com- puters & Operations Research15(1), 19–36 (1988)

    Reibman, A., Trivedi, K.: Numerical transient analysis of Markov models. Com- puters & Operations Research15(1), 19–36 (1988). https://doi.org/10.1016/0305- 0548(88)90026-3

    1988 doi

  38. [47]

    In: QEST

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

    2013 doi

  39. [48]

    ACM Trans

    Reijsbergen, D., de Boer, P., Scheinhardt, W.R.W., Juneja, S.: Path-ZVA: Gen- eral, efficient, and automated importance sampling for highly reliable Markovian systems. ACM Trans. Model. Comput. Simul. 28(3), 22:1–22:25 (2018). ht- tps://doi.org/10.1145/3161569

    2018 doi

  40. [49]

    Rubino, G., Tuffin, B.: Introduction to Rare Event Simulation, chap. 1, pp. 1–13. In: Rubino and Tuffin [50] (2009). https://doi.org/10.1002/9780470745403.ch1

    2009 doi

  41. [50]

    (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

    2009 doi

  42. [51]

    Performance Evaluation45(4), 205–221 (2001)

    Telek, M., Horváth, A.: Transient analysis of Age-MRSPNs by the method of supplementary variables. Performance Evaluation45(4), 205–221 (2001)

    2001

  43. [52]

    Cambridge Univ

    Trivedi, K.S., Bobbio, A.: Reliability and availability engineering: modeling, analysis, and applications. Cambridge Univ. Press (2017)

    2017

  44. [53]

    IEEE Transactions on Software Engineering 27(8), 728–748 (2001)

    Vicario, E.: Static analysis and dynamic steering of time-dependent sys- tems. IEEE Transactions on Software Engineering 27(8), 728–748 (2001). ht- tps://doi.org/10.1109/32.940727

    2001 doi

  45. [54]

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

    Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantit- ative evaluation of dense-time reactive systems. IEEE Transactions on Software Engineering 35(5), 703–719 (2009)

    2009

  46. [55]

    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

  47. [56]

    In: CAV 2002

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

    2002 doi

  48. [406]

    https://doi.org/10.1109/LICS.1992.185551, https://doi.org/10.1109/LICS.1992.185551

    IEEE Computer Society (1992). https://doi.org/10.1109/LICS.1992.185551, https://doi.org/10.1109/LICS.1992.185551

    1992

Pith tools

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