Efficient Controller Synthesis for Consumption Games with Multiple Resource Types

TL;DR

This paper introduces consumption games, a model for systems with multiple resources that are consumed or reloaded, and shows that certain algorithmic problems are polynomial-time solvable when the number of resource types is fixed.

Contribution

The paper formalizes consumption games with multiple resource types and proves polynomial-time solvability of key problems for fixed resource dimensions.

Findings

Problems are computationally hard in general

Polynomial-time solutions exist for fixed resource types

Model captures resource reloading and consumption dynamics

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).