Abstract
This work presents a complete formalization of Alternating-time Temporal Logic (ATL) and its semantic model, Concurrent Game Structures (CGS), in the Calculus of (Co)Inductive Constructions, using the logical framework Coq. Unlike standard ATL semantics, temporal operators are formalized in terms of inductive and coinductive types, employing a fixpoint characterization of these operators. The formalization is used to model a concurrent system with an unbounded number of players and states, and to verify some properties expressed as ATL formulas. Unlike automatic techniques, our formal model has no restrictions in the size of the CGS, and arbitrary state predicates can be used as atomic propositions of ATL.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 23–60. Springer, Heidelberg (1998)
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)
Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: Mocha: Modularity in Model Checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
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 (2004)
Chadha, R., Kremer, S., Scedrov, A.: Formal analysis of multiparty contract signing. Journal of Automated Reasoning 36(1-2), 39–83 (2006)
Coquand, T., Huet, G.: The Calculus of Constructions. In: Information and Computation, vol. 76, pp. 95–120. Academic Press (February/March 1988)
Coupet-Grimal, S.: LTL in Coq. Contributions to the Coq system, Laboratoire d’Informatique Fondamentale de Marseille (2002), http://coq.inria.fr/contribs/LTL.tar.gz
Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 995–1072. Elsevier (1995)
Giménez, E.: A Calculus of Infinite Constructions and its application to the verification of communicating systems. PhD thesis, Ecole Normale Supérieure de Lyon (1996)
Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science 353(1), 93–117 (2006)
Kremer, S., Raskin, J.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security 11(3), 399–429 (2003)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Luna, C.: Computation tree logic for reactive systems and timed computation tree logic for real time systems. Contributions to the Coq system, Universidad de la República, Uruguay (2000)
Merz, S.: An encoding of TLA in Isabelle. Technical report, Institut für Informatic, Universität München, Germany (1999)
Paulin-Mohring, C.: Inductive Definitions in the System Coq - rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE Computer Society, Washington, DC (1977)
Pnueli, A., Arons, T.: tlpvs: A pvs-Based ltl Verification System. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 598–625. Springer, Heidelberg (2004)
Schneider, K., Hoffmann, D.W.: A HOL Conversion for Translating Linear Time Temporal Logic to ω-Automata. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 255–272. Springer, Heidelberg (1999)
The Coq development team. The Coq proof assistant reference manual, version 8.2. LogiCal Project, Distributed electronically (2010), http://coq.inria.fr
The Coq development team. The Coq Standard Library. LogiCal Project (2010), http://coq.inria.fr/stdlib/
van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics. Elsevier and MIT Press (1990)
Zanarini, D.: Formalización de lógica temporal alternante en el cálculo de construcciones coinductivas. Master’s thesis, FCEIA, Universidad Nacional de Rosario, Argentina (2008), http://www.fceia.unr.edu.ar/~dante
Zanarini, D.: Formalization of alternating time temporal logic in Coq (2010), http://www.fceia.unr.edu.ar/~dante
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zanarini, D., Luna, C., Sierra, L. (2012). Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions. In: Gheyi, R., Naumann, D. (eds) Formal Methods: Foundations and Applications. SBMF 2012. Lecture Notes in Computer Science, vol 7498. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33296-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-33296-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33295-1
Online ISBN: 978-3-642-33296-8
eBook Packages: Computer ScienceComputer Science (R0)