Abstract
Alternating temporal logic (atl*) was introduced to prove properties of multi-agent systems in which the agents have different objectives and may collaborate to achieve them. Examples include (distributed) controlled systems, security protocols, and contract-signing protocols. Proving atl* properties over finite-state systems was shown decidable by Alur et al., and a model checker for the sublanguage atl implemented in mocha.
In this paper we present a sound and complete proof system for proving alt* properties over infinite-state systems. The proof system reduces proofs of alt* properties over systems to first-order verification conditions in the underlying assertion language. The verification conditions make use of predicate transformers that depend on the system structure, so that proofs over systems with a simpler structure, e.g., turn-based systems, directly result in simpler verification conditions. We illustrate the use of the proof system on a small example.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 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. 516–520. Springer, Heidelberg (1998)
Kremer, S., Raskin, J.F.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security 11(3), 399–429 (2003)
Kremer, S., Raskin, J.F.: Game analysis of abuse-free contract signing. In: Computer Security Foundations Workshop (CSFW). IEEE Computer Society, Los Alamitos (2002)
Chadha, R., Kremer, S., Scedrov, A.: Formal analysis of multi-party contract signing. Journal of Automated Reasoning (to appear, 2006)
Pauly, M., Wooldridge, M.: Logic for mechanism design—A manifesto. In: Proceedings of the 2003 Workshop on Game Theory and Decision Theory in Agent-Based Systems (GTDT 2003), Melbourne, Australia (2003)
Lamport, L.: Specifying Systems. Addison-Wesley, Reading (2002)
Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science 353(1–3), 93–117 (2006)
Manna, Z., Pnueli, A.: Completing the temporal picture. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 534–558. Springer, Heidelberg (1989)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)
Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theoretical Computer Science 331 (2005) 397–428
Vardi, M.Y.: Verification of concurrent programs: The automata-theoretic framework. Journal of Pure and Applied Logic 51(1–2), 79–98 (1991)
Fix, L., Grumberg, O.: Verification of temporal properties. J. Logic Computat. 6(3), 343–361 (1996)
Slanina, M., Sipma, H.B., Manna, Z.: Proving ATL* properties of infinite-state systems. Technical Report REACT-TR-2006-02, Stanford University, Computer Science Department, REACT Group (2006), avaliable at: http://react.stanford.edu/TR/
Slanina, M.: Control rules for reactive system games. In: Fischer, B., Smith, D.R. (eds.) Logic-Based Program Synthesis: State of the Art and Future Trends. AAAI Spring Symposium. The American Association for Artificial Intelligenc, pp. 95–104. AAAI Press, Menlo Park (2002); available from AAAI as Technical Report SS-02-05
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 135–183 (1998)
Henzinger, T.A., Majumdar, R., Mang, F.Y.C., Raskin, J.-F.: Abstract interpretation of game properties. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 220–240. Springer, Heidelberg (2000)
Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 726–765. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Slanina, M., Sipma, H.B., Manna, Z. (2006). Proving ATL* Properties of Infinite-State Systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_17
Download citation
DOI: https://doi.org/10.1007/11921240_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48815-6
Online ISBN: 978-3-540-48816-3
eBook Packages: Computer ScienceComputer Science (R0)