Skip to main content
SpringerLink
Log in
Book cover

European Workshop on Performance Engineering

EPEW 2013: Computer Performance Engineering pp 58–73Cite as

Tackling Truncation Errors in CSL Model Checking through Bounding Semantics

  • Conference paper

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

Abstract

Model checking aims to give exact answers to queries about a model’s execution but, in probabilistic model checking, ensuring exact answers might be difficult. Numerical iterative methods are heavily used in probabilistic model checking and errors caused by truncation may affect correctness. To tackle truncation errors, we investigate the bounding semantics of continuous stochastic logic for Markov chains. We first focus on analyzing truncation errors for model-checking the time-bounded or unbounded Until operator and propose new algorithms to generate lower and upper bounds. Then, we study the bounding semantics for a subset of nested CSL formulas. We demonstrate result on two models.

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. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  2. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)

    Article  Google Scholar 

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

    Google Scholar 

  4. Berman, A., Plemmons, R.: Nonnegative Matrices in the Mathematical Sciences. SIAM (1979)

    Google Scholar 

  5. Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval. 63, 578–608 (2006)

    Article  Google Scholar 

  6. Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: A Petri Net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 51–95. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)

    Google Scholar 

  8. Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Fox, B.L., Glynn, P.W.: Computing Poisson Probabilities. Comm. ACM 31(4), 440–445 (1988)

    Article  MathSciNet  Google Scholar 

  10. Grassmann, W.K.: Finding transient solutions in Markovian event systems through randomization. In: Numerical Solution of Markov Chains, pp. 357–371. Marcel Dekker, Inc. (1991)

    Google Scholar 

  11. Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-Valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Katoen, J.-P., Kwiatkowska, M., Norman, G., Parker, D.: Faster and symbolic CTMC model checking. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 23–38. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. 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 

  14. Models in this paper, http://www.cs.ucr.edu/~zhaoy/EPEW2013.html

  15. Muppala, J.K., Ciardo, G., Trivedi, K.S.: Stochastic reward nets for reliability prediction. Communications in Reliability, Maintenability and Serviceability 1(2), 9–20 (1994)

    Google Scholar 

  16. Wan, M., Ciardo, G., Miner, A.S.: Approximate steady-state analysis of large Markov models based on the structure of their decision diagram encoding. Perf. Eval. 68, 463–486 (2011)

    Article  Google Scholar 

  17. Zhao, Y., Ciardo, G.: A two-phase Gauss-Seidel algorithm for steady-state solution of structured CTMCs encoded with EVMDDs. In: Proc. QEST, London, UK, pp. 74–83. IEEE Comp. Soc. Press (September 2012)

    Google Scholar 

  18. Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. In: Proc. AVoCS. Electronic Communications of the EASST. European Association of Software Science and Technology, vol. 53 (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of California, Riverside, USA

    Yang Zhao & Gianfranco Ciardo

Authors
  1. Yang Zhao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gianfranco Ciardo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Scienze Ambientali, Informatica e Statistica, Università Ca’ Foscari di Venezia, via Torino 155, 30170, Venezia, Italy

    Maria Simonetta Balsamo  & Andrea Marin  & 

  2. Department of Computing, Imperial College London, South Kensington Campus, SW7 2AZ, London, UK

    William J. Knottenbelt

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhao, Y., Ciardo, G. (2013). Tackling Truncation Errors in CSL Model Checking through Bounding Semantics. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds) Computer Performance Engineering. EPEW 2013. Lecture Notes in Computer Science, vol 8168. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40725-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40725-3_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40724-6

  • Online ISBN: 978-3-642-40725-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation