文章基本信息

标题：Playing Safe
本地全文：下载
作者：Thomas Colcombet ; Nathanael Fijalkow ; Florian Horn 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2014
卷号：29
页码：379-390
DOI：10.4230/LIPIcs.FSTTCS.2014.379
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.
关键词：Game Theory; Synthesis; Safety Specifications; Program Verification