Abstract
Semi-Markov decision processes (SMDPs) are continuous-time Markov decision processes where the residence-time on states is governed by generic distributions on the positive real line.
In this paper we consider the problem of comparing two SMDPs with respect to their time-dependent behaviour. We propose a hemimetric between processes, which we call simulation distance, measuring the least acceleration factor by which a process needs to speed up its actions in order to behave at least as fast as another process. We show that this distance can be computed in time \(\mathcal {O}(n^2 (f(l) + k) + mn^7)\), where n is the number of states, m the number of actions, k the number of atomic propositions, and f(l) the complexity of comparing the residence-time between states. The theoretical relevance and applicability of this distance is further argued by showing that (i) it is suitable for compositional reasoning with respect to CSP-like parallel composition and (ii) has a logical characterisation in terms of a simple Markovian logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
As is standard, we consider numbers to be represented as floating points of bounded size in their binary representation.
References
Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Additive and multiplicative notions of leakage, and their capacities. In: CSF, pp. 308–322 (2014)
Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)
Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149–214 (2005)
Chatzikokolakis, K., Andrés, M.E., Bordenabe, N.E., Palamidessi, C.: Broadening the scope of differential privacy using metrics. In: De Cristofaro, E., Wright, M. (eds.) PETS 2013. LNCS, vol. 7981, pp. 82–102. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39077-7_5
Chen, D., van Breugel, F., Worrell, J.: On the complexity of computing probabilistic bisimilarity. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 437–451. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28729-9_29
Desharnais, J.: Logical characterization of simulation for labelled Markov chains. In: PROBMIV, pp. 33–48. University of Birmingham, Technical report, CS-99-8, August 1999
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)
Ferns, N., Panangaden, P., Precup, D.: Bisimulation metrics for continuous Markov decision processes. SIAM J. Comput. 40(6), 1662–1714 (2011)
Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods, North-Holland, pp. 443–458 (1990)
Götz, N., Herzog, U., Rettelbach, M.: Multiprocessor and distributed system design: the integration of functional specification and performance analysis using Stochastic Process Algebras. In: Donatiello, L., Nelson, R. (eds.) Performance/SIGMETRICS - 1993. LNCS, vol. 729, pp. 121–146. Springer, Heidelberg (1993). https://doi.org/10.1007/BFb0013851
Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45804-2
Hermanns, H., Herzog, U., Mertsiotakis, V.: Stochastic process algebras - between LOTOS and Markov chains. Comput. Netw. 30(9–10), 901–924 (1998)
Hillston, J.: A Compositional Approach to Performance Modelling. Distinguished Dissertations in Computer Science. Cambridge University Press, New York (2005)
Jou, C.-C., Smolka, S.A.: Equivalences, congruences, and complete axiomatizations for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 367–383. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039071
Kozen, D., Mardare, R., Panangaden, P.: Strong completeness for Markovian logics. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 655–666. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40313-2_58
Larsen, K.G., Mardare, R., Panangaden, P.: Taking it to the limit: approximate reasoning for Markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 681–692. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32589-2_59
Neuhäußer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412–427. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_28
Pedersen, M.R., Bacci, G., Larsen, K.G., Mardare, R.: A hemimetric extension of simulation for semi-Markov decision processes. Technical report, Aalborg University, Department of Computer Science (2018). http://people.cs.aau.dk/mrp/pubs/simuldist.pdf
Perman, M., Senegacnik, A., Tuma, M.: Semi-Markov models with an application to power-plant reliability analysis. IEEE Trans. Reliab. 46(4), 526–532 (1997)
Pievatolo, A., Tironi, E., Valade, I.: Semi-Markov processes for power system reliability assessment with application to uninterruptible power supply. IEEE Trans. Power Syst. 19(3), 1326–1333 (2004)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)
Shaked, M., Shanthikumar, G.: Stochastic Orders. Springer Series in Statistics. Springer, New York (2007). https://doi.org/10.1007/978-0-387-34675-5
Sokolova, A., de Vink, E.P.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems: A Guide to Current Research. LNCS, vol. 2925, pp. 1–43. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24611-4_1
Song, L., Zhang, L., Godskesen, J.C.: Bisimulations and logical characterizations on continuous-time Markov decision processes. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 98–117. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54013-4_6
Zhang, L.: Decision algorithms for probabilistic simulations. Ph.D. thesis, Saarland University, Saarbrücken, Germany (2009)
Acknowledgments
We thank the anonymous reviewers for helpful suggestions as well as Robert Furber and Giovanni Bacci for insightful discussions. This research was supported by the Danish FTP project ASAP, the ERC Advanced Grant LASSO, and the Sino-Danish Basic Research Center IDEA4CPS.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Pedersen, M.R., Bacci, G., Larsen, K.G., Mardare, R. (2018). A Hemimetric Extension of Simulation for Semi-Markov Decision Processes. In: McIver, A., Horvath, A. (eds) Quantitative Evaluation of Systems. QEST 2018. Lecture Notes in Computer Science(), vol 11024. Springer, Cham. https://doi.org/10.1007/978-3-319-99154-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-99154-2_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99153-5
Online ISBN: 978-3-319-99154-2
eBook Packages: Computer ScienceComputer Science (R0)