article

Bisimulations for non-deterministic labelled markov processes

Authors:

Pedro R. D'argenio,

Pedro Sánchez Terraf,

Nicolás WolovickAuthors Info & Claims

Mathematical Structures in Computer Science, Volume 22, Issue 1

Pages 43 - 68

https://doi.org/10.1017/S0960129511000454

Published: 01 February 2012 Publication History

Abstract

We extend the theory of labelled Markov processes to include internal non-determinism, which is a fundamental concept for the further development of a process theory with abstraction on non-deterministic continuous probabilistic systems. We define non-deterministic labelled Markov processes (NLMP) and provide three definitions of bisimulations: a bisimulation following a traditional characterisation; a state-based bisimulation tailored to our 'measurable' non-determinism; and an event-based bisimulation. We show the relations between them, including the fact that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy-Milner logic that characterises event bisimulation and is sound with respect to the other bisimulations for an arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable <private-char><inline-graphic mime-subtype="gif" xlink="S0960129511000454_char1"/></private-char>. We then introduce a finitary sublogic that characterises all bisimulations for an image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all the notions of bisimulation we consider turn out to be equal. Finally, we show that all these bisimulation notions are different in the general case. The counterexamples that separate them turn out to be non-probabilistic NLMPs.

References

[1]

Billingsley, P. (1995) Probability and Measure, Wiley-Interscience.

[2]

Bohnenkamp, H., D'Argenio, P.R., Hermanns, H. and Katoen, J.-P. (2006) MoDeST: A compositional modeling formalism for real-time and stochastic systems. IEEE Trans. Softw. Eng. 32 812-830.

Digital Library

[3]

Bravetti, M. (2002) Specification and Analysis of Stochastic Real-Time Systems, Ph.D. thesis, Universit à di Bologna, Padova, Venezia.

[4]

Bravetti, M. and D'Argenio, P. R. (2004) Tutte le algebre insieme: Concepts, discussions and relations of stochastic process algebras with general distributions. In: Validation of Stochastic Systems. Springer-Verlag Lecture Notes in Computer Science 2925 44-88.

[5]

van Breugel, F. (2005) The metric monad for probabilistic nondeterminism. Draft.

[6]

Cattani, S. (2005) Trace-based Process Algebras for Real-Time Probabilistic Systems, Ph.D. thesis, University of Birmingham.

[7]

Cattani, S., Segala, R., Kwiatkowska, M.Z. and Norman, G. (2005) Stochastic transition systems for continuous state spaces and non-determinism. In: Proceedings FoSSaCS 2005. Springer-Verlag Lecture Notes in Computer Science 3441 125-139.

Digital Library

[8]

Celayes, P. (2006) Procesos de Markov etiquetados sobre espacios de Borel estándar. Master's thesis, FaMAF, Universidad Nacional de Córdoba.

[9]

Clarke, E.M., Grumberg, O. and Peled, D. (1999) Model Checking, MIT Press.

[10]

Danos, V., Desharnais, J., Laviolette, F. and Panangaden, P. (2006) Bisimulation and cocongruence for probabilistic systems. Information and Computation 204 503-523.

Digital Library

[11]

D'Argenio, P. R. (1999) Algebras and Automata for Timed and Stochastic Systems, Ph.D. thesis, Department of Computer Science, University of Twente.

[12]

D'Argenio, P. R. and Katoen, J.-P. (2005) A theory of stochastic systems, Part I: Stochastic automata, and Part II: Process algebra. Information and Computation 203 1-38, 39-74.

Digital Library

[13]

D'Argenio, P. R., Wolovick, N., Terraf, P. S. and Celayes, P. (2009) Nondeterministic labeled markov processes: Bisimulations and logical characterization. In: Quantitative Evaluation of Systems, International Conference on, IEEE Computer Society 11-20.

[14]

Desharnais, J. (1999) Labeled Markov Process, Ph.D. thesis, McGill University.

[15]

Desharnais, J. and Panangaden, P. (2003) Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. J. Log. Algebr. Program. 56 (1-2) 99-115.

[16]

J. Desharnais, A. Edalat and P. Panangaden Bisimulation for labelled Markov processes. Information and Computation 179 (2) 163-193.

[17]

Doberkat, E.-E. (2007) Stochastic relations. Foundations for Markov transition systems, Studies in Informatics Series, Chapman and Hall.

[18]

Giry, M. (1981) A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis. Springer-Verlag Lecture Notes in Mathematics 915 68-85.

[19]

van Glabeek, R. J. (2001) The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In: Bergstra, J. A., Ponse, A. and Smolka, S.A. (eds.) Handbook of Process Algebra, North-Holland 3-99.

[20]

Kechris, A. S. (1995) Classical Descriptive Set Theory, Graduate Texts in Mathematics 156 Springer-Verlag.

[21]

Larsen, K. G. and Skou, A. (1991) Bisimulation through probabilistic testing. Information and Computation 94 (1) 1-28.

Digital Library

[22]

