article

Metrics for labelled Markov processes

Authors:

Josée Desharnais,

Radha Jagadeesan,

Prakash PanangadenAuthors Info & Claims

Theoretical Computer Science, Volume 318, Issue 3

Pages 323 - 354

https://doi.org/10.1016/j.tcs.2003.09.013

Published: 08 June 2004 Publication History

Abstract

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.

References

[1]

{1} R. Alur, L. Jagadeesan, J.J. Kott, J.E. von Olnhausen, Model-checking of real-time systems: a telecommunications application, in: Proc. 19th Internat. Conf. on Software Engineering, Boston, Massachusetts, USA, 1997, pp. 514-524.]]

Digital Library

[2]

{2} J.C.M. Baeten, J.A. Bergstra, S.A. Smolka, Axiomatizing probabilistic processes: ACP with generative probabilities, Inform. Comput. 121 (2) (1995) 234-255.]]

Digital Library

[3]

{3} C. Baier, E. Clark, V. Hartonas-Garmhausen, M. Kwiatkowska, M. Ryan, Symbolic model checking for probabilistic processes, in: Proc. 24th Internat. Coll. on Automata Languages and Programming, Lecture Notes in Computer Science. Vol. 1256, Springer, Berlin, 1997, pp. 430-440.]]

[4]

{4} J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, UppAal: a tool suite for automatic verification of real-time systems, in: R. Alur, T. Henzinger, E. Sontag (Eds.), Hybrid Systems III, Lecture Notes in Computer Science. Vol. 1066, Springer, Berlin, 1996, pp. 232-243.]]

[5]

{5} A. Bianco, L. de Alfaro, Model checking of probabilistic and nondeterministic systems, in: P.S. Thiagarajan (Ed.), Proc. 15th Ann. Conf. on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 1026, Springer, Berlin, 1995, pp. 499-513.]]

[6]

{6} R. Blute, J. Desharnais, A. Edalat, P. Panangaden, Bisimulation for labelled Markov processes, in: Proc. 12th IEEE Symp. on Logic in Computer Science, Warsaw, Poland, 1997.]]

[7]

{7} R. Cleaveland, S. Smolka, A. Zwarico, Testing preorders for probabilistic processes, in: W. Kuich (Ed.), Automata, Languages and Programming (ICALP 92), Lecture Notes in Computer Science, Vol. 623, Springer, Berlin, 1992, pp. 708-719.]]

[8]

{8} C. Courcoubetis, M. Yannakakis, The complexity of probabilistic verification, J. ACM 42 (4) (1995) 857-907.]]

Digital Library

[9]

{9} T. Cover, J. Thomas, Elements of Information Theory. Wiley, New York, 1991.]]

[10]

{10} L. de Alfaro, private communication.]]

[11]

{11} J. de Kleer, B.C. Williams, Diagnosis with behavioral modes, in: Proc. 11th Internat. Joint Conf. on Artificial Intelligence, Detroit, Michigan, USA, August 1989, pp. 1324-1330.]]

[12]

{12} J. Desharnais, Labelled Markov processes, Ph.D. Thesis, McGill University, November 1999.]]

[13]

{13} J. Desharnais, Logical characterization of simulation for Markov chains, in: M. Kwiatkowska (Ed.), Probmiv99, Proc. Second Internat. Workshop on Probabilistic Methods in Verification, The University of Birmingham, 1999, pp. 33-48, available as TR: CSR-99-8.]]

[14]

{14} J. Desharnais, A. Edalat, P. Panangaden, A logical characterization of bisimulation for labelled Markov processes, in: Proc. 13th IEEE Symp. on Logic in Computer Science, Indianapolis, IEEE Press, New York, June 1998, pp. 478-489.]]

[15]

{15} J. Desharnais, A. Edalat, P. Panangaden, Bisimlation for labeled Markov processes, Inform. Comput. 179 (2) (2002) 163-193.]]

Digital Library

[16]

{16} J. Desharnais, V. Gupta, R. Jagadeesan, P. Panangaden, Metrics for labeled Markov systems, in: Proc. CONCUR99, Lecture Notes in Computer Science, Springer, Berlin, 1999.]]

