@Misc{Z09a,
author = {Zimmermann, Martin},
title = {Time-optimal {W}inning {S}trategies in {I}nfinite {G}ames.},
howpublished = {Diplomarbeit, RWTH Aachen},
year = {2009},
abstract = {
Infinite Games are an important tool in the synthesis of finite-state
controllers for reactive systems. The interaction between the environment
and the system is modeled by a finite graph. The specification that has
to be satisfied by the controlled system is translated into a winning
condition on the infinite paths of the graph. Then, a winning strategy
is a controller that is correct with respect to the given specification.
Winning strategies are often finitely described by automata with output.
While classical optimization of synthesized controllers focuses on the
size of the automaton we consider a different quality measure. Many
winning conditions allow a natural definition of waiting times that
reflect periods of waiting in the original system. We investigate
time-optimal strategies for Request-Response Games, Poset Games - a
novel type of infinite games that extends Request-Response Games - and
games with winning conditions in Parametric Linear Temporal Logic. Here,
the temporal operators of classical Temporal Logics can be subscribed with
free variables that represent bounds on the satisfaction. Then, one is
interested in winning strategies with respect to optimal valuations of the
free variables. The optimization objective, maximization respectively
minimization of the variable values, depends on the formula.
For Request-Response Games and Poset Games, we prove the existence of
time-optimal finite-state winning strategies. For games with winning
conditions in Parametric Linear Temporal Logic, we prove that optimal
winning strategies are computable for solitary games.}
}