Abstract
We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.
Chapter PDF
Similar content being viewed by others
Keywords
- Mixed Integer Linear Programming
- Markov Decision Process
- Mutual Exclusion
- Reward Function
- Reward Property
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Akshay, S., Bertrand, N., Haddad, S., Hélouët, L.: The steady-state control problem for markov decision processes. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 290–304. Springer, Heidelberg (2013)
Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)
Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., Kučera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: LICS 2011, pp. 33–42. IEEE Computer Society (2011)
Brázdil, T., Chatterjee, K., Forejt, V., Kučera, A.: MultiGain: A controller synthesis tool for mdps with multiple mean-payoff objectives. CoRR, abs/1501.03093 (2015)
Chatterjee, K.: Markov decision processes with multiple long-run average objectives. In: FSTTCS, pp. 473–484 (2007)
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: A model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013)
Duflot, M., Fribourg, L., Picaronny, C.: Randomized dining philosophers without fairness assumption. Distributed Computing 17(1), 65–76 (2004)
Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 317–332. Springer, Heidelberg (2012)
Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press (1960)
Lehmann, D., Rabin, M.: On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In: POPL 1981 (1981)
Puterman, M.L.: Markov Decision Processes. J. Wiley and Sons (1994)
Rabin, M.: N-process mutual exclusion with bounded waiting by 4log2 N-valued shared variable. Journal of Computer and System Sciences 25(1), 66–75 (1982)
Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons (1998)
Černý, P., Gopi, S., Henzinger, T.A., Radhakrishna, A., Totla, N.: Synthesis from incompatible specifications. In: EMSOFT, pp. 53–62 (2012)
Wimmer, R., Braitling, B., Becker, B., Hahn, E.M., Crouzen, P., Hermanns, H., Dhama, A., Theel, O.E.: Symblicit calculation of long-run averages for concurrent probabilistic systems. In: QEST, pp. 27–36. IEEE Computer Society Press (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brázdil, T., Chatterjee, K., Forejt, V., Kučera, A. (2015). MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. In: Baier, C., Tinelli, C. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015. Lecture Notes in Computer Science(), vol 9035. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-662-46681-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46680-3
Online ISBN: 978-3-662-46681-0
eBook Packages: Computer ScienceComputer Science (R0)