[17]

{17} J. Desharnais, V. Gupta, R. Jagadeesan, P. Panangaden, Approximation of labeled Markov processes. in: Proc. 15th Ann. IEEE Symp. on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, June 2000, pp. 95-106.]]

[18]

{18} J. Desharnais, V. Gupta, R. Jagadeesan, P. Panangaden, The metric analogue of weak bisimulation for labelled Markov processes, in: Proc. 17th Ann. IEEE Symp. on Logic in Computer Science, Copenhagen, Denmark, July 2002, pp. 413-422.]]

[19]

{19} J. Desharnais, V. Gupta, R. Jagadeesan, P. Panangaden, Approximating labeled Markov processes, Inform. Comput. 184 (1) (2003) 160-200.]]

Digital Library

[20]

{20} E. de Vink, J.J.M.M. Rutten, Bisimulation for probabilistic transition systems: a coalgebraic approach, Theoret. Comput. Sci. 221 (1/2) (1999) 271-293.]]

Digital Library

[21]

{21} L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, Berlin, 1996.]]

[22]

{22} D. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, ACM Distinguished Dissertations, MIT Press, Cambridge, MA, 1988.]]

[23]

{23} G.A. Edgar, Integral, Probability and Fractal Measures, Springer, Berlin, 1998.]]

[24]

{24} R. Geroch, Mathematical Physics, in: Chicago Lectures in Physics, University of Chicago Press, Chicago, 1985.]]

[25]

{25} A. Giacalone, C. Jou, S. Smolka, Algebraic reasoning for probabilistic concurrent systems, in: Proc. Working Conf. Programming Concepts and Methods, IFIP TC2, Sea of Galilee, Israel, 1990.]]

[26]

{26} V. Gupta, T.A. Henzinger, R. Jagadeesan, Robust timed automata, in: O. Maler (Ed.), Hybrid and Real-Time Systems, Lecture Notes in Computer Science, Vol. 1201, Springer, Berlin, March 1997, pp. 331-345.]]

Digital Library

[27]

{27} H. Hansson, B. Jonsson, A calculus for communicating systems with time and probabilities, in: Proc. 11th IEEE Real-time Systems Symp., IEEE Computer Society Press, Silver Spring, MD, 1990, pp. 278-287.]]

[28]

{28} S. Hart, M. Sharir, Probabilistic propositional temporal logics, Inform. Control 70 (1986) 97-155.]]

Digital Library

[29]

{29} J. Hillston, A compositional approach to performance modelling, Ph.D. Thesis, University of Edinburgh, 1994 (Published as a Distinguished Dissertation by Cambridge University Press in 1996).]]

[30]

{30} J.E. Hutchinson, Fractals and self-similarity, Indiana Univ. Math. J. 30 (1981) 713-747.]]

[31]

{31} M. Huth, M. Kwiatkowska, Quantitative analysis and model checking, in: Proc. 12 IEEE Symp. on Logic in Computer Science, IEEE Press, New York, 1997, pp. 111-122.]]

[32]

{32} C. Jones, G.D. Plotkin, A probabilistic powerdomain of evaluations, in: Proc. Fourth Ann. IEEE Symp. on Logic in Computer Science, Asilomar, California, USA, 1989, pp. 186-195.]]

Digital Library

[33]

{33} B. Jonsson, W. Yi, Compositional testing preorders for probabilistic processes, in: Proc. 10th Ann. IEEE Symp. on Logic in Computer Science, San Diego, California, USA, 1995, pp. 431-441.]]

[34]

{34} M.B. Josephs, Receptive process theory, Acta Inform. 29 (1) (1992) 17-31.]]

Digital Library

[35]

{35} C.-C. Jou, S.A. Smolka, Equivalences, congruences, and complete axiomatizations for probabilistic processes, in: J.C.M. Baeten, J.W. Klop (Eds.), CONCUR 90 First Internat. Conf. on Concurrency Theory, Lecture Notes in Computer Science, Vol. 458, Springer, Berlin, 1990.]]

