Cost vs. time in stochastic games and Markov automata
Hassan Hatefi, Ralf Wimmer, Bettina Braitling, Luis María Ferrer Fioriti, Bernd Becker, Holger Hermanns · Formal Aspects of Computing · 2017
Abstract Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies.