Skip to main content
SpringerLink
Log in
Book cover

Annual Asian Computing Science Conference

ASIAN 2006: Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues pp 316–330Cite as

Formalization of CTL* in Calculus of Inductive Constructions

  • Conference paper

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

Abstract

A modular formalization of the branching time temporal logic CTL* is presented. Our formalization subsumes prior formalizations of propositional linear temporal logic (PTL) and computation tree logic (CTL). Moreover, the modularity allows to instantiate our formalization for different formal security models. Validity of axioms and soundness of inference rules in axiomatizations of PTL, UB, CTL, and CTL* are discussed as well.

The work is partly supported by NSC grands 95-3114-P-001-002-Y02, 95-2221-E-001-024-MY3, and the project SISARL of Academia Sinica.

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. Bauer, G.: Some properties of CTL. Technische Universität München, Isabelle/Isar document (2001)

    Google Scholar 

  2. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2004)

    Google Scholar 

  3. Coupet-Grimal, S.: An axiomatization of linear temporal logic in the calculus of inductive constructions. Logic and Computation 13(6), 801–813 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  4. Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier Science Publishers (1990)

    Google Scholar 

  5. Emerson, E., Halpern, J.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30, 1–24 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  6. Kröger, F.: Temporal Logic of Programs. Springer, Heidelberg (1987)

    Book  MATH  Google Scholar 

  7. Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)

    Article  Google Scholar 

  8. Manolios, P.: Mu-calculus model-checking. In: Computer-Aided Reasoning: ACL2 Case Studies, pp. 93–111. Kluwer Academic Publishers, Dordrecht (2000)

    Chapter  Google Scholar 

  9. Merz, S.: Isabelle/TLA. Technische Universität München, Isabelle/Isar document (1998)

    Google Scholar 

  10. Miculan, M.: On the formalization of the modal μ-calculus in the calculus of inductive constructions. Information and Computation 164(1), 199–231 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  11. Müller, O., Nipkow, T.: Combining model checking and deduction for I/O-automata. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 1–16. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  12. Müller, O.: I/O automata and beyond - temporal logic and abstraction in Isabelle. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol. 1479, pp. 331–348. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Müller, O.: A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, Technische Universität München (1998)

    Google Scholar 

  14. Müller, O., Nipkow, T.: Traces of I/O automata in Isabelle/HOLCF. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 580–595. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  15. Reynolds, M.: An axiomatization of full computation tree logic. Journal of Symbolic Logic 66(3), 1011–1057 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  16. Sprenger, C.: A verified model checker for the modal μ-calculus in Coq. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 167–183. Springer, Heidelberg (1998)

    Google Scholar 

  17. Tsai, M.H., Wang, B.Y.: Modular formalization of reactive modules and CTL* in Coq. submitted for publication (2006)

    Google Scholar 

  18. Yu, S., Luo, Z.: Implementing a model checker for LEGO. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 442–458. Springer, Heidelberg (1997)

    Google Scholar 

  19. Zhang, X., Parisi-Presicce, F., Sandhu, R.: Formal model and policy specification of usage control. ACM Transactions on Information and System Security 8(4), 351–387 (2005)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Information Science, Academia Sinica, Taiwan

    Ming-Hsien Tsai & Bow-Yaw Wang

  2. Department of Information Management, National Taiwan University, Taiwan

    Ming-Hsien Tsai

Authors
  1. Ming-Hsien Tsai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bow-Yaw Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mitsu Okada Ichiro Satoh

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tsai, MH., Wang, BY. (2007). Formalization of CTL* in Calculus of Inductive Constructions. In: Okada, M., Satoh, I. (eds) Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues. ASIAN 2006. Lecture Notes in Computer Science, vol 4435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77505-8_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-77505-8_25

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-77505-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation