pith. sign in

arxiv: 2607.00782 · v1 · pith:N55CC5CJnew · submitted 2026-07-01 · 💻 cs.LO

Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

Pedro R. D'Argenio , Arnd Hartmanns , Annabell Petri This is my paper

Pith reviewed 2026-07-02 04:05 UTC · model grok-4.3

classification 💻 cs.LO
keywords stochastic automatamodel checkinginterval abstractionreachability probabilitiescontinuous distributionsbig time stepsformal verification
0
0 comments X

The pith

Interval abstraction with big time steps yields bounds for general stochastic automata checking

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

The paper develops a model checking method for stochastic automata that accepts arbitrary continuous probability distributions on timer expirations. It abstracts those distributions into refinable intervals and applies the big time steps semantics directly to obtain sound upper and lower bounds on maximum and minimum reachability probabilities. The approach places few restrictions on the input models and is shown to scale to nontrivial examples via a prototype implementation that extends existing modeling languages.

Core claim

The central claim is that combining a refinable interval abstraction of continuous distributions with the direct application of the big time steps semantics produces sound upper and lower bounds on extremal reachability probabilities for stochastic automata, constituting the first dedicated model checking approach that is both general and effective.

What carries the argument

Refinable interval abstraction of arbitrary continuous distributions paired with the big time steps semantics of stochastic automata

If this is right

  • Reachability probabilities in systems with faults, maintenance, and repairs modeled by general distributions can be bounded.
  • Existing modeling languages can be extended to support stochastic automata without major changes.
  • A practical implementation exists that handles nontrivial models in reasonable time.
  • Analysis shifts from statistical sampling or restricted distribution families to deterministic interval-based verification.

Where Pith is reading between the lines

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

  • The same abstraction technique could be tested on other continuous-time formalisms that rely on countdown timers.
  • Tighter intervals or adaptive refinement strategies might reduce bound width on larger models.
  • The bounds could serve as starting points for statistical model checking to narrow uncertainty further.

Load-bearing premise

The interval abstraction must produce sound bounds on extremal reachability probabilities when paired with big time steps semantics for distributions outside restricted families.

What would settle it

A concrete stochastic automaton example where an actual maximum or minimum reachability probability computed by simulation or exact analysis falls outside the interval bounds returned by the method.

Figures

Figures reproduced from arXiv: 2607.00782 by Annabell Petri, Arnd Hartmanns, Pedro R. D'Argenio.

