Controller synthesis is investigated through a game theoretic view. In the context of games, synthesis is the extraction of a winning strategy.
We investigate multi-weighted games, and various strategy types. We hierarchically order these strategy types by expressiveness.
We also present a weighted computation tree logic, for which we provide an undecidability result, and a decidable sub-logic, limited to reachability with upper bounds.
Further more we provide complexity results for the synthesis problem with the reachability sub-logic. We present two methods for synthesis of strategies in 1-weighted games:
We extend the attractor set method with weights giving a global algorithm with polynomial time complexity. And we also show how a strategy can be extracted using
prefixed-point assignment of a symbolic dependency graph.