Henzinger, Thomas AISTA ; Majumdar, Ritankar; Mang, Freddy; Raskin, Jean
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.
7th International Symposium on Static Analysis
220 - 239
SAS: Static Analysis Symposium
Santa Barbara, CA, United States of America
2000-06-29 – 2000-07-06
Henzinger TA, Majumdar R, Mang F, Raskin J. Abstract interpretation of game properties. In: 7th International Symposium on Static Analysis. Vol 1824. Springer; 2000:220-239. doi:10.1007/978-3-540-45099-3_12
Henzinger, T. A., Majumdar, R., Mang, F., & Raskin, J. (2000). Abstract interpretation of game properties. In 7th International Symposium on Static Analysis (Vol. 1824, pp. 220–239). Santa Barbara, CA, United States of America: Springer. https://doi.org/10.1007/978-3-540-45099-3_12
Henzinger, Thomas A, Ritankar Majumdar, Freddy Mang, and Jean Raskin. “Abstract Interpretation of Game Properties.” In 7th International Symposium on Static Analysis, 1824:220–39. Springer, 2000. https://doi.org/10.1007/978-3-540-45099-3_12.
T. A. Henzinger, R. Majumdar, F. Mang, and J. Raskin, “Abstract interpretation of game properties,” in 7th International Symposium on Static Analysis, Santa Barbara, CA, United States of America, 2000, vol. 1824, pp. 220–239.
Henzinger TA, Majumdar R, Mang F, Raskin J. 2000. Abstract interpretation of game properties. 7th International Symposium on Static Analysis. SAS: Static Analysis Symposium, LNCS, vol. 1824, 220–239.
Henzinger, Thomas A., et al. “Abstract Interpretation of Game Properties.” 7th International Symposium on Static Analysis, vol. 1824, Springer, 2000, pp. 220–39, doi:10.1007/978-3-540-45099-3_12.