Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Theoretical Aspects of Computing

ICTAC 2005: Theoretical Aspects of Computing – ICTAC 2005 pp 439–453Cite as

Quantitative Temporal Logic Mechanized in HOL

  • Conference paper

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

Abstract

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.

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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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. Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  2. Celiku, O., McIver, A.: Cost-based analysis of probabilistic programs mechanised in HOL. Nordic Journal of Computing 11(2), 102–128 (2004)

    MATH  MathSciNet  Google Scholar 

  3. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  4. Erlangen-Twente Markov Chain Checker, http://www.informatik.uni-erlangen.de/etmcc/

  5. Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  8. Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)

    Google Scholar 

  9. Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. In: Proc. of QAPL 2004 (March 2004)

    Google Scholar 

  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. Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  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. McIver, A., Morgan, C.: Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL. Theoretical Computer Science 293(3), 507–534 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  14. McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Heidelberg (2004)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  16. McIver, A.K.: Quantitative program logic and expected time bounds in probabilistic distributed algorithms. Theoretical Computer Science 282, 191–219 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  17. Morgan, C.: Probabilistic temporal logic: qTL. Lectures on Probabilistic Formal Methods for the 2004 RSISE Logic Summer School, Slides available at http://www.cse.unsw.edu.au/~carrollm/canberra04/

  18. Morgan, C., McIver, A.: An expectation-transformer model for probabilistic temporal logic. Logic Journal of the IGPL 7(6), 779–804 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  19. Morgan, C., McIver, A.: pGCL: Formal reasoning for random algorithms. South African Computer Journal 22, 14–27 (1999)

    Google Scholar 

  20. Morgan, C.C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  21. Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  23. Probabilistic Symbolic Model Checker, http://www.cs.bham.ac.uk/dxp/prism/

  24. Ymer, http://www.cs.cmu.edu/~lorens/ymer.html

Download references

Author information

Authors and Affiliations

  1. Åbo Akademi University and Turku Centre for Computer Science, Lemminkäisenkatu 14 A, 20520, Turku, Finland

    Orieta Celiku

Authors
  1. Orieta Celiku
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. College of Technology, Vietnam National University, Hanoi, Vietnam

    Dang Van Hung

  2. Institute of Computer Science, LMU Munich, Munich, Germany

    Martin Wirsing

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Celiku, O. (2005). Quantitative Temporal Logic Mechanized in HOL. In: Van Hung, D., Wirsing, M. (eds) Theoretical Aspects of Computing – ICTAC 2005. ICTAC 2005. Lecture Notes in Computer Science, vol 3722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560647_29

Download citation

  • DOI: https://doi.org/10.1007/11560647_29

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29107-7

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation