Skip to main content

Til the Well Runs Dry: Modelling and Synthesis of Resource-Dependent Systems

Petr Novotny

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.

Speaker bio

Petr is now finishing his Ph.D. study at Masaryk University, Czech Republic, where he works under the guidance of Prof. Antonín Kučera. His research interests include verification of infinite-state and stochastic systems and algorithmic analysis of graph games. During his postgraduate research he co-authored, among others, papers on stochastic Petri nets, one-counter Markov decision processes, and various modifications of energy games. Petr holds a master's degree in mathematics and undergraduate degrees in mathematics and computer science.

Share this: