Abstract
We propose an SOS transition rule format for the generative model of probabilistic processes. Transition rules are partitioned in several strata, giving rise to an ordering relation analogous to those introduced by Ulidowski and Phillips for classic process algebras. Our rule format guarantees that probabilistic bisimulation is a congruence w.r.t. process algebra operations. Moreover, our rule format guarantees that process algebra operations preserve semistochasticity of processes, i.e. the property that the sum of the probability of the moves of any process is either 0 or 1. Finally, we show that most of operations of the probabilistic process algebras studied in the literature are captured by our format, which, therefore, has practical applications.
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.
Download to read the full chapter text
Chapter PDF
References
Aceto, L., Fokkink, W.J., Verhoef, C.: Structural Operational Semantics. In: Handbook of Process Algebra, pp. 197–292. Elsevier, Amsterdam (2001)
Aldini, A., Bravetti, M., Gorrieri, R.: A Process-algebraic Approach for the Analysis of Probabilistic Non-interference. J. Comput. Secur. 12, 191–245 (2004)
Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing Probabilistic Processes: ACP with Generative Probabilities. Inf. Comput. 121, 234–255 (1995)
Baeten, J.C.M., Verhoef, C.: A Congruence Theorem for Structured Operational Semantics with Predicates. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715. Springer, Heidelberg (1993)
Baier, C., Hermanns, H.: Weak Bisimulation for Fully Probabilistic Processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997)
Bartels, F.: GSOS for Probabilistic Transition Systems. In: Proc. Coalgebraic Methods in Computer Science. ENTCS 65 (2002)
Bloom, B., Istrail, S., Meyer, A.: Bisimulation Can’t Be Traced. J. Assoc. Comput. Mach. 42, 232–268 (1995)
Bravetti, M., Aldini, A.: Discrete Time Generative-reactive Probabilistic Processes with Different Advancing Speeds. Theor. Comput. Sci. 290, 355–406 (2003)
D’Argenio, P.R., Hermanns, H., Katoen, J.P.: On Generative Parallel Composition. In: Proc. Probabilistic Methods in Verification. ENTCS 22 (1999)
Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic Reasoning for Probabilistic Concurrent Systems. In: IFIP Work. Conf. on Progr., Concepts and Methods (1990)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, Generative and Stratified Models of Probabilistic Processes. Inf. Comput. 121, 59–80 (1995)
Groote, J.F., Vaandrager, F.: Structured Operational Semantics and Bisimulation as a Congruence. Inf. Comput. 100, 202–260 (1992)
Jonsson, B., Larsen, K.L., Yi, W.: Probabilistic Extensions of Process Algebras. In: Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Plotkin, G.: A Structural Approach to Operational Semantics. Technical report DAIMI FN-19, University of Aarhus (1981)
Plotkin, G.: A Structural Approach to Operational Semantics. J. Log. Algebr. Program., 60–61, 17–139 (2004)
de Simone, R.: Higher-level Synchronizing Devices in Meije-SCCS. Theor. Comput. Sci. 37, 245–267 (1985)
Tini, S.: Rule Formats for Non-Interference. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 129–143. Springer, Heidelberg (2003)
Tini, S.: Rule Formats for Compositional non Interference Properties. J. Log. Algebr. Program., 60–61, 353–400 (2004)
Ulidowski, I., Phillips, I.: Ordered SOS Process Languages for Branching and Eager Bisimulations. Inf. Comput. 178, 180–213 (2002)
Verhoef, C.: A Congruence Theorem for Structural Operational Semantics with Predicates and Negative Premises. Nord. J. Comput. 2, 274–302 (1995)
Wu, S.H., Smolka, S.A., Stark, E.W.: Composition and Behaviors of Probabilistic I/O Automata. Theor. Comput. Sci. 176, 1–38 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lanotte, R., Tini, S. (2005). Probabilistic Congruence for Semistochastic Generative Processes. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)