---
_id: '4482'
abstract:
- lang: eng
  text: "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.\r\nWe
    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."
acknowledgement: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Freddy
  full_name: Mang, Freddy
  last_name: Mang
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  ama: 'Henzinger TA, Majumdar R, Mang F, Raskin J. Abstract interpretation of game
    properties. In: <i>Proceedings of the 7th International Symposium on Static Analysis</i>.
    Vol 1824. Springer; 2000:220-239. doi:<a href="https://doi.org/10.1007/978-3-540-45099-3_12">10.1007/978-3-540-45099-3_12</a>'
  apa: 'Henzinger, T. A., Majumdar, R., Mang, F., &#38; Raskin, J. (2000). Abstract
    interpretation of game properties. In <i>Proceedings of the 7th International
    Symposium on Static Analysis</i> (Vol. 1824, pp. 220–239). Santa Barbara, CA,
    USA: Springer. <a href="https://doi.org/10.1007/978-3-540-45099-3_12">https://doi.org/10.1007/978-3-540-45099-3_12</a>'
  chicago: Henzinger, Thomas A, Ritankar Majumdar, Freddy Mang, and Jean Raskin. “Abstract
    Interpretation of Game Properties.” In <i>Proceedings of the 7th International
    Symposium on Static Analysis</i>, 1824:220–39. Springer, 2000. <a href="https://doi.org/10.1007/978-3-540-45099-3_12">https://doi.org/10.1007/978-3-540-45099-3_12</a>.
  ieee: T. A. Henzinger, R. Majumdar, F. Mang, and J. Raskin, “Abstract interpretation
    of game properties,” in <i>Proceedings of the 7th International Symposium on Static
    Analysis</i>, Santa Barbara, CA, USA, 2000, vol. 1824, pp. 220–239.
  ista: 'Henzinger TA, Majumdar R, Mang F, Raskin J. 2000. Abstract interpretation
    of game properties. Proceedings of the 7th International Symposium on Static Analysis.
    SAS: Static Analysis Symposium, LNCS, vol. 1824, 220–239.'
  mla: Henzinger, Thomas A., et al. “Abstract Interpretation of Game Properties.”
    <i>Proceedings of the 7th International Symposium on Static Analysis</i>, vol.
    1824, Springer, 2000, pp. 220–39, doi:<a href="https://doi.org/10.1007/978-3-540-45099-3_12">10.1007/978-3-540-45099-3_12</a>.
  short: T.A. Henzinger, R. Majumdar, F. Mang, J. Raskin, in:, Proceedings of the
    7th International Symposium on Static Analysis, Springer, 2000, pp. 220–239.
conference:
  end_date: 2000-07-06
  location: Santa Barbara, CA, USA
  name: 'SAS: Static Analysis Symposium'
  start_date: 2000-06-29
date_created: 2018-12-11T12:09:04Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:49:56Z
day: '01'
doi: 10.1007/978-3-540-45099-3_12
extern: '1'
intvolume: '      1824'
language:
- iso: eng
month: '01'
oa_version: None
page: 220 - 239
publication: Proceedings of the 7th International Symposium on Static Analysis
publication_identifier:
  isbn:
  - '9783540676683'
publication_status: published
publisher: Springer
publist_id: '248'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstract interpretation of game properties
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1824
year: '2000'
...