## From Verification to Control:
Dynamic Programs for Omega-regular Objectives

*Luca de Alfaro,
Thomas A. Henzinger,
and Rupak Majumdar*

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 mu-calculus. Yet few connections have been made between
different interpretations of fixpoint algorithms. We study the question of
when a particular fixpoint iteration scheme *f* for verifying an
omega-regular property *L* on a Kripke structure can be used also for
solving a two-player game on a game graph with winning objective *L*.
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 *f* solves the game with
objective *L* if and only if both (1) under an existential
interpretation on Kripke structures, *f* is equivalent to *EL*, and
(2) under a universal interpretation on Kripke structures, *f* is
equivalent to *AL*. In other words, *f* 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 omega-regular properties to the
mu-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
omega-regular objective.

*Proceedings of the
16th Annual Symposium on Logic in Computer Science*
(LICS), IEEE Computer Society Press, 2001, pp. 279-290.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2001 IEEE.