Citation
Tom Henzinger, Ranjit Jhala, Rupak Majumdar. "Counterexample-Guided Control". Proc. 30th Int. Colloquium on Automata, Languages, and Programming (ICALP), volume 2719 of LNCS, 886-902, 2003.

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 omega-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 omega-regular specifications. Our algorithm is useful in all situations where omega-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.

Electronic downloads

• http://www-cad.eecs.berkeley.edu/~tah/Publications/counterexample-guided_control.ps
• counterexample-guided_control.pdf · download/application · 299 kbytes

• HTML

  Tom Henzinger, Ranjit Jhala, Rupak Majumdar. <a
  href="http://chess.eecs.berkeley.edu/pubs/737.html"
  >Counterexample-Guided Control</a>, Proc. 30th Int.
  Colloquium on Automata, Languages, and Programming (ICALP),
  volume 2719 of LNCS, 886-902, 2003.

• Plain text

  Tom Henzinger, Ranjit Jhala, Rupak Majumdar.
  "Counterexample-Guided Control". Proc. 30th Int.
  Colloquium on Automata, Languages, and Programming (ICALP),
  volume 2719 of LNCS, 886-902, 2003.

• BibTeX

  @inproceedings{HenzingerJhalaMajumdar03_CounterexampleGuidedControl,
      author = {Tom Henzinger and Ranjit Jhala and Rupak Majumdar},
      title = {Counterexample-Guided Control},
      booktitle = {Proc. 30th Int. Colloquium on Automata, Languages,
                and Programming (ICALP), volume 2719 of LNCS},
      pages = {886-902},
      year = {2003},
      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 omega-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 omega-regular
                specifications. Our algorithm is useful in all
                situations where omega-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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/737.html}
  }
  

Posted by Christopher Brooks on 4 Nov 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.