Figure 1
Figure 1. Figure 1: Example SA Mre . R({x, y}). We omit empty reset sets. In general, SA are compositional: They can be equipped with a notion of parallel composition and an open semantics with dense time steps and without maximal progress. This facilitates elegant and compact models of systems consisting of concurrent components. For analysis, usually the composition’s closed seman￾tics which excludes parallel composition an… view at source ↗
Figure 2
Figure 2. Figure 2: Excerpt of ia(Mre ) created with per-interval probability 0.5. The superscript intervals denote the possible valuations for timers x (on the left) and y (on the right). (i) are in G, (ii) have previously expired, or (iii) whose upper bound is at most lb(G) (which applies to timers not in G that have “low” values). In the second case, we have an unexpired timer x /∈ G that is not forced to expire now. Its l… view at source ↗
Figure 3
Figure 3. Figure 3: Transformations of the semantics of the SA M′ re . ia(JMK), it now leads into a discrete distribution (solid dot ) over sets of states out of which one is chosen nondeterministically (outlined dots ). The (reachable) states of JMK and ia(JMK) are the same, as is the transition graph structure. Given a strategy s for JMK, we can construct a randomised strategy sJiaK for ia(JMK) that induces the exact same p… view at source ↗
Figure 4
Figure 4. Figure 4: Modest model for Mre . Implementing a new tool for the analysis of SA would now require imple￾menting a parser for either IOSA (if its restrictions are acceptable) or Modest, which is a large and tedious task in either case. To reduce such burden on tool developers, the JSON-based Jani format was designed as a model interchange [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: SA M1 ℓ0 M2: x: Uni(0, 8) y : Uni(0, 1) z : Uni(0, 4) ℓ1 ℓ2 ℓ3 ℓ4 ✓ ✗ ∅ R({x, z}) {x} R({z}) {z} R({z}) ∅ R({y}) ∅ R({y}) {x} {y} {y} {x} [PITH_FULL_IMAGE:figures/full_fig_p021_5.png] view at source ↗
read the original abstract

Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularly useful to faithfully model and analyse dependable systems involving faults, maintenance, and repairs. Effective SA analysis approaches have so far been limited to statistical model checking and thus deterministic SA, while previously proposed model-checking techniques apply to limited subclasses of SA only, or do not scale. In this paper, we present the first dedicated SA model checking approach that is general and effective: It puts few restrictions on the input SA, and we show in our experimental evaluation that it works well for nontrivial examples. It combines a refinable interval abstraction of the continuous distributions with a direct application of the "big time steps" semantics of SA, providing upper/lower bounds on maximum/minimum reachability probabilities. We extend the Modest and Jani modelling formalisms with support for SA, and provide a prototype implementation of our approach in Rust.

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

0 major / 3 minor

Summary. The paper claims to introduce the first general and effective dedicated model-checking approach for stochastic automata (SA) with arbitrary continuous distributions. It combines a refinable interval abstraction of the distributions with the big time steps semantics to compute sound upper/lower bounds on maximum/minimum reachability probabilities. The method imposes few restrictions on input SA, is implemented in a Rust prototype, and is shown effective on nontrivial examples; the Modest and Jani formalisms are extended to support SA.

Significance. If the soundness of the interval abstraction and the experimental results hold, the work would constitute a meaningful advance in stochastic model checking by enabling analysis of general SA models for dependable systems (faults, maintenance, repairs) without restricting to statistical methods, deterministic SA, or narrow distribution families.

minor comments (3)
  1. [Abstract] The abstract states that the approach 'puts few restrictions on the input SA' and works 'well for nontrivial examples,' but the manuscript should explicitly list the remaining restrictions (e.g., on timer dependencies or distribution support) in §2 or §3 to allow readers to assess generality.
  2. [Related work] The claim that the method is 'the first dedicated SA model checking approach that is general and effective' should be supported by a concise comparison table in the related-work section contrasting the new technique against prior statistical and limited-subclass methods.
  3. [Experimental evaluation] The experimental evaluation is referenced but not described in the provided abstract; the full manuscript should report concrete metrics (e.g., number of benchmarks, state-space sizes, bound tightness, runtime) in a dedicated section or table.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work and the recommendation of minor revision. The report contains no specific major comments requiring point-by-point rebuttal.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper presents a new algorithmic method combining refinable interval abstraction of arbitrary continuous distributions with big time steps semantics to obtain sound bounds on extremal reachability probabilities for general SA. No derivation step reduces by construction to fitted parameters, self-definitions, or load-bearing self-citations; the soundness claim and effectiveness are positioned as the contribution, backed by experiments on nontrivial cases. The approach is self-contained against external benchmarks with no quoted reductions matching the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard definitions of stochastic automata and reachability probabilities; no free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • standard math Standard definitions of stochastic automata, continuous probability distributions, and reachability probabilities in continuous time.
    Invoked to define the input model and the quantities to be bounded.

pith-pipeline@v0.9.1-grok · 5700 in / 1142 out tokens · 35237 ms · 2026-07-02T04:05:37.370100+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

41 extracted references · 29 canonical work pages

  1. [1]

    Agha,G.,Palmskog,K.:Asurveyofstatisticalmodelchecking.ACMTrans.Model. Comput. Simul.28(1), 6:1–6:39 (2018).https://doi.org/10.1145/3158668

    work page doi:10.1145/3158668 2018

  2. [2]

    In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R

    Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Hand- book of Model Checking, pp. 963–999. Springer (2018).https://doi.org/10. 1007/978-3-319-10575-8_28

    2018

  3. [3]

    IEEE Trans

    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng.29(6), 524–541 (2003).https://doi.org/10.1109/TSE.2003.1205180

    work page doi:10.1109/tse.2003.1205180 2003

  4. [4]

    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM53(9), 76–85 (2010).https:// doi.org/10.1145/1810891.1810912

    work page doi:10.1145/1810891.1810912 2010

  5. [5]

    Journal of Mathematics and Mechanics 6(5), 679–684 (1957)

    Bellman, R.: A Markovian decision process. Journal of Mathematics and Mechanics 6(5), 679–684 (1957)

    1957

  6. [6]

    IEEE Trans

    Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng.32(10), 812–830 (2006).https://doi.org/10.1109/TSE.2006.104

    work page doi:10.1109/tse.2006.104 2006

  7. [7]

    ACM Trans

    Bryans, J.W., Bowman, H., Derrick, J.: Model checking stochastic automata. ACM Trans. Comput. Log.4(4), 452–492 (2003).https://doi.org/10.1145/937555. 937558

    work page doi:10.1145/937555 2003

  8. [8]

    In: 44th Annual IEEE/IFIP Interna- tional Conference on Dependable Systems and Networks (DSN 2014)

    Buchholz, P., Kriege, J., Scheftelowitsch, D.: Model checking stochastic automata for dependability and performance measures. In: 44th Annual IEEE/IFIP Interna- tional Conference on Dependable Systems and Networks (DSN 2014). pp. 503–514. IEEE Computer Society (2014).https://doi.org/10.1109/DSN.2014.53

    work page doi:10.1109/dsn.2014.53 2014

  9. [9]

    SIGMETRICS Per- form

    Budde, C.E.: FIG: the finite improbability generator v1.3. SIGMETRICS Per- form. Evaluation Rev.49(4), 59–64 (2022).https://doi.org/10.1145/3543146. 3543160

    work page doi:10.1145/3543146 2022

  10. [10]

    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

    work page doi:10.1007/s10009-020-00563-2 2020

  11. [11]

    In: Legay, A., Margaria, T

    Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and AnalysisofSystems(TACAS2017).LectureNotesinComputerScience,vol.10206, pp. 151–168. Springer (2017).https://doi.org/10....

    work page doi:10.1007/978-3-662-54580-5_9 2017

  12. [12]

    D’Argenio, P.R.: Algebras and Automata for Timed and Stochastic Systems. Ph.D. thesis, University of Twente, Nether- lands (1999),https://research.utwente.nl/en/publications/ algebras-and-automata-for-timed-and-stochastic-systems

    1999

  13. [13]

    In: Baier, C., Lago, U.D

    D’Argenio, P.R., Gerhold, M., Hartmanns, A., Sedwards, S.: A hierarchy of sched- uler classes for stochastic automata. In: Baier, C., Lago, U.D. (eds.) 21st Interna- tional Conference on Foundations of Software Science and Computation Structures (FOSSACS 2018). Lecture Notes in Computer Science, vol. 10803, pp. 384–402. Springer (2018).https://doi.org/10....

    work page doi:10.1007/978-3-319-89366-2_21 2018

  14. [14]

    D’Argenio, P.R., Katoen, J.P.: A theory of stochastic systems part I: Stochastic automata. Inf. Comput.203(1), 1–38 (2005).https://doi.org/10.1016/J.IC. 2005.07.001 18 P. R. D’Argenio, A. Hartmanns, A. Petri

    work page doi:10.1016/j.ic 2005

  15. [15]

    In: Fischer, B., Uustalu, T

    D’Argenio, P.R., Monti, R.E.: Input/output stochastic automata with urgency: Confluence and weak determinism. In: Fischer, B., Uustalu, T. (eds.) 15th In- ternational Colloquium on Theoretical Aspects of Computing (ICTAC 2018). Lecture Notes in Computer Science, vol. 11187, pp. 132–152. Springer (2018). https://doi.org/10.1007/978-3-030-02508-3_8

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

  16. [16]

    In: Kalyvianaki, E., Paolieri, M

    Delicaris, J., Stübbe, J., Schupp, S., Remke, A.: RealySt: A C++ tool for op- timizing reachability probabilities in stochastic hybrid systems. In: Kalyvianaki, E., Paolieri, M. (eds.) 16th EAI International Conference on Performance Evalu- ation Methodologies and Tools (VALUETOOLS 2023). Lecture Notes of the In- stitute for Computer Sciences, Social Info...

    2023

  17. [17]

    In: Prabhakar, P., Vandin, A

    Dengler, G., Budde, C.E., Carnevali, L., Hartmanns, A.: Time-sensitive impor- tance splitting. In: Prabhakar, P., Vandin, A. (eds.) 2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS 2025). Lecture Notes in Com- puter Science, vol. 16143, pp. 21–41. Springer (2025).https...

    2025

  18. [18]

    In: Colom, J.M., Desel, J

    Eisentraut, C., Hermanns, H., Katoen, J.P., Zhang, L.: A semantics for every GSPN. In: Colom, J.M., Desel, J. (eds.) 34th International Conference on Ap- plication and Theory of Petri Nets and Concurrency (Petri Nets 2013). Lec- ture Notes in Computer Science, vol. 7927, pp. 90–109. Springer (2013).https: //doi.org/10.1007/978-3-642-38697-8_6

    work page doi:10.1007/978-3-642-38697-8_6 2013

  19. [19]

    In: Abdulla, P.A., Leino, K.R.M

    Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011). Lecture Notes in Com- puter Science, vol. 6605, pp. 112–127. Springer (2...

    2011

  20. [20]

    In: Caccamo, M., Fraz- zoli, E., Grosu, R

    Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurabil- ity and safety verification for stochastic hybrid systems. In: Caccamo, M., Fraz- zoli, E., Grosu, R. (eds.) 14th ACM International Conference on Hybrid Sys- tems: Computation and Control (HSCC 2011). pp. 43–52. ACM (2011).https: //doi.org/10.1145/1967701.1967710

    work page doi:10.1145/1967701.1967710 2011

  21. [21]

    Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf.10(3), 263–279 (2008).https://doi.org/10.1007/ S10009-007-0062-X

    2008

  22. [22]

    In: Haviv, M., Knottenbelt, W.J., Maggi, L., Mio- randi, D

    Ghasemieh, H., Remke, A., Haverkort, B.R.: Hybrid Petri nets with multiple stochastic transition firings. In: Haviv, M., Knottenbelt, W.J., Maggi, L., Mio- randi, D. (eds.) 8th International Conference on Performance Evaluation Method- ologies and Tools (VALUETOOLS 2014). pp. 217–224. ICST (2014).https: //doi.org/10.4108/icst.valuetools.2014.258204

    work page doi:10.4108/icst.valuetools.2014.258204 2014

  23. [23]

    Hahn, E.M.: Model checking stochastic hybrid systems. Ph.D. thesis, Saarland Uni- versity (2013),http://scidok.sulb.uni-saarland.de/volltexte/2013/5259/

    2013

  24. [24]

    Electron

    Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70(2014).https://doi.org/10.14279/TUJ.ECEASST.70.968

    work page doi:10.14279/tuj.eceasst.70.968 2014

  25. [25]

    Formal Methods Syst

    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional mod- elling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des.43(2), 191–232 (2013).https://doi.org/10.1007/S10703-012-0167-Z Stochastic Automata Model Checking by Interval Abstraction 19

    work page doi:10.1007/s10703-012-0167-z 2013

  26. [26]

    In: 8th International Conference on Quantitative Evaluation of Systems (QEST 2011)

    Hahn, E.M., Norman, G., Parker, D., Wachter, B., Zhang, L.: Game-based abstrac- tion and controller synthesis for probabilistic hybrid systems. In: 8th International Conference on Quantitative Evaluation of Systems (QEST 2011). pp. 69–78. IEEE Computer Society (2011).https://doi.org/10.1109/QEST.2011.17

    work page doi:10.1109/qest.2011.17 2011

  27. [27]

    In: Fisman, D., Rosu, G

    Hartmanns, A.: Correct probabilistic model checking with floating-point arith- metic. In: Fisman, D., Rosu, G. (eds.) 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). Lecture Notes in Computer Science, vol. 13244, pp. 41–59. Springer (2022). https://doi.org/10.1007/978-3-030-99527-0_3

    work page doi:10.1007/978-3-030-99527-0_3 2022

  28. [28]

    In: Ábrahám, E., Havelund, K

    Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Lecture Notes in Computer Science, vol. 8413, pp. 593–598. Springer (2014).https://doi....

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

  29. [29]

    In: Sankaranarayanan, S., Sharygina, N

    Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) 29th International Conference on Tools and Algorithms for the Construction and AnalysisofSystems(TACAS2023).LectureNotesinComputerScience,vol.13993, pp. 469–488. Springer (2023).https://doi.org/10....

    work page doi:10.1007/978-3-031-30823-9_24 2023

  30. [30]

    (ed.) 19th International Colloquium on Automata, Languages and Program- ming (ICALP 1992)

    Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) 19th International Colloquium on Automata, Languages and Program- ming (ICALP 1992). Lecture Notes in Computer Science, vol. 623, pp. 545–558. Springer (1992).https://doi.org/10.1007/3-540-55719-9_103

    work page doi:10.1007/3-540-55719-9_103 1992

  31. [31]

    MIT Press (1960)

    Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press (1960)

    1960

  32. [32]

    In: Ouaknine, J., Vaandrager, F.W

    Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) 7th Inter- national Conference on Formal Modeling and Analysis of Timed Systems (FOR- MATS 2009). Lecture Notes in Computer Science, vol. 5813, pp. 212–227. Springer (2009).https://doi.org/10.1007/978-3-64...

    work page doi:10.1007/978-3-642-04368-0_17 2009

  33. [33]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilis- tic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) 23rd International Conference on Computer Aided Verification (CAV 2011). Lecture Notes in Com- puter Science, vol. 6806, pp. 585–591. Springer (2011).https://doi.org/10.1007/ 978-3-642-22110-1_47

    2011

  34. [34]

    Formal Methods Syst

    Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33–78 (2006).https://doi.org/10.1007/S10703-006-0005-2

    work page doi:10.1007/s10703-006-0005-2 2006

  35. [35]

    Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002).https://doi.org/10.1016/S0304-3975(01)00046-9

    work page doi:10.1016/s0304-3975(01)00046-9 2002

  36. [36]

    In: Steffen, B., Woeginger, G.J

    Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Sta- tistical model checking. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science – State of the Art and Perspectives, Lecture Notes in Com- puter Science, vol. 10000, pp. 478–504. Springer (2019).https://doi.org/10. 1007/978-3-319-91908-9_23

    2019

  37. [37]

    ACM Trans

    Marsan, M.A., 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

    work page doi:10.1145/190.191 1984

  38. [38]

    Zenodo (2026).https://doi.org/10.5281/zenodo.19829349 20 P

    Petri, A.: Effective stochastic automata model checking by interval abstraction (artifact). Zenodo (2026).https://doi.org/10.5281/zenodo.19829349 20 P. R. D’Argenio, A. Hartmanns, A. Petri

    work page doi:10.5281/zenodo.19829349 2026

  39. [39]

    In: Joseph, M

    Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2000). Lecture Notes in Computer Science, 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_ 2000

  40. [40]

    Wolovick,N.:Continuousprobabilityandnondeterminisminlabeledtransitionsys- tems. Ph.D. thesis, Universidad Nacional de Córdoba, Córdoba, Argentina (2012)

    2012

  41. [41]

    In: Touili, T., Cook, B., Jackson, P.B

    Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. In: Touili, T., Cook, B., Jackson, P.B. (eds.) 22nd International Conference on Computer Aided Verification (CAV 2010). Lecture Notes in Computer Science, vol. 6174, pp. 196–211. Springer (2010).https:// doi.org/10.1007/978-3-642-14295-6_21 St...

    work page doi:10.1007/978-3-642-14295-6_21 2010