Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
Abstract
We introduce consumption games, a model for discrete interactive system with multiple resources that are consumed or reloaded independently. More precisely, a consumption game is a finite-state graph where each transition is labeled by a vector of resource updates, where every update is a non-positive number or omega. The omega updates model the reloading of a given resource. Each vertex belongs either to player \Box or player \Diamond, where the aim of player \Box is to play so that the resources are never exhausted. We consider several natural algorithmic problems about consumption games, and show that although these problems are computationally hard in general, they are solvable in polynomial time for every fixed number of resource types (i.e., the dimension of the update vectors).
Keywords
Cite
@article{arxiv.1202.0796,
title = {Efficient Controller Synthesis for Consumption Games with Multiple Resource Types},
author = {Tomáš Brázdil and Krishnendu Chatterjee and Antonín Kučera and Petr Novotný},
journal= {arXiv preprint arXiv:1202.0796},
year = {2012}
}
Comments
Revised version, 38 pages. This is a full version of a paper accepted for publication in the proceedings of CAV 2012