[36]

{36} D. Kozen, A probabilistic PDL, J. Comput. Systems Sci. 30 (2) (1985) 162-178.]]

[37]

{37} M. Kwiatkowska, G.J. Norman, Probabilistic metric semantics for a simple language with recursion, in: W. Penczek, A. Szalas (Eds.), Proc. 21st Internat. Symp. on Math. Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 1113, Springer, Berlin, 1996, pp. 419-430.]]

[38]

{38} M. Kwiatkowska, G.J. Norman, A testing equivalence for reactive probabilistic processes, in: I. Castelliani, C. Palamidessi (Eds.), Proc. Fifth Internat. Workshop on Expressiveness in Concurrency, Electronic Notes in Theoretical Computer Science, Vol. 16, Elsevier, Amsterdam, 1998.]]

[39]

{39} K.G. Larsen, A. Skou, Bisimulation through probablistic testing, Inform. Comput. 94 (1991) 1-28.]]

Digital Library

[40]

{40} P.D. Lincoln, J.C. Mitchell, M. Mitchell, A. Scedrov, A probabilistic poly-time framework for protocol analysis, in: Proc. of the 5th ACM Conference on Computer and Communication Security (CCS-5), San Francisco, 1998, pp. 112-121.]]

Digital Library

[41]

{41} N.A. Lynch, M.R. Tuttle, An introduction to input/output automata, CWI Quart. 2 (3) (1989) 219-246.]]

[42]

{42} M.A. Marsan, Stochastic petri nets: an elementary introduction, in: Advances in Petri Nets 1989, Springer, Berlin, 1989, pp. 1-29.]]

Digital Library

[43]

{43} K.R. Parthasarathy, Probability Measures on Metric Spaces, Academic Press, New York, 1967.]]

[44]

{44} J.L. Peterson, A. Silberschatz, Operating System Concepts, Addison-Wesley Inc., Reading, MA, 1985.]]

[45]

{45} R. Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. Thesis, Department of Electrical Engineering and Computer Science, MIT, 1995, Also appears as Technical Report MIT/LCS/TR-676.]]

[46]

{46} F.W. Vaandrager, On the relationship between process algebra and input/output automata, in: Proc. Sixth Ann. IEEE Symp. on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, July 1991, pp. 387-398.]]

[47]

{47} F. van Breugel, private communication.]]

[48]

{48} F. van Breugel, private communication.]]

[49]

{49} F. van Breugel, M. Mislove, J. Ouaknine, J. Worrell, An intrinsic characterization of approximate probabilistic bisimilarity, in: Proc FOSSACS 03, Lecture Notes in Computer Science, Vol. 2620, Springer, Berlin, 2003.]]

[50]

{50} F. van Breugel, J. Worrell, An algorithm for quantitative verification on probabilistic systems, in: K.G. Larsen, M. Nielsen (Eds.), Proc. 12th Internat. Conf. on Concurrency Theory-CONCUR'01, Lecture Notes in Computer Science. Vol. 2154, Springer, Berlin, 2001, pp. 336-350.]]

[51]

{51} F. van Breugel, J. Worrell, Towards quantitative verification of probabilistic systems, in: Proc. 28th Internat. Coll. on Automata, Languages and Programming, Springer, Berlin, 2001.]]

[52]

{52} R. van Glabbeek, S.A. Smolka, B.U. Steffen, Reactive, generative, and stratified models of probabilistic processes, Inform. Comput. 121 (1) (1995) 59-80.]]

Digital Library

[53]

{53} N. Viswanadham, Y. Narahari, Performance Modeling of Automated Manufacturing Systems, Prentice-Hall Inc., Englewood Cliffs, NJ, 1992.]]

[54]

{54} S.-H. Wu, S.A. Smolka, E.W. Stark, Composition and behaviors for probabilistic I/O automata, Theoret. Comput. Sci. 176 (1-2) (1997) 1-36.]]

Digital Library

Cited By

