Abstract
We present a format for the specification of probabilistic transition systems that guarantees that bisimulation equivalence is a congruence for any operator defined in this format. In this sense, the format is somehow comparable to the ntyft/ntyxt format in a non-probabilistic setting. We also study the modular construction of probabilistic transition systems specifications and prove that some standard conservative extension theorems also hold in our setting. Finally, we show that the trace congruence for image-finite processes induced by our format is precisely bisimulation on probabilistic systems.
Partially supported by Project ANPCYT PAE-PICT 02272 and SeCyT-UNC.
Chapter PDF
References
Aceto, L., Fokkink, W., Verhoef, C.: Conservative extension in structural operational semantics. In: Current Trends in Theor. Comput. Sci., pp. 504–524. World Scientific (2001)
Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, pp. 197–292. Elsevier (2001)
Baeten, J.C.M., Bergstra, J.A.: Process Algebra with a Zero Object. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 83–98. Springer, Heidelberg (1990)
Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes: ACP with generative probabilities. Inf. Comput. 121(2), 234–255 (1995)
Baier, C.: On Algorithmics Verification Methods for Probabilistic Systems. Habilitation thesis, University of Mannheim (1999)
Bartels, F.: GSOS for probabilistic transition systems. Electr. Notes Theor. Comput. Sci. 65(1) (2002)
Bartels, F.: On Generalised Coinduction and Probabilistic Specification Formats. PhD thesis, Vrije Universiteit (2004)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995)
Bol, R., Groote, J.F.: The meaning of negative premises in transition system specifications. J. ACM 43(5), 863–914 (1996)
D’Argenio, P.R., Verhoef, C.: A general conservative extension theorem in process algebras with inequalities. Theor. Comput. Sci. 177(2), 351–380 (1997)
Fokkink, W., van Glabbeek, R.J.: Ntyft/ntyxt rules reduce to ntree rules. Inf. Comput. 126(1) (1996)
Groote, J.F.: Transition system specifications with negative premises. Theor. Comput. Sci. 118(2), 263–299 (1993)
Groote, J.F., Vaandrager, F.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100(2), 202–260 (1992)
Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Handbook of Process Algebra, pp. 685–710. Elsevier (2001)
Klin, B.: Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci. 412(38), 5043–5069 (2011)
Lanotte, R., Tini, S.: Probabilistic Congruence for Semistochastic Generative Processes. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 63–78. Springer, Heidelberg (2005)
Lanotte, R., Tini, S.: Probabilistic bisimulation as a congruence. ACM Trans. Comput. Log. 10(2) (2009)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Milner, R.: Communication and Concurrency. Prentice-Hall, Inc. (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. PhD thesis. MIT (1995)
Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: LICS, pp. 280–291 (1997)
van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. J. Log. Algebr. Program. 60-61, 229–258 (2004)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
D’Argenio, P.R., Lee, M.D. (2012). Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation. In: Birkedal, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2012. Lecture Notes in Computer Science, vol 7213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28729-9_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-28729-9_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28728-2
Online ISBN: 978-3-642-28729-9
eBook Packages: Computer ScienceComputer Science (R0)