Reactive Synthesis Without Regret

Guillermo A. Pérez
Friday, 27 February, 2015 - 16:00
NO Solvay (5th floor)

Two-player, zero-sum games of infinite duration and their quantitative generalizations are often used in verification to model the interaction between a controller (Eve) and an antagonistic environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can win against any strategy of Adam. In this work we are interested in strategies of Eve that minimize her regret as defined by Halpern and Pass. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies.