[{"month":"06","title":"Handbook of Model Checking","publication_status":"published","oa_version":"None","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2018-12-11T12:02:32Z","author":[{"last_name":"Clarke","first_name":"Edmund M.","full_name":"Clarke, Edmund M."},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"},{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"}],"_id":"3300","scopus_import":"1","publisher":"Springer Nature","language":[{"iso":"eng"}],"page":"XLVIII, 1212","quality_controlled":"1","retracted":"1","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."}],"publist_id":"3340","doi":"10.1007/978-3-319-10575-8","edition":"1","publication_identifier":{"eisbn":["978-3-319-10575-8"],"isbn":["978-3-319-10574-1"]},"day":"08","date_published":"2018-06-08T00:00:00Z","type":"book","date_updated":"2025-07-24T09:25:31Z","citation":{"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.","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>","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>","ista":"Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking 1st ed., Cham: Springer Nature, XLVIII, 1212p.","short":"E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st ed., Springer Nature, Cham, 2018.","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>."},"year":"2018","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","place":"Cham"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_updated":"2021-01-12T08:05:10Z","year":"2018","citation":{"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.","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.","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>.","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>","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>"},"date_published":"2018-05-19T00:00:00Z","type":"book_chapter","doi":"10.1007/978-3-319-10575-8_27","day":"19","publication_identifier":{"isbn":["978-3-319-10574-1"]},"edition":"1","abstract":[{"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.","lang":"eng"}],"publist_id":"7995","page":"921 - 962","quality_controlled":"1","language":[{"iso":"eng"}],"publisher":"Springer","editor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Clarke, Edmund M.","last_name":"Clarke","first_name":"Edmund M."},{"last_name":"Veith","first_name":"Helmut","full_name":"Veith, Helmut"},{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"}],"_id":"59","publication":"Handbook of Model Checking","scopus_import":1,"author":[{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"}],"oa_version":"None","publication_status":"published","date_created":"2018-12-11T11:44:24Z","department":[{"_id":"KrCh"}],"title":"Graph games and reactive synthesis","month":"05"}]