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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bauer, G.: Some properties of CTL. Technische Universität München, Isabelle/Isar document (2001)
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)
Coupet-Grimal, S.: An axiomatization of linear temporal logic in the calculus of inductive constructions. Logic and Computation 13(6), 801–813 (2003)
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)
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)
Kröger, F.: Temporal Logic of Programs. Springer, Heidelberg (1987)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Manolios, P.: Mu-calculus model-checking. In: Computer-Aided Reasoning: ACL2 Case Studies, pp. 93–111. Kluwer Academic Publishers, Dordrecht (2000)
Merz, S.: Isabelle/TLA. Technische Universität München, Isabelle/Isar document (1998)
Miculan, M.: On the formalization of the modal μ-calculus in the calculus of inductive constructions. Information and Computation 164(1), 199–231 (2001)
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)
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)
Müller, O.: A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, Technische Universität München (1998)
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)
Reynolds, M.: An axiomatization of full computation tree logic. Journal of Symbolic Logic 66(3), 1011–1057 (2001)
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)
Tsai, M.H., Wang, B.Y.: Modular formalization of reactive modules and CTL* in Coq. submitted for publication (2006)
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)
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)
Author information
Authors and Affiliations
Editor information
Rights 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)