Til the Well Runs Dry: Modelling and Synthesis of Resource-Dependent Systems
The recent proliferation of embedded systems sparked a lot of interest in the analysis and synthesis of resource-dependent systems, i.e. systems that need to consume resources of limited supply in order to operate correctly. A typical goal in this setting is to synthesize a system which performs some required task without running out of its resources. Turn-based games played on transition graphs of counter automata, also known as energy games, provide an abstract framework in which such a resource-constrained synthesis problem can be formulated. In this talk we present an alternative model of resource-dependent systems, so called consumption games. This formalism retains much of the expressive power of energy games (it differs only in the way which resource replenishment is modelled) while admitting more efficient algorithmic analysis. We present algorithms solving several natural problems for consumption games, including synthesis problems in which 'hard' resource constraints (such as 'never run out of a resource') are mixed with 'soft' constraints (such as 'optimize the long-run average consumption'). We also discuss several possible directions of future work.
The talk is (for the most part) based on papers presented at CAV'12 and CAV'14. Joint work with T Brázdil, K. Chatterjee, D. Klaška, and A Kucera.