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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ash RB, Doléans-Dade CA (1999) Probability & measure theory, 2nd edn. Academic Press, New York
Andova S, Hermanns H, Katoen JP (2003) Discrete-time rewards model-checked. In: Int’l conf. on formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science. vol 2791. Springer, Berlin, pp 88–104
Boudali H, Crouzen P, Stoelinga M (2010) A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Tran Depend Sec Comput 7(2): 128–143
Bruno JL, Downey PJ, Frederickson GN (1981) Sequencing tasks with exponential service times to minimize the expected flow time or makespan. J ACM 28(1): 100–113
Braitling B, María Ferrer Fioriti L, Hatefi H, Wimmer R, Becker B, Hermanns H (2014) MeGARA: menu-based game abstraction refinement for Markov automata. In: Bertrand N, Bertolussi L (eds) Int’l workshop on quantitative aspects of programming languages and systems (QAPL). In: Electronic proceedings in theoretical computer science, vol 154. Open Publishing Association, Grenoble, pp 48–63
Braitling B, María Ferrer FL, Hatefi H, Wimmer R, Hermanns H, Becker B (2015) Abstraction-based computation of reward measures for Markov automata. In: Int’l conf. on verification, model checking, and abstract interpretation (VMCAI). Lecture Notes in Computer Science, vol 8931. Springer, Berlin, pp 172–189
Brázdil T, Forejt V, Krcál J, Kretínský J, Kucera A (2013) Continuous-time stochastic games with time-bounded reachability. Inf Comput 224: 46–70
Baier C, Haverkort BR, Hermanns H, Katoen JP (2000) On the logical characterisation of performability properties. In: Int’l colloquium on automata, languages, and programming (ICALP). In: Lecture notes in computer science, vol 1853. Springer, Berlin, pp 780–792
Baier C, Haverkort BR, Hermanns H, Katoen JP (2008) Reachability in continuous-time Markov reward decision processes. In: Logic and automata: history and perspectives. Honor of Wolfgang Thomas. Texts in logic and games, vol 2. Amsterdam University Press, Amsterdam, pp 53–72
Butkova Y, Hatefi H, Hermanns H, Krcál J (2015) Optimal continuous time Markov decisions. In: Finkbeiner B, Pu G, Zhang L (eds) Int’l symp. on automated technology for verification and analysis (ATVA). Lecture notes in computer science, vol 9364. Springer, Shanghai, pp 166–182
Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press, Massachusetts
Buchholz P, Schulz I (2011) Numerical analysis of continuous time Markov decision processes over finite horizons. Comput Oper Res 38(3): 651–659
Cloth L, Katoen J-P, Khattri M, Pulungan R (2005) Model checking Markov reward models with impulse rewards. In: Int’l conf. on dependable systems and networks (DSN). IEEE Computer Society, New York, pp 722–731
Eisentraut C, Hermanns H, Katoen J-P, Zhang L (2013) A semantics for every GSPN. In: Proc. of petri nets. Lecture notes in computer science, vol 7927. Springer, Berlin, pp 90–109
Eisentraut C, Hermanns H, Zhang L (2010) On probabilistic automata in continuous time. In: Annual IEEE symp. on logic in computer science (LICS). IEEE Computer Society, New York, pp 342–351
Fu H (2014) Maximal cost-bounded reachability probability on continuous-time Markov decision processes. In: Int’l conf. on foundations of software science and computation structures (FoSSaCS). Lecture notes in computer science, vol 8412. Springer, Berlin, pp 73–87
Fu H (2014) Verifying probabilistic systems: new algorithms and complexity results. PhD thesis, RWTH Aachen University
Gburek D, Baier C, Klüppelholz S (2016) Composition of stochastic transition systems based on spans and couplings. In: 43rd international colloquium on automata, languages, and programming, ICALP 2016, July 11–15, 2016, Rome, Italy, pp 102:1–102:15
Guck D, Hatefi H, Hermanns H, Katoen J.-P. Timmer M (2013) Modelling, reduction and analysis of Markov automata. In: Int’l conf. on quantitative evaluation of systems (QEST). Lecture notes in computer science, vol 8054. Springer, Berlin, pp 55–71
Guck D, Hatefi H, Hermanns H, Katoen JP, Timmer M (2014) Analysis of timed and long-run objectives for Markov automata. Logical Methods Comput Sci 10(3)
Guck D, Han T, Katoen JP, Neuhäußer MR (2012) Quantitative timed analysis of interactive Markov chains. In: NASA formal methods symposium (NFM). Lecture notes in computer science, vol 7226. Springer, Berlin, pp 8–23
Guck D, Timmer M, Hatefi H, Ruijters E, Stoelinga M (2014) Modelling and analysis of Markov reward automata. In: Int’l symp. on automated technology for verification and analysis (ATVA). Lecture notes in computer science, vol 8837. Springer, Berlin, pp 168–184
Hatefi H, Braitling B, Wimmer R, María Ferrer Fioriti L, Hermanns H, Becker B (2015) Cost vs. time in stochastic games and Markov automata. In: Li X, Liu Z, Yi W (eds) int’l symp. on dependable software engineering: theory, tools and applications (SETTA). Lecture notes in computer science, vol 9409. Springer, Nanjing, pp 19–34
Hermanns H (2002) Interactive Markov chains: the quest for quantified quality. In: Lecture notes in computer science, vol 2428. Springer, Berlin
Hatefi H, Hermanns H (2012) Model checking algorithms for Markov automata. ECEASST 53
Johr S (2008) Model checking compositional Markov systems. PhD thesis, Saarland University, Saarbrücken
Miller BL (1968) Finite state continuous time Markov decision processes with a finite planning horizon. SIAM J Control 6(2): 266–280
Neuhäußer MR (2010) Model checking nondeterministic and randomly timed systems. PhD thesis, RWTH Aachen University and University of Twente
Neyman, A, Sorin, S (eds) (2003) Stochastic games and applications. Springer, Berlin
Neuhäußer MR, Zhang L (2010) Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Int’l conf. on quantitative evaluation of systems (QEST). IEEE Computer Society, New York, pp 209–218
Qiu Q, Qu Q, Pedram M (2001) Stochastic modeling of a power-managed system-construction and optimization. IEEE Trans CAD Integrat Circ Syst 20(10): 1200–1217
Simunic T, Benini L, Glynn P.W, De Micheli G (2000) Dynamic power management for portable systems. In: Annual int’l conf. on mobile computing and networking (MOBICOM), Boston, MA, USA, August, pp 11–19
Segala R (1995) A compositional trace-based semantics for probabilistic automata. In: Int’l conf. on concurrency theory (CONCUR). Lecture notes in computer science, vol 962. Springer, Berlin, pp 234–248
Shapley LS (1953) Stochastic games. Proc Natl Acad Sci USA 39(10):1095
Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2): 285–309
Timmer M, Katoen J-P van de Pol J, Stoelinga M (2012) Efficient modelling and generation of Markov automata. In: Int’l conf. on concurrency theory (CONCUR). Lecture notes in computer science, vol 7454. Springer, Berlin, pp 364–379
Timmer M, van de Pol J, Stoelinga M (2013) Confluence reduction for Markov automata. In: Int’l conf. on formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science, vol 8053. Springer, Berlin, pp 243–257
Wolovick N, Johr S (2006) A characterization of meaningful schedulers for continuous-time Markov decision processes. In: Asarin E, Bouyer P (eds) Int’l conf. on formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science, vol 4202. Springer, Paris, pp 352–367
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by Cliff Jones, Xuandong Li, and Zhiming Liu
Part of this work was done while Ralf Wimmer was a visiting professor at Saarland University, Saarbrücken, Germany. This work was partly supported by the CDZ project CAP (GZ 1023) and by the German Research Foundation (DFG) as part of the Cluster of Excellence BrainLinks/BrainTools (EXC 1086).
Rights and permissions
About this article
Cite this article
Hatefi, H., Wimmer, R., Braitling, B. et al. Cost vs. time in stochastic games and Markov automata. Form Asp Comp 29, 629–649 (2017). https://doi.org/10.1007/s00165-016-0411-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0411-1