Abstract
We apply the theory of abstract interpretation to the verification of game properties for reactive systems. Unlike properties expressed in standard temporal logics, game properties can distinguish adversarial from collaborative relationships between the processes of a concurrent program, or the components of a parallel system. We consider two-player concurrent games –say, component vs. environment– and specify properties of such games –say, the component has a winning strategy to obtain a resource, no matter how the environment behaves– in the alternating-time μ-calculus (Aμ ). A sound abstraction of such a game must at the same time restrict the behaviors of the component and increase the behaviors of the environment: if a less powerful component can win against a more powerful environment, then surely the original component can win against the original environment.
We formalize the concrete semantics of a concurrent game in terms of controllable and uncontrollable predecessor predicates, which suffice for model checking all Aμ properties by applying boolean operations and iteration. We then define the abstract semantics of a concurrent game in terms of abstractions for the controllable and uncontrollable predecessor predicates. This allows us to give general characterizations for the soundness and completeness of abstract games with respect to Aμ properties. We also present a simple programming language for multi-process programs, and show how approximations of the maximal abstraction (w.r.t. Aμ properties) can be obtained from the program text. We apply the theory to two practical verification examples, a communication protocol developed at the Berkeley Wireless Research Center, and a protocol converter. In the wireless protocol, both the use of a game property for specification and the use of abstraction for automatic verification were instrumental to uncover a subtle bug.
This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
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: Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pp. 100–109. IEEE Computer Society Press, Los Alamitos (1997)
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Berkeley Wireless Research Center, http://bwrc.eecs.berkeley.edu
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 395–407. Springer, Heidelberg (1995)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Proceedings of the 19th Annual Symposium on Principles of Programming Languages, pp. 343–354. ACM Press, New York (1992)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Fourth Annual Symposium on Principles of Programming Languages. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2/3), 103–179 (1992)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Automated Software Engineering 6(1), 69–95 (1999)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proceedings of the 27th Annual Symposium on Principles of Programming Languages, pp. 12–25. ACM Press, New York (2000)
Dams, D.R.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, The Netherlands (1996)
Dams, D.R., Gerth, R., Döhmen, G., Herrmann, R., Kelb, P., Pargmann, H.: Model checking using adaptive state and data abstraction. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 455–467. Springer, Heidelberg (1994)
Dams, D.R., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems 19(2), 253–291 (1997)
Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: Proceedings of the 39th Annual Symposium on Foundations of Computer Science, pp. 564–575. IEEE Computer Society Press, Los Alamitos (1998)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite state games. Technical report, University of California, Berkeley (2000)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Dill, D.L., Wong-Toi, H.: Verification of real-time systems by successive overand underapproximation. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 409–422. Springer, Heidelberg (1995)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier Science Publishers, Amsterdam (1990)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Complete abstract interpretations made constructive. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 366–377. Springer, Heidelberg (1998)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretation complete. Journal of the ACM (2000) (to appear)
Graf, S.: Verification of a distributed cache memory by using abstractions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 207–219. Springer, Heidelberg (1994)
Graf, S., Saïdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 11–44 (1995)
Long, D.E.: Model checking, abstraction, and compositional verification. PhD thesis, Carnegie Mellon University, Pittsburgh, PA (1993)
McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219–237. Springer, Heidelberg (1999)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete-event processes. SIAM Journal of Control and Optimization 25(1), 206–230 (1987)
Stevens, P.: Abstract interpretation of games. In: Proceedings of the 2nd International Workshop on Verification, Model Checking and Abstract Interpretation (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Majumdar, R., Mang, F., Raskin, JF. (2000). Abstract Interpretation of Game Properties. In: Palsberg, J. (eds) Static Analysis. SAS 2000. Lecture Notes in Computer Science, vol 1824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45099-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-45099-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67668-3
Online ISBN: 978-3-540-45099-3
eBook Packages: Springer Book Archive