Skip to main content
SpringerLink
Log in

Computation tree measurement language (CTML)

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

In this work, we present a formal language, CTML, to reason over probabilistic systems. CTML extends stochastic temporal logics in a way that it takes a real value as input and output a real value in the range of \({[0, \infty)}\), as opposed to 0/1 values as input and output, and it can nest real values. This allows CTML to express a rich set of queries towards the unification of model checking and performance evaluation. In fact, CTML covers PCTL. It can express a nontrivial subset of PLTL formulas that cannot be expressed by PCTL. The significance of this result is that the overall complexity of CTML is linear, as opposed to exponential as it is with PLTL, in the size of the operators for a given formula, and polynomial in the size of a given model. Moreover, CTML can express real-valued performance queries such as: “if a system encounters a failure, what is the expected time to reach a recovery state?” that cannot be expressed by a probabilistic model checking logic, because they are “probabilistic” at most. Along with the specification language, we present a set of algorithms for the evaluation of the language and show proofs for their correctness. Additionally, we include an application example and show experimental results.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Andova S, Hermanns H, Katoen J-P (2003) Discrete-time rewards model-checked. In: Larsen KG, Niebert P (eds) Formal modelling and analysis of timed systems, volume 2791 of Lecture notes in computer science. Springer, pp 88–104

  2. Aziz A, Singhal V, Balarin F (1995) It usually works: The temporal logic of stochastic systems. In: Proceedings of the 7th international conference on computer aided verification, London, UK. Springer, pp 155–165

  3. Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans Softw Eng 33, 209–224 (2007)

    Article  Google Scholar 

  4. Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Proceedings of the 15th conference on foundations of software technology and theoretical computer science, Berlin, Heidelberg. Springer, pp 499–513

  5. Beaudry DM (1978) Performance-related reliability measures for computing systems. IEEE Trans Comput C-27(6):540–547

  6. Borgerson BR, Freitas RF (1975) A reliability model for gracefully degrading and standby-sparing systems. IEEE Trans Comput C-24(5):517–525

  7. Baier C, Haverkort BR, Hermanns H, Katoen J-P (2000) On the logical characterisation of performability properties. In: Proceedings of the 27th international colloquium on automata, languages and programming, London, UK. Springer, pp 780–792

  8. 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  MATH  Google Scholar 

  9. Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math Oper Res 16(3), 580–595 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  10. Çinlar, E.: Introduction to stochastic processes. Prentice-Hall, Englewood Cliffs (1975)

    MATH  Google Scholar 

  11. Clark G, Gilmore S, Hillston J (1999) Specifying performance measures for PEPA. In: Proceedings of the 5th international AMAST workshop on formal methods for real-time and probabilistic systems, London, UK. Springer, pp 211–227

  12. Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)

    Google Scholar 

  13. Chung KL (1979) Elementary probability theory with stochastic processes. Undergraduate texts in mathematics, 3rd edn. Springer, Orlando

  14. Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logic and stochastic modeling with SMART. Perform Eval 63(6), 578–608 (2006)

    Article  Google Scholar 

  15. Cohn, D.L.: Measure theory. Birkhäuser, Boston (1980)

    Book  MATH  Google Scholar 

  16. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  17. de Alfaro L (1997) Temporal logics for the specification of performance and reliability. In: Proceedings of the 14th annual symposium on theoretical aspects of computer science, London, UK. Springer, pp 165–176

  18. de Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Proceedings of the 10th international conference on concurrency theory, London, UK. Springer, pp 66–81

  19. de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theoret Comput Sci 345(1), 139–170 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  20. Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL\(^{{\text{TA}}}\). IEEE Trans Softw Eng 35(2), 224–240 (2009)

    Article  Google Scholar 

  21. Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Inform 1, 115–138 (1971)

    Article  MathSciNet  Google Scholar 

  22. Emerson EA (1990) Temporal and modal logic. In: Handbook of theoretical computer science. Elsevier, pp 995–1072

  23. Gaonkar, S., Keefe, K., Lamprecht, R., Rozier, E., Kemper, P., Sanders, W.H.: Performance and dependability modeling with möbius. SIGMETRICS Perform Eval Rev 36(4), 16–21 (2009)

    Article  Google Scholar 

  24. Grinstead CM, Snell JL (2003) Introduction to probability. American Mathematical Society

  25. Haverkort BR, Cloth L, Hermanns H, Katoen J-P (2002) Model checking performability properties. In: Proceedings of the 2002 international conference on dependable systems and networks, Washington, DC, USA. IEEE Computer Society, pp 103–112

  26. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form Asp Comput 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  27. Harrison, P.G., Knottenbelt, W.J.: Passage time distributions in large Markov chains. SIGMETRICS Perform Eval Rev 30(1), 77–85 (2002)

    Article  Google Scholar 

  28. Jing Yaping (2015) A formal language towards the unification of model checking and performance evaluation. PhD thesis, Iowa State University, Ames, IA

  29. Kwiatkowska, M., Norman, G., Parker, D.: Prism: probabilistic model checking for performance and reliability analysis. SIGMETRICS Perform Eval Rev 36(4), 40–45 (2009)

    Article  Google Scholar 

  30. Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of 23rd international conference on computer aided verification, volume 6806 of LNCS. Springer, pp 585–591

  31. Kwiatkowska M, Norman G, Parker D, Sproston J (2003) Performance analysis of probabilistic timed automata using digital clocks. In: Proceedings of formal modeling and analysis of timed systems, volume 2791 of LNCS. Springer, pp 105–120

  32. Kemeny, J.G., Snell, J.L.: Finite Markov Chains. D. Van Nostrand Company Inc, Princeton (1960)

    MATH  Google Scholar 

  33. Kwiatkowska M (2007) Quantitative verification: models techniques and tools. In: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, New York, NY, USA, ACM, pp 449–458

  34. Laroussinie, F., Sproston, J.: Model checking durational probabilistic systems. In: Vladimiro, S. (ed.) 8th international conference on foundations of software science and computational structures. Springer, vol. 3441, pp. 140–154. Berlin, Heidelberg (2005)

    Google Scholar 

  35. Liu Y, Trivedi KS (2004) A general framework for network survivability quantification. In: Peter B, Ralf L, Michal P (eds) MMB. VDE Verlag, pp 369–378

  36. Muppala JK, Ciardo G, Trivedi KS (1993) Modeling using stochastic reward nets. In: Proceedings of the international workshop on modeling, analysis, and simulation on computer and telecommunication systems. Society for Computer Simulation, pp 367–372

  37. Meyer JF (1980) On evaluating the performability of degradable computing systems. IEEE Trans Comput C-29(8):720–731

  38. Miner, A.S.: Implicit GSPN reachability set generation using decision diagrams. Perform Eval 56(1–4), 145–165 (2004)

    Article  Google Scholar 

  39. Miner AS, Jing Y (2010) A formal language toward the unification of model checking and performance evaluation. In: Analytical and stochastic modeling techniques and applications, pp 130–144

  40. Obal, W.D., Sanders, W.H.: State-space support for path-based reward variables. Perform Eval 35(3–4), 233–251 (1999)

    Article  MATH  Google Scholar 

  41. Pnueli, A.: The temporal semantics of concurrent programs. Theoret Comput Sci 13, 45–60 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  42. Ross, S.M.: Introduction to probability models, 9th edn. Academic, Orlando (2006)

    MATH  Google Scholar 

  43. Suto T, Bradley JT, Knottenbelt WJ (2007) Performance trees: Expressiveness and quantitative semantics. In: Proceedings of the fourth international conference on quantitative evaluation of systems, Washington, DC, USA. IEEE Computer Society, pp 41–50

  44. Schnoebelen P (2002) The complexity of temporal logic model checking. In: Advances in modal logic, pp 393–436

  45. Stewart WJ (1994) Introduction to the numerical solution of Markov Chains. Princeton University Press

  46. Trivedi, K.S., Ciardo, G., Malhotra, M., Sahner, R.A.: Dependability and performability analysis. Performance evaluation of computer and communication systems, joint tutorial papers of performance’93 and Sigmetrics’93, pp. 587–612. UK, Springer, London (1993)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Math and Computer Science, Salisbury University, Salisbury, MD, USA

    Yaping Jing

  2. Department of Computer Science, Iowa State University, Ames, IA, USA

    Andrew S. Miner

Authors
  1. Yaping Jing
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew S. Miner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yaping Jing.

Additional information

Communicated by Jin Song Dong

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Jing, Y., Miner, A.S. Computation tree measurement language (CTML). Form Asp Comp 30, 443–462 (2018). https://doi.org/10.1007/s00165-018-0457-3

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-018-0457-3

Keywords

Search

Navigation