Abstract
Probabilistic transition system specifications (PTSS) provide structural operational semantics for reactive probabilistic labeled transition systems. Bisimulation equivalences and bisimulation metrics are fundamental notions to describe behavioral relations and distances of states, respectively. We provide a method to generate from a PTSS a sound and ground-complete equational axiomatization for strong and convex bisimilarity. The construction is based on the method of Aceto, Bloom and Vaandrager developed for non-deterministic transition system specifications. The novelty in our approach is to employ many-sorted algebras to axiomatize separately non-deterministic choice, probabilistic choice and their interaction. Furthermore, we generalize this method to axiomatize the strong and convex metric bisimulation distance of PTSS.
Supported by ANPCYT PICT 2012-1823, SeCyT-UNC 05/B497 and 05/BP02, Eramus Mundus Action 2 Lot 13A EU Mobility Programme 2010-2401/001-001-EMA2 and EU 7FP grant agreement 295261 (MEALS).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aceto, L., Bloom, B., Vaandrager, F.: Turning SOS rules into equations. Inf. Comput. 111(1), 1–52 (1994)
Aceto, L., Goriac, E.-I., Ingolfsdottir, A., Mousavi, M.R., Reniers, M.A.: Exploiting algebraic laws to improve mechanized axiomatizations. In: Heckel, R. (ed.) CALCO 2013. LNCS, vol. 8089, pp. 36–50. Springer, Heidelberg (2013)
Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, New York (2009)
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. TCS 51, 129–176 (1987)
Bandini, E., Segala, R.: Axiomatizations for probabilistic bisimulation. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 370–381. Springer, Heidelberg (2001)
Bartels, F.: On Generalised Coinduction and Probabilistic Specification Formats. Ph.D. thesis, VU University Amsterdam (2004)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42, 232–268 (1995)
Contejean, E., Marché, C., Rabehasaina, L.: Rewrite systems for natural, integral, and rational arithmetic. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 98–112. Springer, Heidelberg (1997)
D’Argenio, P.R., Lee, M.D.: Probabilistic transition system specification: Congruence and full abstraction of bisimulation. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 452–466. Springer, Heidelberg (2012)
Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proc. LICS 2002, pp. 413–422. IEEE (2002)
Gazda, M., Fokkink, W.: Turning GSOS rules into equations for linear time-branching time semantics. The Computer Journal 56(1), 34–44 (2013)
Gebler, D., Tini, S.: Compositionality of approximate bisimulation for probabilistic systems. In: Proc. EXPRESS/SOS 2013. EPTCS, vol. 120, pp. 32–46 (2013)
Goguen, J.A., Meseguer, J.: Completeness of many-sorted equational logic. SIGPLAN Not. 17(1), 9–17 (1982)
Groote, J.F., Vaandrager, F.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100, 202–260 (1992)
Hennessy, M.: Exploring probabilistic bisimulations, part I. Formal Aspects of Computing 24(4-6), 749–768 (2012)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)
Lee, M.D., Gebler, D., D’Argenio, P.R.: Tree rules in probabilistic transition system specifications with negative and quantitative premises. In: Proc. EXPRESS/SOS 2012. EPTCS, vol. 89, pp. 115–130 (2012)
Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theor. Comput. Sci. 373(3), 238–272 (2007)
Plotkin, G.: A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University (1981), reprinted in J. Log. Algebr. Program, 60-61, 17–139 (2004)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
D’Argenio, P.R., Gebler, D., Lee, M.D. (2014). Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)