Kori MWatanabe KRot JKatsumata SSobocinski PLago UEsparza J(2024)Composing Codensity BisimulationsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662139(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662139
Bacci GBacci GLarsen KSquillace GTribastone MTschaikowski MVandin A(2024)Dissimilarity for Linear Dynamical SystemsQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_8(125-142)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_8
Baldan PEggert RKönig BMatt TPadoan T(2023)A Monoidal View on Fixpoint ChecksGraph Transformation10.1007/978-3-031-36709-0_1(3-21)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-36709-0_1
Show More Cited By

Index Terms

Metrics for labelled Markov processes
1. Mathematics of computing
  1. Mathematical analysis
    1. Numerical analysis
  2. Probability and statistics
    1. Probabilistic representations
      1. Markov networks
    2. Stochastic processes
      1. Markov processes
2. Theory of computation
  1. Theory and algorithms for application domains
    1. Machine learning theory
      1. Markov decision processes

Recommendations

Testing Labelled Markov Processes
ICALP '02: Proceedings of the 29th International Colloquium on Automata, Languages and Programming

Larsen and Skou introduced a notion of bisimulation for probabilistic transition systems. They characterized probabilistic bisimilarity in terms of a probabilistic modal logic and also in terms of 'button pressing' tests. Desharnais et al. extended the ...
The Research of Metrics Repository for Business Process Metrics
ISCID '09: Proceedings of the 2009 Second International Symposium on Computational Intelligence and Design - Volume 02

According to the reusability of its assets, metrics repository as a place to collect and store all assets in the course of the business process metrics plays a more and more important role in business process metrics, provides effective service for it, ...
Using process mining metrics to measure noisy process fidelity
EASE'09: Proceedings of the 13th international conference on Evaluation and Assessment in Software Engineering

Background: When teams follow a software development process they do not follow the process consistently. We need a method to measure their fidelity to that process. Objective: To evaluate Rozinat and Aalst's metrics for process conformance to a state ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 318, Issue 3

Logic, semantics and theory of programming

8 June 2004

227 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 08 June 2004

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

98
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kori MWatanabe KRot JKatsumata SSobocinski PLago UEsparza J(2024)Composing Codensity BisimulationsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662139(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662139
Bacci GBacci GLarsen KSquillace GTribastone MTschaikowski MVandin A(2024)Dissimilarity for Linear Dynamical SystemsQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_8(125-142)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_8
Baldan PEggert RKönig BMatt TPadoan T(2023)A Monoidal View on Fixpoint ChecksGraph Transformation10.1007/978-3-031-36709-0_1(3-21)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-36709-0_1
Barthe GCrubillé RDal Lago UGavazzo F(2022)On Feller continuity and full abstractionProceedings of the ACM on Programming Languages10.1145/35476516:ICFP(826-854)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547651
Dagnino FPasquali F(2022)Logical Foundations of Quantitative EqualityProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533337(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533337
Dal Lago UGavazzo F(2022)Effectful program distancingProceedings of the ACM on Programming Languages10.1145/34986806:POPL(1-30)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498680
Aman BCiobanu G(2022)Dynamics of reputation in mobile agents systems and weighted timed automataInformation and Computation10.1016/j.ic.2020.104653282:COnline publication date: 1-Jan-2022
https://dl.acm.org/doi/10.1016/j.ic.2020.104653
Komorida YKatsumata SHu NKlin BHumeau SEberhart CHasuo I(2022)Codensity Games for BisimilarityNew Generation Computing10.1007/s00354-022-00186-y40:2(403-465)Online publication date: 3-Aug-2022
https://dl.acm.org/doi/10.1007/s00354-022-00186-y
Bartoletti MMurgia MZunino R(2022)A Sound Up-to- Bisimilarity for PCTLCoordination Models and Languages10.1007/978-3-031-08143-9_3(35-52)Online publication date: 13-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-08143-9_3
Castro PKastner TPanangaden PRowland MRanzato MBeygelzimer ADauphin YLiang PVaughan J(2021)MICoProceedings of the 35th International Conference on Neural Information Processing Systems10.5555/3540261.3542566(30113-30126)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.5555/3540261.3542566
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents