Publication
Title
Reactive synthesis without regret
Author
Abstract
Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (1) unrestricted, (2) limited to positional strategies, or (3) limited to word strategies, and show that the two last cases have natural modelling applications. These results apply for quantitative games defined with the classical payoff functions , , , , and mean-payoff. We also show that our notion of regret minimization in which Adam is limited to word strategies generalizes the notion of good for games introduced by Henzinger and Piterman, and is related to the notion of determinization by pruning due to Aminof, Kupferman and Lampert.
Language
English
Source (journal)
Acta informatica. - Berlin
Source (book)
26th International Conference on Concurrency Theory (CONCUR), SEP 01-04, 2015, Univ Complutense Madrid, Fac Matematicas, Univ Complutense Madrid, Fac Matematicas, Madrid, SPAIN
Publication
New york : Springer , 2017
ISSN
0001-5903
Volume/pages
54 :1 (2017) , p. 3-39
ISI
000394152600002
Full text (Publisher's DOI)
Full text (publisher's version - intranet only)
UAntwerpen
Publication type
Subject
External links
Web of Science
Record
Identification
Creation 16.11.2018
Last edited 23.09.2021