Skip to main content
SpringerLink
Log in

Model Checking for a Class of Performance Properties of Fluid Stochastic Models

  • Conference paper
Formal Methods and Stochastic Models for Performance Evaluation (EPEW 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4054))

Included in the following conference series:

Abstract

Recently, there is an explosive development of fluid approa- ches to computer and distributed systems. These approaches are inherently stochastic and generate continuous state space models. Usually, the performance measures for these systems are defined using probabilities of reaching certain sets of the state space. These measures are well understood in the discrete context and many efficient model checking procedures have been developed for specifications involving them. The continuous case is far more complicated and new methods are necessary. In this paper we propose a general model checking strategy founded on advanced concepts and results of stochastic analysis. Due to the problem complexity, in this paper, we achieve the first necessary step of characterizing mathematically the problem. We construct upper bounds for the performance measures using Martin capacities. We introduce a concept of bisimulation that preserves the performance measures and a metric that characterizes the bisimulation.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Pappas, G.J. (eds.): HSCC 2004. LNCS, vol. 2993. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  2. Bertsekas, D.P., Shreve, S.E.: Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific (1996)

    Google Scholar 

  3. Bohacek, S., Hespanha, J., Lee, J., Obraczka, K.: Modeling Data Communication Networks Using Hybrid Systems. IEEE/ACM Trans. on Networking (2006)

    Google Scholar 

  4. Borkar, V.S.: Probability Theory. An Advance Course. Springer, Heidelberg (1995)

    MATH  Google Scholar 

  5. Bujorianu, M.L.: Extended Stochastic Hybrid Systems and their Reachability Problem. In: [1], pp. 234–249 (2004)

    Google Scholar 

  6. Bujorianu, M.L., Lygeros, J., Bujorianu, M.C.: Bisimulation for General Stochastic Hybrid Systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 198–214. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Bujorianu, M.L.: Capacities and Markov Processes. Lib. Math. 24, 201–210 (2004)

    MATH  MathSciNet  Google Scholar 

  8. Bujorianu, M.L., Bujorianu, M.C.: Distributed Stochastic Hybrid Systems. In: Kucera, A. (ed.) Proceedings of IFAC 2005. Elsevier Press, Amsterdam (2005)

    Google Scholar 

  9. Bujorianu, M.L., Bujorianu, M.C., Blom, H.A.P.: Towards Model Checking Stochastic Hybrid Systems by Approximate Abstractions (Submitted)

    Google Scholar 

  10. Choquet, G.: Theory of Capacities. Annales de l’Institut Fourier, Grenoble 5, 131–291 (1953)

    MathSciNet  Google Scholar 

  11. Chung, K.L.: Probabilistic Approach in Potential Theory to the Equilibrium Problem. Annales de L’Institut Fourier,Grenoble 23, 313–322 (1973)

    MATH  Google Scholar 

  12. Ciardo, G., Nicol, D., Trivedi, K.S.: Discrete-Event Simulation of Fluid Stochastic Petri Nets. In: Proc. 7th Int. Workshop on Petri Nets and Performance Models, pp. 217–225 (1997)

    Google Scholar 

  13. Davis, M.H.A.: Markov Models and Optimization. Chapman & Hall, London (1993)

    MATH  Google Scholar 

  14. Desharnais, J., Gupta, V., Jagadeesan, Panangaden, P.: Weak Bisimulation is Sound and Complete for PCTL. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 355–370. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Dempster, D.: Upper and Lower Probabilities Induced by a Multi-valued Mapping. Ann. Math. Statist. 38, 325–339 (1967)

    Article  MATH  MathSciNet  Google Scholar 

  16. Dubois, D., Prade, H.: Modelling Uncertainty and Inductive Inference: A Survey of Recent Non-Additive Probability Systems. Acta Psychologica 68, 53–78 (1988)

    Article  Google Scholar 

  17. Fitzsimmons, P.J.: Markov Processes with Equal Capacities. J. Theor. Prob. 12, 271–292 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  18. Horton, G., Kulkarni, V., Nicol, D., Trivedi, K.S.: Fluid Stochastic Petri Nets: Theory, Applications, and Solution. Eur. J. Oper. Res. 105(1), 184–201 (1998)

    Article  MATH  Google Scholar 

  19. Huber, P.J.: Robust Statistics. Willey, New York (1980)

    Google Scholar 

  20. Hermanns, H., Katoen, J.-P.: Automated Compositional Markov Chain Generation for a Plain-old Telephone System. Science of Computer Programming 36(1), 97–127 (2000)

    Article  MATH  Google Scholar 

  21. Hespanha, J.P.: Stochastic Hybrid Systems: Application to Communication Networks. In: [1], pp. 387–401 (2004)

    Google Scholar 

  22. Kang, W., Kelly, F.P., Lee, N.H., Williams, R.J.: Fluid and Brownian Approximations for an Internet congestion control model. In: Proceedings of the 43rd IEEE Conference on Decision and Control (2004)

    Google Scholar 

  23. Kelly, F.P.: Mathematical Modelling of the Internet. In: Engquist, B., Schmid, W. (eds.) Mathematics Unlimited - 2001 and Beyond, pp. 670–685. Springer, Heidelberg (2001)

    Google Scholar 

  24. Kulkarni, V., Trivedi, K.S.: FSPNs: Fluid Stochastic Petri Nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 24–31. Springer, Heidelberg (1993)

    Google Scholar 

  25. Kwiatkowska, Norman, G., Parker, D., Sproston, J.: Performance Analysis of Probabilistic Timed Automata using Digital Clocks. In: Formal Methods in System Design. Springer, Heidelberg (to appear, 2006)

    Google Scholar 

  26. Kwiatkowska, M., Norman, G., Segal, R., Sproston, J.: Automatic Verification of Real Time Systems with Discrete Probability Distribution. Theoretical Computer Science 282, 101–150 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  27. NWO Project Description AiSHA: Abstraction in Stochastic and Hybrid process Algebra, www.onderzoekinformatie.nl/en/oi/nod/onderzoek/OND1303139

  28. Pola, G., Bujorianu, M.L., Lygeros, J., Di Benedetto, M.D.: Stochastic Hybrid Models: An Overview with applications to Air Traffic Management. In: Proccedings Analysis and Design of Hybrid Systems IFAC ADHS 2003, pp. 45–50 (2003)

    Google Scholar 

  29. Shafer, G.: A Mathematical Theory of Evidence. Princeton Univ. Press, Princeton (1976)

    MATH  Google Scholar 

  30. Schmeidler, D.: Subjective Probability and Expected Utility Without Additivity. Econometrica 57, 571–587 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  31. Viertl, R.: Statistical Methods for Non-Precise Data. CRC Press, Boca Raton (1996)

    Google Scholar 

  32. Walley, P.: Statistical Reasoning with Imprecise Probabilities. Chapman & Hall, Boca Raton (1991)

    MATH  Google Scholar 

  33. Wolter, K.: Second Order Fluid Stochastic Petri Nets: an Extension of GSPNs for Approximate and Continuous Modeling. In: World Congress on System Simulation, pp. 328–332 (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Computer Science, University of Twente,  

    Manuela L. Bujorianu

  2. Computing Laboratory, University of Kent, Canterbury CT2 7NF, UK

    Marius C. Bujorianu

Authors
  1. Manuela L. Bujorianu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marius C. Bujorianu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    András Horváth

  2. Department of Telecommunications, Technical University of Budapest, 1521, Budapest, Hungary

    Miklós Telek

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bujorianu, M.L., Bujorianu, M.C. (2006). Model Checking for a Class of Performance Properties of Fluid Stochastic Models. In: Horváth, A., Telek, M. (eds) Formal Methods and Stochastic Models for Performance Evaluation. EPEW 2006. Lecture Notes in Computer Science, vol 4054. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11777830_7

Download citation

  • DOI: https://doi.org/10.1007/11777830_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35362-1

  • Online ISBN: 978-3-540-35365-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation