Graph games and reactive synthesis
Bloem R, Chatterjee K, Jobstmann B. 2018.Graph games and reactive synthesis. In: Handbook of Model Checking. , 921–962.
Download
No fulltext has been uploaded. References only!
Book Chapter
| Published
| English
Scopus indexed
Author
Bloem, Roderick;
Chatterjee, KrishnenduISTA 
;
Jobstmann, Barbara
;
Jobstmann, BarbaraBook Editor
Henzinger, Thomas AISTA ;
Clarke, Edmund M.;
Veith, Helmut;
Bloem, Roderick
;
Clarke, Edmund M.;
Veith, Helmut;
Bloem, RoderickDepartment
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.
Publishing Year
Date Published
2018-05-19
Book Title
Handbook of Model Checking
Publisher
Springer
Page
921 - 962
ISBN
IST-REx-ID
Cite this
Bloem R, Chatterjee K, Jobstmann B. Graph games and reactive synthesis. In: Henzinger TA, Clarke EM, Veith H, Bloem R, eds. Handbook of Model Checking. 1st ed. Springer; 2018:921-962. doi:10.1007/978-3-319-10575-8_27
Bloem, R., Chatterjee, K., & Jobstmann, B. (2018). Graph games and reactive synthesis. In T. A. Henzinger, E. M. Clarke, H. Veith, & R. Bloem (Eds.), Handbook of Model Checking (1st ed., pp. 921–962). Springer. https://doi.org/10.1007/978-3-319-10575-8_27
Bloem, Roderick, Krishnendu Chatterjee, and Barbara Jobstmann. “Graph Games and Reactive Synthesis.” In Handbook of Model Checking, edited by Thomas A Henzinger, Edmund M. Clarke, Helmut Veith, and Roderick Bloem, 1st ed., 921–62. Springer, 2018. https://doi.org/10.1007/978-3-319-10575-8_27.
R. Bloem, K. Chatterjee, and B. Jobstmann, “Graph games and reactive synthesis,” in Handbook of Model Checking, 1st ed., T. A. Henzinger, E. M. Clarke, H. Veith, and R. Bloem, Eds. Springer, 2018, pp. 921–962.
Bloem R, Chatterjee K, Jobstmann B. 2018.Graph games and reactive synthesis. In: Handbook of Model Checking. , 921–962.
Bloem, Roderick, et al. “Graph Games and Reactive Synthesis.” Handbook of Model Checking, edited by Thomas A Henzinger et al., 1st ed., Springer, 2018, pp. 921–62, doi:10.1007/978-3-319-10575-8_27.
Google Scholar
ISBN Search