Linear Distances between Markov Chains
We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results.
probabilistic systems
verification
statistical model checking
temporal logic
behavioural equivalence
20:1-20:15
Regular Paper
Przemyslaw
Daca
Przemyslaw Daca
Thomas A.
Henzinger
Thomas A. Henzinger
Jan
Kretinsky
Jan Kretinsky
Tatjana
Petrov
Tatjana Petrov
10.4230/LIPIcs.CONCUR.2016.20
Alessandro Abate. Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: A survey. Electr. Notes Theor. Comput. Sci., 297:3-25, 2013.
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. The BisimDist library: Efficient computation of bisimilarity distances for Markovian models. In QEST, pages 278-281, 2013.
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Computing behavioral distances, compositionally. In MFCS, pages 74-85, 2013.
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. In TACAS, pages 1-15, 2013.
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Converging from branching to linear metrics on Markov chains. In ICTAC, pages 349-367, 2015.
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On the total variation distance of semi-Markov chains. In FoSSaCS, pages 185-199, 2015.
Paul Caspi and Albert Benveniste. Toward an approximation theory for computerised control. In EMSOFT, pages 294-304, 2002.
Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. In CSL-LICS, pages 33:1-33:10, 2014.
Przemyslaw Daca, Thomas A. Henzinger, Jan Křetínský, and Tatjana Petrov. Linear distances between Markov chains. Technical Report abs/1605.00186, arXiv.org, 2014.
Przemyslaw Daca, Thomas A. Henzinger, Jan Křetínský, and Tatjana Petrov. Faster statistical model checking for unbounded temporal properties. TACAS, pages 112-129, 2016.
Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quantitative transition systems. In ICALP, pages 97-109, 2004.
Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, and Mariëlle Stoelinga. Game relations and metrics. In LICS, pages 99-108, 2007.
Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled Markov systems. In CONCUR, pages 258-273, 1999.
Jyotirmoy V. Deshmukh, Rupak Majumdar, and Vinayak S. Prabhu. Quantifying conformance using the Skorokhod metric. In CAV, pages 234-250, 2015.
Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci., 19(3):549-563, 2008.
Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite Markov decision processes. In AAAI, pages 950-951, 2004.
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. In FOSSACS, pages 303-318, 2016.
Antoine Girard and George J. Pappas. Approximate bisimulation: A bridge between computer science and control theory. Eur. J. Control, 17(5-6):568-578, 2011.
Leo A Goodman. Simultaneous confidence intervals for contrasts among multinomial populations. The Annals of Mathematical Statistics, pages 716-725, 1964.
Manfred Jaeger, Hua Mao, Kim G. Larsen, and Radu Mardare. Continuity properties of distances for Markov processes. In QEST, pages 297-312, 2014.
Stefan Kiefer and A. Prasad Sistla. Distinguishing hidden markov chains. In 31th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, 2016.
Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. In POPL, pages 344-352, 1989.
Rupak Majumdar and Vinayak S. Prabhu. Computing the Skorokhod distance between polygonal traces. In HSCC, pages 199-208, 2015.
Ilya Tkachev and Alessandro Abate. On approximation metrics for linear temporal model-checking of stochastic systems. In HSCC, pages 193-202, 2014.
Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount for probabilistic systems. In FOSSACS, pages 123-137, 2007.
Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comput. Sci., 360(1-3):373-385, 2006.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode