Efficient controller synthesis for consumption games with multiple resource types Conference Paper


Author(s): Brázdil, Brázdil; Chatterjee, Krishnendu; Kučera, Antonín; Novotný, Petr
Title: Efficient controller synthesis for consumption games with multiple resource types
Title Series: LNCS
Affiliation IST Austria
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 ω. The ω updates model the reloading of a given resource. Each vertex belongs either to player □ or player ◇, where the aim of player □ 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) and bounded resource updates.
Keywords: Controller synthesis; Polynomial-time; Fixed numbers; Algorithmic problems; Finite-state; Interactive system; Multiple resources
Conference Title: CAV: Computer Aided Verification
Volume: 7358 LNCS
Conference Dates: July 7-13, 2012
Conference Location: Berkeley, CA, USA
Publisher: Springer  
Location: Berlin, Germany
Date Published: 2012-06-12
Start Page: 23
End Page: 38
URL:
DOI: 10.1007/978-3-642-31424-7_8
Notes: Tomas Brazdil, Antonin Kucera, and Petr Novotny are supported by the Czech Science Foundation, grant No. P202/10/1469. Krishnendu Chatterjee is supported by the FWF (Austrian Science Fund) NFN Grant No S11407-N23 (RiSE) and ERC Start grant (279307: Graph Games).
Open access: yes (repository)
IST Austria Authors
Related IST Austria Work