---
_id: '4636'
abstract:
- lang: eng
  text: 'Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for
    solving many problems on state spaces, including model checking on Kripke structures
    (“verification”), computing shortest paths on weighted graphs (“optimization”),
    computing the value of games played on game graphs (“control”). For Kripke structures,
    a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections
    have been made between different interpretations of fixpoint algorithms. We study
    the question of when a particular fixpoint iteration scheme ϕ for verifying an
    ω-regular property Ψ on a Kripke structure can be used also for solving a two-player
    game on a game graph with winning objective Ψ. We provide a sufficient and necessary
    criterion for the answer to be affirmative in the form of an extremal-model theorem
    for games: under a game interpretation, the dynamic program ϕ solves the game
    with objective Ψ if and only if both (1) under an existential interpretation on
    Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation
    on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all
    two-player game graphs iff it is correct on all extremal game graphs, where one
    or the other player has no choice of moves. The theorem generalizes to quantitative
    interpretations, where it connects two-player games with costs to weighted graphs.
    While the standard translations from ω-regular properties to the µ-calculus violate
    (1) or (2), we give a translation that satisfies both conditions. Our construction,
    therefore, yields fixpoint iteration schemes that can be uniformly applied on
    Kripke structures, weighted graphs, game graphs, and game graphs with costs, in
    order to meet or optimize a given ω-regular objective.'
article_processing_charge: No
author:
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'De Alfaro L, Henzinger TA, Majumdar R. From verification to control: dynamic
    programs for omega-regular objectives. In: <i>Proceedings of the 16th Annual IEEE
    Symposium on Logic in Computer Science</i>. IEEE; 2001:279-290. doi:<a href="https://doi.org/10.1109/LICS.2001.932504">10.1109/LICS.2001.932504</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2001). From verification
    to control: dynamic programs for omega-regular objectives. In <i>Proceedings of
    the 16th Annual IEEE Symposium on Logic in Computer Science</i> (pp. 279–290).
    Boston, MA, USA: IEEE. <a href="https://doi.org/10.1109/LICS.2001.932504">https://doi.org/10.1109/LICS.2001.932504</a>'
  chicago: 'De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “From Verification
    to Control: Dynamic Programs for Omega-Regular Objectives.” In <i>Proceedings
    of the 16th Annual IEEE Symposium on Logic in Computer Science</i>, 279–90. IEEE,
    2001. <a href="https://doi.org/10.1109/LICS.2001.932504">https://doi.org/10.1109/LICS.2001.932504</a>.'
  ieee: 'L. De Alfaro, T. A. Henzinger, and R. Majumdar, “From verification to control:
    dynamic programs for omega-regular objectives,” in <i>Proceedings of the 16th
    Annual IEEE Symposium on Logic in Computer Science</i>, Boston, MA, USA, 2001,
    pp. 279–290.'
  ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2001. From verification to control:
    dynamic programs for omega-regular objectives. Proceedings of the 16th Annual
    IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science,
    279–290.'
  mla: 'De Alfaro, Luca, et al. “From Verification to Control: Dynamic Programs for
    Omega-Regular Objectives.” <i>Proceedings of the 16th Annual IEEE Symposium on
    Logic in Computer Science</i>, IEEE, 2001, pp. 279–90, doi:<a href="https://doi.org/10.1109/LICS.2001.932504">10.1109/LICS.2001.932504</a>.'
  short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 16th Annual
    IEEE Symposium on Logic in Computer Science, IEEE, 2001, pp. 279–290.
conference:
  end_date: 2001-06-19
  location: Boston, MA, USA
  name: 'LICS: Logic in Computer Science'
  start_date: 2001-06-16
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-07T00:00:00Z
date_updated: 2023-05-08T09:48:06Z
day: '07'
doi: 10.1109/LICS.2001.932504
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 279 - 290
publication: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
  isbn:
  - 076951281X
publication_status: published
publisher: IEEE
publist_id: '72'
quality_controlled: '1'
status: public
title: 'From verification to control: dynamic programs for omega-regular objectives'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...