Milner, R. (1989) Communication and Concurrency, Prentice Hall.

[23]

Naimpally, S. (2003) What is a hit-and-miss topology? Topological Commentary 8 (1).

[24]

Parma, A. and Segala, R. (2007) Logical characterizations of bisimulations for discrete probabilistic systems. In: Proceedings FoSSaCS 07. Springer-Verlag Lecture Notes in Computer Science 4423 287-301.

[25]

Puterman, M.L. (1994) Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley-Interscience.

[26]

Segala, R. (1995) Modeling and Verification of Randomized Distributed Real-Time Systems, Ph.D. thesis, Massachusetts Institute of Technology.

[27]

Strulo, B. (1993) Process Algebra for Discrete Event Simulation, Ph.D. thesis, Department of Computing, Imperial College, University of London.

[28]

Vardi, M.Y. (1985) Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings 26th FOCS, IEEE Computer Society 327-338.

Digital Library

[29]

Viglizzo, I.D. (2005) Coalgebras on Measurable Spaces, Ph.D. thesis, Department of Mathematics, Indiana University.

Cited By

Benveniste ARaclet J(2023)Mixed Nondeterministic-Probabilistic AutomataDiscrete Event Dynamic Systems10.1007/s10626-023-00375-x33:4(455-505)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s10626-023-00375-x
Baier CD’Argenio PHermanns H(2020)On the probabilistic bisimulation spectrum with silent movesActa Informatica10.1007/s00236-020-00379-257:3-5(465-512)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s00236-020-00379-2
Gburek DBaier C(2018)Bisimulations, logics, and trace distributions for stochastic systems with rewardsProceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)10.1145/3178126.3178139(31-40)Online publication date: 11-Apr-2018
https://dl.acm.org/doi/10.1145/3178126.3178139
Show More Cited By

Bisimulations for non-deterministic labelled markov processes
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic representations
2. Theory of computation

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 ...
Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization
QEST '09: Proceedings of the 2009 Sixth International Conference on the Quantitative Evaluation of Systems

We extend the theory of labeled Markov processeswith internal nondeterminism, a fundamental conceptfor the further development of a process theory withabstraction on nondeterministic continuous probabilisticsystems. We define nondeterministic labeled ...
Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes
VMCAI 2014: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318

In this paper we study strong and weak bisimulation equivalences for continuous-time Markov decision processes CTMDPs and the logical characterizations of these relations with respect to the continuous-time stochastic logic CSL. For strong bisimulation, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Mathematical Structures in Computer Science

Mathematical Structures in Computer Science Volume 22, Issue 1

February 2012

132 pages

ISSN:0960-1295

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 February 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Benveniste ARaclet J(2023)Mixed Nondeterministic-Probabilistic AutomataDiscrete Event Dynamic Systems10.1007/s10626-023-00375-x33:4(455-505)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s10626-023-00375-x
Baier CD’Argenio PHermanns H(2020)On the probabilistic bisimulation spectrum with silent movesActa Informatica10.1007/s00236-020-00379-257:3-5(465-512)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s00236-020-00379-2
Gburek DBaier C(2018)Bisimulations, logics, and trace distributions for stochastic systems with rewardsProceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)10.1145/3178126.3178139(31-40)Online publication date: 11-Apr-2018
https://dl.acm.org/doi/10.1145/3178126.3178139
Wu HChen YBu TDeng Y(2018)Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systemsFuzzy Sets and Systems10.1016/j.fss.2017.02.008333:C(106-123)Online publication date: 15-Feb-2018
https://dl.acm.org/doi/10.1016/j.fss.2017.02.008
Doberkat E(2017)Using coalgebras and the Giry monad for interpreting game logics -- a tutorialFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6155-511:6(948-970)Online publication date: 1-Dec-2017
https://dl.acm.org/doi/10.1007/s11704-016-6155-5
D'Argenio PGebler DLee M(2016)A general SOS theory for the specification of probabilistic transition systemsInformation and Computation10.1016/j.ic.2016.03.009249:C(76-109)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1016/j.ic.2016.03.009
Hartmanns AHermanns H(2015)In the quantitative automata zooScience of Computer Programming10.1016/j.scico.2015.08.009112:P1(3-23)Online publication date: 15-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2015.08.009
Budde CD'Argenio PSánchez Terraf PWolovick N(2012)A Theory for the Semantics of Stochastic and Non-deterministic Continuous SystemsAdvanced Lectures of the International Autumn School on Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems - Volume 845310.1007/978-3-662-45489-3_3(67-86)Online publication date: 22-Oct-2012
https://dl.acm.org/doi/10.1007/978-3-662-45489-3_3
Fränzle MHahn EHermanns HWolovick NZhang LCaccamo MFrazzoli EGrosu R(2011)Measurability and safety verification for stochastic hybrid systemsProceedings of the 14th international conference on Hybrid systems: computation and control10.1145/1967701.1967710(43-52)Online publication date: 12-Apr-2011
https://dl.acm.org/doi/10.1145/1967701.1967710

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