Skip to main content
SpringerLink
Log in
Book cover

International Conference on Quantitative Evaluation of Systems

QEST 2013: Quantitative Evaluation of Systems pp 355–371Cite as

Transient Analysis of Networks of Stochastic Timed Automata Using Stochastic State Classes

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8054))

Abstract

Stochastic Timed Automata (STA) associate logical locations with continuous, generally distributed sojourn times. In this paper, we introduce Networks of Stochastic Timed Automata (NSTA), where the components interact with each other by message broadcasts. This results in an underlying stochastic process whose state is made of the vector of logical locations, the remaining sojourn times, and the value of clocks. We characterize this general state space Markov process through transient stochastic state classes that sample the state and the absolute age after each event. This provides an algorithmic approach to transient analysis of NSTA models, with fairly general termination conditions which we characterize with respect to structural properties of individual components that can be checked through straightforward algorithms.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Bernadsky, M.: Bounded model checking for GSMP models of stochastic real-time systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 19–33. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Alur, R., Courcoubetis, C., Dill, D.: Model-checking for Probabilistic Real-time Systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 115–126. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  3. Alur, R., Courcoubetis, C., Dill, D.L.: Verifying Automata Specifications of Probabilistic Real-time Systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 28–44. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  4. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Probabilistic and topological semantics for timed automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179–191. Springer, Heidelberg (2007)

    Google Scholar 

  6. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: LICS 2008, pp. 217–226. IEEE CS (2008)

    Google Scholar 

  7. Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST 2008, pp. 55–64. IEEE CS (2008)

    Google Scholar 

  9. Bobbio, A., Telek, M.: Markov regenerative SPN with non-overlapping activity cycles. In: IPDS 1995, pp. 124–133. IEEE CS (1995)

    Google Scholar 

  10. Bouyer, P., Brihaye, T., Jurdzinski, M., Menet, Q.: Almost-sure model-checking of reactive timed automata. In: QEST 2012, pp. 138–147. IEEE CS (2012)

    Google Scholar 

  11. Bucci, G., Carnevali, L., Ridi, L., Vicario, E.: Oris: a tool for modeling, verification and evaluation of real-time systems. Int. J. on Softw. Tools for Techn. Transfer 12(5), 391–403 (2010)

    Article  Google Scholar 

  12. Bucci, G., Piovosi, R., Sassoli, L., Vicario, E.: Introducing probability within state class analysis of dense time dependent systems. In: QEST 2005, pp. 13–22. IEEE CS (2005)

    Google Scholar 

  13. Carnevali, L., Grassi, L., Vicario, E.: State-density functions over DBM domains in the analysis of non-Markovian models. IEEE Trans. Softw. Eng. 35(2), 178–194 (2009)

    Article  Google Scholar 

  14. Carnevali, L., Ridi, L., Vicario, E.: A framework for simulation and symbolic state space analysis of non-Markovian models. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 409–422. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  15. Ciardo, G., German, R., Lindemann, C.: A characterization of the stochastic process underlying a stochastic Petri net. IEEE Trans. Softw. Eng. 20(7), 506–515 (1994)

    Article  Google Scholar 

  16. Cox, D.R.: The analysis of non-Markovian stochastic processes by the inclusion of supplementary variables. Math. Proc. Cambridge 51, 433–441 (1955)

    Article  MATH  Google Scholar 

  17. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  18. Haas, P.J.: Stochastic Petri Nets: Modelling, Stability, Simulation. Springer (2002)

    Google Scholar 

  19. Horváth, A., Paolieri, M., Ridi, L., Vicario, E.: Probabilistic model checking of non-Markovian models with concurrent generally distributed timers. In: QEST 2011, pp. 131–140. IEEE CS (2011)

    Google Scholar 

  20. Horváth, A., Paolieri, M., Ridi, L., Vicario, E.: Transient analysis of non-Markovian models using stochastic state classes. Perform. Eval. 69(7-8), 315–335 (2012)

    Article  Google Scholar 

  21. Kulkarni, V.: Modeling and analysis of stochastic systems. Chapman & Hall (1995)

    Google Scholar 

  22. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  23. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 123–137. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  24. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  25. Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: INFINITY, pp. 33–46 (2010)

    Google Scholar 

  26. Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. Softw. Eng. 35(5), 703–719 (2009)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Centrale Paris, France

    Paolo Ballarini

  2. Inria Rennes, France

    Nathalie Bertrand

  3. Università di Torino, Italy

    András Horváth

  4. Università di Firenze, Italy

    Marco Paolieri & Enrico Vicario

Authors
  1. Paolo Ballarini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nathalie Bertrand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. András Horváth
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marco Paolieri
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Enrico Vicario
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. AT&T Labs Research, 180 Park Avenue, Building 103, 07932, Florham Park, NJ, USA

    Kaustubh Joshi

  2. Institut für Technische Informatik, Universität der Bundeswehr München, Werner-Heisenberg Weg 39, 85577, Neubiberg, Germany

    Markus Siegle

  3. Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, Drienerlolaan 5, Zilverling Building, 7522 NB, Enschede, The Netherlands

    Mariëlle Stoelinga

  4. Facultad de Matemáticas, Astronomía y Física, Universidad Nacional de Córdoba – CONICET, Medina Allende s/n, X5000HUA, Córdoba, Argentina

    Pedro R. D’Argenio

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ballarini, P., Bertrand, N., Horváth, A., Paolieri, M., Vicario, E. (2013). Transient Analysis of Networks of Stochastic Timed Automata Using Stochastic State Classes. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds) Quantitative Evaluation of Systems. QEST 2013. Lecture Notes in Computer Science, vol 8054. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40196-1_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40196-1_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40195-4

  • Online ISBN: 978-3-642-40196-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation