Probabilistic bisimulation as a congruence

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Probabilistic bisimulation as a congruence

Full text

Pdf (403 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 2 (February 2009) table of contents

Article No. 9

Year of Publication: 2009

ISSN:1529-3785

Authors

Ruggero Lanotte	Università dell'Insubria, Como, Italy
Simone Tini	Università dell'Insubria, Como, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 69, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1462179.1462181 What is a DOI?

ABSTRACT

We propose both an SOS transition rule format for the generative model of probabilistic processes, and an SOS transition rule format for the reactive model of the probabilistic processes. Our rule formats guarantee that probabilistic bisimulation is a congruence with respect to process algebra operations. Moreover, our rule format for generative process algebras guarantees that the probability of the moves of a given process, if there are any, sum up to 1, and the rule format for reactive process algebras guarantees that the probability of the moves of a given process labeled with the same action, if there are any, sum up to 1. We show that most operations of the probabilistic process algebras studied in the literature are captured by our formats, which, therefore, have practical applications.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Aceto, L., Fokkink, W. J., and Verhoef, C. 2001. Structural operational semantics. In Handbook of Process Algebra, J. A. Bergstra et al., Eds. Elsevier, Amsterdam, 197--292.
	2	Alessandro Aldini , Mario Bravetti , Roberto Gorrieri, A process-algebraic approach for the analysis of probabilistic noninterference, Journal of Computer Security, v.12 n.2, p.191-245, April 2004
	3	J. C. M. Baeten , J. A. Bergstra , S. A. Smolka, Axiomatizing probabilistic processes: ACP with generative probabilities, Information and Computation, v.121 n.2, p.234-255, Sept. 1995 [doi>10.1006/inco.1995.1135]
	4	Christel Baier , Holger Hermanns, Weak Bisimulation for Fully Probabilistic Processes, Proceedings of the 9th International Conference on Computer Aided Verification, p.119-130, June 22-25, 1997
	5	Bartels, F. 2002. GSOS for probabilistic transition systems. In Coalgebraic Methods in Computer Science. Electronic Notes in Theoretical Computer Science, vol. 65. Elsevier, Amsterdam.
	6	Bartels, F. 2004. On generalized coinduction and probabilistic specification formats. Ph.D. thesis, Vrije Univesiteit, Amsterdam.
	7	Bard Bloom , Sorin Istrail , Albert R. Meyer, Bisimulation can't be traced, Journal of the ACM (JACM), v.42 n.1, p.232-268, Jan. 1995 [doi>10.1145/200836.200876]
	8	M. Bravetti , A. Aldini, Discrete time generative-reactive probabilistic processes with different advancing speeds, Theoretical Computer Science, v.290 n.1, p.355-406, 1 January 2003 [doi>10.1016/S0304-3975(01)00344-9]
	9	D'Argenio, P. R., Hermanns, H., and Katoen, J. P. 1999. On generative parallel composition. In Proceedings of the International Workshop on Probabilistic Methods in Verification. Electronic Notes in Theoretical Computer Science, vol. 22. Elsevier, Amsterdam.
	10	de Simone, R. 1985. Higher-Level synchronizing devices in meije-sccs. Theor. Comput. Sci. 37, 245--267.
	11	Giacalone, A., Jou, C. C., and Smolka, S. A. 1990. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of the IFIP Working Conference on Programming, Concepts and Methods. North Holland, 443--458.
	12	Jan Friso Groote, Transition system specifications with negative premises, Theoretical Computer Science, v.118 n.2, p.263-299, Sept. 27, 1993 [doi>10.1016/0304-3975(93)90111-6]
	13	Jan Friso Groote , Frits Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, v.100 n.2, p.202-260, Oct. 1992 [doi>10.1016/0890-5401(92)90013-6]
	14	Jonsson, B., Larsen, K. G., and Yi, W. 2001. Probabilistic extensions of process algebras. In Handbook of Process Algebra, J. A. Bergstra et al., Eds. Elsevier, Amsterdam, 685--710.
	15	Kleene, S. C. 1956. Representation of events in nerve nets and finite automata. In Automata Studies, C. E. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton, NJ, 3--41.
	16	Lanotte, R. and Tini, S. 2005. Probabilistic congruence for generative semistochastic processes. In Proceedings of the International Conference on Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol. 3441. Springer, 63--78.
	17	Kim G. Larsen , Arne Skou, Bisimulation through probabilistic testing, Information and Computation, v.94 n.1, p.1-28, Sept. 1991 [doi>10.1016/0890-5401(91)90030-6]
	18	Milner, R. 1991. The polyadic π-calculus: A tutorial. Tech. rep. ECS--LFCS--91--180, Department of Computer Science, Edinburgh University.
	19	Plotkin, G. 1981. A structural approach to operational semantics. Tech. rep. DAIMI FN-19, University of Aarhus.
	20	Plotkin, G. 2004. A structural approach to operational semantics. J. Log. Algebr. Program. 60--61, 17--139.
	21	Eugene W. Stark , Scott A. Smolka, A complete axiom system for finite-state probabilistic processes, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
	22	Tini, S. 2003. Rule formats for non-interference. In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 2618. Springer, 129--143.
	23	Tini, S. 2004. Rule formats for compositional non interference properties. J. Log. Algebr. Program. 60--61, 353--400.
	24	Daniele Turi , Gordon Plotkin, Towards a Mathematical Operational Semantics, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.280, June 29-July 02, 1997
	25	Irek Ulidowski , Iain Phillips, Ordered SOS process languages for branching and Eager bisimulation, Information and Computation, v.178 n.1, p.180-213, October 10, 2002 [doi>10.1016/S0890-5401(02)93161-5]
	26	Ulidowski, I. and Yuen, S. 2004. Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation. J. Log. Algebr. Program. 60--61, 401--460.
	27	van Glabbeek, R. J. 2004. The meaning of negative premises in transition system specifications ii. J. Log. Algebr. Program. 60-61, 229--258.
	28	Rob J. VanGlabbeek , Scott A. Smolka , Bernhard Steffen, Reactive, generative, and stratified models of probabilistic processes, Information and Computation, v.121 n.1, p.59-80, Aug. 15, 1995 [doi>10.1006/inco.1995.1123]
	29	Sue-Hwey Wu , Scott A. Smolka , Eugene W. Stark, Composition and behaviors of probabilistic I/O automata, Theoretical Computer Science, v.176 n.1-2, p.1-38, April 20, 1997 [doi>10.1016/S0304-3975(97)00056-X]