Graph games and reactive synthesis Book Section


Author(s): Bloem, Roderick; Chatterjee, Krishnendu; Jobstmann, Barbara
Editor(s): Henzinger, Thomas A
Article/Chapter Title: Graph games and reactive synthesis
Affiliation IST Austria
Abstract: 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.
Book Title: Handbook of Modeling Checking
ISBN: 978-331910575-8
Publisher: Springer  
Date Published: 2018-05-19
Start Page: 921
End Page: 962
DOI: 10.1007/978-3-319-10575-8_27
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work