Abstract
We study the strong and strutter trace distances on Markov chains (MCs). Our interest in these metrics is motivated by their relation to the probabilistic \(\text { LTL}^{}\)-model checking problem: we prove that they correspond to the maximal differences in the probability of satisfying the same \(\text { LTL}^{}\) and \(\text { LTL}^{\text {-}\mathsf {x}}\) (\(\text { LTL}^{}\) without next operator) formulas, respectively. The threshold problem for these distances (whether their value exceeds a given threshold) is NP-hard and not known to be decidable. Nevertheless, we provide an approximation schema where each lower and upper-approximant is computable in polynomial time in the size of the MC.
The upper-approximants are Kantorovich-like pseudometrics, i.e. branching-time distances, that converge point-wise to the linear-time metrics. This convergence is interesting in itself, since it reveals a nontrivial relation between branching and linear-time metric-based semantics that does not hold in the case of equivalence-based semantics.
Work supported by the European Union 7th Framework Programme (FP7/2007–2013) under Grants Agreement nr. 318490 (SENSATION), nr. 601148 (CASSTING) and by the Sino-Danish Basic Research Center IDEA4CPS funded by the Danish National Research Foundation and the National Science Foundation China.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Existence and uniqueness follows by the Hahn-Kolmogorov extension theorem.
- 2.
The MC has been adapted to the case of labeled states, instead of labeled transitions.
- 3.
Note that
, i.e., it is the unique map s.t., for all \(n \ge 1\), 
. - 4.
We assume that
whenever \(i > j\).
, i.e., it is the unique map s.t., for all 
.
whenever References
Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 1–15. Springer, Heidelberg (2013)
Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On the total variation distance of semi-markov chains. In: Pitts, A. (ed.) FOSSACS 2015. LNCS, vol. 9034, pp. 185–199. Springer, Heidelberg (2015)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125–126. IEEE Computer Society (2006)
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)
Chen, T., Kiefer, S.: On the total variation distance of labelled markov chains. In: CSL-LICS 2014, pp. 33:1–33:10. ACM (2014)
Cortes, C., Mohri, M., Rastogi, A.: Lp distance and equivalence of probabilistic automata. Int. J. Found. Comput. Sci. 18(04), 761–779 (2007)
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching metrics for quantitative transition systems. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 97–109. Springer, Heidelberg (2004)
de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: LICS, pp. 99–108, July 2007
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labeled markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 258–273. Springer, Heidelberg (1999)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled markov processes. Theoret. Comput. Sci. 318(3), 323–354 (2004)
Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: LICS, pp. 413–422. IEEE Computer Society (2002)
Ferns, N., Precup, D., Knight, S.: Bisimulation for markov decision processes through families of functional expressions. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. LNCS, vol. 8464, pp. 319–342. Springer, Heidelberg (2014)
Fu, H.: Computing game metrics on markov decision processes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 227–238. Springer, Heidelberg (2012)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Lamport, L.: What good is temporal logic?. In: IFIP, pp. 657–668 (1983)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Lindvall, T.: Lectures on the Coupling Method. Wiley Series in Probability and Mathematical Statistics. Wiley, New York (1992)
Lyngsø, R.B., Pedersen, C.N.S.: The consensus string problem and the complexity of comparing hidden Markov models. J. Comput. Syst. Sci. 65(3), 545–569 (2002)
Mio, M.: Upper-expectation bisimilarity and Lukasiewicz \(\mu \)-calculus. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 335–350. Springer, Heidelberg (2014)
Pnueli, A.: The temporal logic of programs. In: SFCS, pp. 46–57. IEEE Computer Society (1977)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bacci, G., Bacci, G., Larsen, K.G., Mardare, R. (2015). Converging from Branching to Linear Metrics on Markov Chains. In: Leucker, M., Rueda, C., Valencia, F. (eds) Theoretical Aspects of Computing - ICTAC 2015. ICTAC 2015. Lecture Notes in Computer Science(), vol 9399. Springer, Cham. https://doi.org/10.1007/978-3-319-25150-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-25150-9_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25149-3
Online ISBN: 978-3-319-25150-9
eBook Packages: Computer ScienceComputer Science (R0)