---
_id: '3300'
abstract:
- lang: eng
  text: "This book first explores the origins of this idea, grounded in theoretical
    work on temporal logic and automata. The editors and authors are among the world's
    leading researchers in this domain, and they contributed 32 chapters representing
    a thorough view of the development and application of the technique. Topics covered
    include binary decision diagrams, symbolic model checking, satisfiability modulo
    theories, partial-order reduction, abstraction, interpolation, concurrency, security
    protocols, games, probabilistic model checking, and process algebra, and chapters
    on the transfer of theory to industrial practice, property specification languages
    for hardware, and verification of real-time systems and hybrid systems.\r\n\r\nThe
    book will be valuable for researchers and graduate students engaged with the development
    of formal methods and verification tools."
article_processing_charge: No
author:
- first_name: Edmund M.
  full_name: Clarke, Edmund M.
  last_name: Clarke
- 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: Helmut
  full_name: Veith, Helmut
  last_name: Veith
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
citation:
  ama: 'Clarke EM, Henzinger TA, Veith H, Bloem R. <i>Handbook of Model Checking</i>.
    1st ed. Cham: Springer Nature; 2018. doi:<a href="https://doi.org/10.1007/978-3-319-10575-8">10.1007/978-3-319-10575-8</a>'
  apa: 'Clarke, E. M., Henzinger, T. A., Veith, H., &#38; Bloem, R. (2018). <i>Handbook
    of Model Checking</i> (1st ed.). Cham: Springer Nature. <a href="https://doi.org/10.1007/978-3-319-10575-8">https://doi.org/10.1007/978-3-319-10575-8</a>'
  chicago: 'Clarke, Edmund M., Thomas A Henzinger, Helmut Veith, and Roderick Bloem.
    <i>Handbook of Model Checking</i>. 1st ed. Cham: Springer Nature, 2018. <a href="https://doi.org/10.1007/978-3-319-10575-8">https://doi.org/10.1007/978-3-319-10575-8</a>.'
  ieee: 'E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, <i>Handbook of Model
    Checking</i>, 1st ed. Cham: Springer Nature, 2018.'
  ista: 'Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking
    1st ed., Cham: Springer Nature, XLVIII, 1212p.'
  mla: Clarke, Edmund M., et al. <i>Handbook of Model Checking</i>. 1st ed., Springer
    Nature, 2018, doi:<a href="https://doi.org/10.1007/978-3-319-10575-8">10.1007/978-3-319-10575-8</a>.
  short: E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking,
    1st ed., Springer Nature, Cham, 2018.
date_created: 2018-12-11T12:02:32Z
date_published: 2018-06-08T00:00:00Z
date_updated: 2025-07-24T09:25:31Z
day: '08'
department:
- _id: ToHe
doi: 10.1007/978-3-319-10575-8
edition: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: XLVIII, 1212
place: Cham
publication_identifier:
  eisbn:
  - 978-3-319-10575-8
  isbn:
  - 978-3-319-10574-1
publication_status: published
publisher: Springer Nature
publist_id: '3340'
quality_controlled: '1'
retracted: '1'
scopus_import: '1'
status: public
title: Handbook of Model Checking
type: book
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2018'
...
---
_id: '59'
abstract:
- lang: eng
  text: Graph-based games are an important tool in computer science. They have applications
    in synthesis, verification, refinement, and far beyond. We review graphbased games
    with objectives on infinite plays. We give definitions and algorithms to solve
    the games and to give a winning strategy. The objectives we consider are mostly
    Boolean, but we also look at quantitative graph-based games and their objectives.
    Synthesis aims to turn temporal logic specifications into correct reactive systems.
    We explain the reduction of synthesis to graph-based games (or equivalently tree
    automata) using synthesis of LTL specifications as an example. We treat the classical
    approach that uses determinization of parity automata and more modern approaches.
author:
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
citation:
  ama: 'Bloem R, Chatterjee K, Jobstmann B. Graph games and reactive synthesis. In:
    Henzinger TA, Clarke EM, Veith H, Bloem R, eds. <i>Handbook of Model Checking</i>.
    1st ed. Springer; 2018:921-962. doi:<a href="https://doi.org/10.1007/978-3-319-10575-8_27">10.1007/978-3-319-10575-8_27</a>'
  apa: Bloem, R., Chatterjee, K., &#38; Jobstmann, B. (2018). Graph games and reactive
    synthesis. In T. A. Henzinger, E. M. Clarke, H. Veith, &#38; R. Bloem (Eds.),
    <i>Handbook of Model Checking</i> (1st ed., pp. 921–962). Springer. <a href="https://doi.org/10.1007/978-3-319-10575-8_27">https://doi.org/10.1007/978-3-319-10575-8_27</a>
  chicago: Bloem, Roderick, Krishnendu Chatterjee, and Barbara Jobstmann. “Graph Games
    and Reactive Synthesis.” In <i>Handbook of Model Checking</i>, edited by Thomas
    A Henzinger, Edmund M. Clarke, Helmut Veith, and Roderick Bloem, 1st ed., 921–62.
    Springer, 2018. <a href="https://doi.org/10.1007/978-3-319-10575-8_27">https://doi.org/10.1007/978-3-319-10575-8_27</a>.
  ieee: R. Bloem, K. Chatterjee, and B. Jobstmann, “Graph games and reactive synthesis,”
    in <i>Handbook of Model Checking</i>, 1st ed., T. A. Henzinger, E. M. Clarke,
    H. Veith, and R. Bloem, Eds. Springer, 2018, pp. 921–962.
  ista: 'Bloem R, Chatterjee K, Jobstmann B. 2018.Graph games and reactive synthesis.
    In: Handbook of Model Checking. , 921–962.'
  mla: Bloem, Roderick, et al. “Graph Games and Reactive Synthesis.” <i>Handbook of
    Model Checking</i>, edited by Thomas A Henzinger et al., 1st ed., Springer, 2018,
    pp. 921–62, doi:<a href="https://doi.org/10.1007/978-3-319-10575-8_27">10.1007/978-3-319-10575-8_27</a>.
  short: R. Bloem, K. Chatterjee, B. Jobstmann, in:, T.A. Henzinger, E.M. Clarke,
    H. Veith, R. Bloem (Eds.), Handbook of Model Checking, 1st ed., Springer, 2018,
    pp. 921–962.
date_created: 2018-12-11T11:44:24Z
date_published: 2018-05-19T00:00:00Z
date_updated: 2021-01-12T08:05:10Z
day: '19'
department:
- _id: KrCh
doi: 10.1007/978-3-319-10575-8_27
edition: '1'
editor:
- 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: Edmund M.
  full_name: Clarke, Edmund M.
  last_name: Clarke
- first_name: Helmut
  full_name: Veith, Helmut
  last_name: Veith
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
language:
- iso: eng
month: '05'
oa_version: None
page: 921 - 962
publication: Handbook of Model Checking
publication_identifier:
  isbn:
  - 978-3-319-10574-1
publication_status: published
publisher: Springer
publist_id: '7995'
quality_controlled: '1'
scopus_import: 1
status: public
title: Graph games and reactive synthesis
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2018'
...