--- res: bibo_abstract: - 'A major hurdle in the algorithmic verification and control of systems is the need to find suitable abstract models, which omit enough details to overcome the state-explosion problem, but retain enough details to exhibit satisfaction or controllability with respect to the specification. The paradigm of counterexample-guided abstraction refinement suggests a fully automatic way of finding suitable abstract models: one starts with a coarse abstraction, attempts to verify or control the abstract model, and if this attempt fails and the abstract counterexample does not correspond to a concrete counterexample, then one uses the spurious counterexample to guide the refinement of the abstract model. We present a counterexample-guided refinement algorithm for solving ω-regular control objectives. The main difficulty is that in control, unlike in verification, counterexamples are strategies in a game between system and controller. In the case that the controller has no choices, our scheme subsumes known counterexample-guided refinement algorithms for the verification of ω-regular specifications. Our algorithm is useful in all situations where ω-regular games need to be solved, such as supervisory control, sequential and program synthesis, and modular verification. The algorithm is fully symbolic, and therefore applicable also to infinite-state systems.@eng' bibo_authorlist: - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Ranjit foaf_name: Jhala, Ranjit foaf_surname: Jhala - foaf_Person: foaf_givenName: Ritankar foaf_name: Majumdar, Ritankar foaf_surname: Majumdar bibo_doi: 10.1007/3-540-45061-0_69 bibo_volume: 2719 dct_date: 2003^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/9783540404934 dct_language: eng dct_publisher: Springer@ dct_title: Counterexample-guided control@ ...