---
res:
  bibo_abstract:
  - '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.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Luca
      foaf_name: De Alfaro, Luca
      foaf_surname: De Alfaro
  - 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: Ritankar
      foaf_name: Majumdar, Ritankar
      foaf_surname: Majumdar
  bibo_doi: 10.1109/LICS.2001.932504
  dct_date: 2001^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/076951281X
  dct_language: eng
  dct_publisher: IEEE@
  dct_title: 'From verification to control: dynamic programs for omega-regular objectives@'
...