Quantitative Temporal Logic Mechanized in HOL

  • Orieta Celiku
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


The paper describes an implementation in the HOL theorem prover of the quantitative Temporal Logic (qTL) of Morgan and McIver [18,4]. qTL is a branching-time temporal logic suitable for reasoning about probabilistic nondeterministic systems. The interaction between probabilities and nondeterminism, which is generally very difficult to reason about, is handled by interpreting the logic over real- rather than boolean-valued functions. In theqTL framework many laws of standard branching-time temporal logic generalize nicely giving access to a number of logical tools for reasoning about quantitative aspects of randomized algorithms.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Celiku, O., McIver, A.: Cost-based analysis of probabilistic programs mechanised in HOL. Nordic Journal of Computing 11(2), 102–128 (2004)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  4. 4.
    Erlangen-Twente Markov Chain Checker,
  5. 5.
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  6. 6.
    Hartonas-Garmhausen, V., Campos, S.V.A., Clarke, E.M.: Probverus: Probabilistic symbolic model checking. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 96–110. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C.: Probabilistic invariants for probabilistic machines. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 240–259. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)Google Scholar
  9. 9.
    Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. In: Proc. of QAPL 2004 (March 2004)Google Scholar
  10. 10.
    Jeannet, B., D’Argenio, P., Larsen, K.: Rapture: A tool for verifying Markov Decision Processes. In: Cerna, I. (ed.) Tools Day 2002, Brno, Czech Republic, Technical Report. Faculty of Informatics, Masaryk University Brno (2002)Google Scholar
  11. 11.
    Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)Google Scholar
  13. 13.
    McIver, A., Morgan, C.: Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL. Theoretical Computer Science 293(3), 507–534 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Heidelberg (2004)Google Scholar
  15. 15.
    McIver, A., Morgan, C., Hoang, T.S.: Probabilistic termination in B. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 216–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 16.
    McIver, A.K.: Quantitative program logic and expected time bounds in probabilistic distributed algorithms. Theoretical Computer Science 282, 191–219 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Morgan, C.: Probabilistic temporal logic: qTL. Lectures on Probabilistic Formal Methods for the 2004 RSISE Logic Summer School, Slides available at
  18. 18.
    Morgan, C., McIver, A.: An expectation-transformer model for probabilistic temporal logic. Logic Journal of the IGPL 7(6), 779–804 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Morgan, C., McIver, A.: pGCL: Formal reasoning for random algorithms. South African Computer Journal 22, 14–27 (1999)Google Scholar
  20. 20.
    Morgan, C.C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  21. 21.
    Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)CrossRefGoogle Scholar
  22. 22.
    Norman, G.: Analysing randomized distributed algorithms. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 384–418. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  23. 23.
    Probabilistic Symbolic Model Checker,
  24. 24.

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Orieta Celiku
    • 1
  1. 1.Åbo Akademi University and Turku Centre for Computer ScienceTurkuFinland

Personalised recommendations