×

Structural operational semantics for stochastic and weighted transition systems. (English) Zbl 1358.68214

Summary: We introduce weighted GSOS, a general syntactic framework to specify well-behaved transition systems where transitions are equipped with weights coming from a commutative monoid. We prove that weighted bisimilarity is a congruence on systems defined by weighted GSOS specifications. We illustrate the flexibility of the framework by instantiating it to handle some special cases, most notably that of stochastic transition systems. Through examples we provide weighted-GSOS definitions for common stochastic operators in the literature.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto, L.; Fokkink, W. J.; Verhoef, C., Structural operational semantics, (Bergstra, J. A.; Ponse, A.; Smolka, S., Handbook of Process Algebra (2002), Elsevier), 197-292 · Zbl 1062.68074
[2] Barr, M., Terminal coalgebras in well-founded set theory, Theoretical Computer Science, 114, 299-315 (1993) · Zbl 0779.18004
[3] Bartels, F., On generalised coinduction and probabilistic specification formats (2004), CWI: CWI Amsterdam, PhD dissertation
[4] Bernardo, M.; Gorrieri, R., A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time, Theoretical Computer Science, 202, 1-2, 1-54 (1998) · Zbl 0902.68075
[5] Bloom, B.; Istrail, S.; Meyer, A., Bisimulation canʼt be traced, Journal of the ACM, 42, 232-268 (1995) · Zbl 0886.68027
[6] Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, Journal of the ACM, 31, 560-599 (1995) · Zbl 0628.68025
[7] Cardelli, L.; Mardare, R., The measurable space of stochastic processes, (Procs. QESTʼ10 (2010), IEEE Computer Society), 171-180
[8] de Nicola, Rocco; Latella, Diego; Loreti, Michele; Massink, Mieke, Rate-based transition systems for stochastic process calculi, (Procs. ICALPʼ09. Procs. ICALPʼ09, Lecture Notes in Computer Science, vol. 5556 (2009), Springer) · Zbl 1248.68350
[9] de Vink, E. P.; Rutten, J. J.M. M., Bisimulation for probabilistic transition systems: A coalgebraic approach, Theoretical Computer Science, 221, 1-2, 271-293 (1999) · Zbl 0930.68092
[10] Degano, P.; Priami, C., Enhanced operational semantics, ACM Computational Surveys, 28, 2, 352-354 (1996)
[11] Götz, N.; Herzog, U.; Rettelbach, M., Multiprocessor and distributed system design: The integration of functional specification and performance analysis using stochastic process algebras, (Performance/SIGMETRICS Tutorials (1993)), 121-146
[12] Hermanns, H.; Herzog, U.; Katoen, J.-P., Process algebra for performance evaluation, Theoretical Computer Science, 274, 1-2, 43-87 (2002) · Zbl 0992.68149
[13] Hillston, J., On the nature of synchronisation, (Procs. PAPMʼ94 (1994)), 51-70
[14] Hillston, J., A Compositional Approach to Performance Modelling (1996), Cambridge University Press
[15] Hillston, J., Process algebras for quantitative analysis, (Procs. LiCSʼ05 (2005), IEEE Computer Society Press), 239-248
[16] Klin, B., Structural operational semantics for weighted transition systems, (Semantics and Algebraic Specification. Semantics and Algebraic Specification, Lecture Notes in Computer Science, vol. 5700 (2009), Springer), 121-139 · Zbl 1253.68214
[17] Klin, B., Bialgebras for structural operational semantics: An introduction, Theoretical Computer Science, 412, 38, 5043-5069 (2011) · Zbl 1246.68150
[18] Klin, B.; Sassone, V., Structural operational semantic for stochastic systems, (Proc. FOSSACSʼ08. Proc. FOSSACSʼ08, Lecture Notes in Computer Science, vol. 4962 (2008)), 428-442 · Zbl 1138.68468
[19] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Information and Computation, 94, 1-28 (1991) · Zbl 0756.68035
[20] Mac Lane, S., Categories for the Working Mathematician (1998), Springer · Zbl 0906.18001
[21] Milner, R., Communication and Concurrency (1988), Prentice Hall
[22] Moller, F.; Tofts, C., A temporal calculus of communicating systems, (Proc. CONCURʼ90. Proc. CONCURʼ90, Lecture Notes in Computer Science, vol. 458 (1990)), 401-415
[23] Park, D. M., Concurrency and Automata on Infinite Sequences, Lecture Notes in Computer Science, vol. 140, 195-219 (1981)
[24] Plotkin, G. D., A structural approach to operational semantics (1981), Computer Science Department, Aarhus University, DAIMI Report FN-19
[25] Plotkin, G. D., A structural approach to operational semantics, Journal of Logic and Algebraic Programming, 60-61, 17-139 (2004) · Zbl 1082.68062
[26] Priami, C., Stochastic \(π\)-calculus, Computer Journal, 38, 7, 578-589 (1995)
[27] Priami, C., Language-based performance prediction for distributed and mobile systems, Information and Computation, 175, 2, 119-145 (2002) · Zbl 1012.68115
[28] Priami, C.; Regev, A.; Shapiro, E. Y.; Silverman, W., Application of a stochastic name-passing calculus to representation and simulation of molecular processes, Information Processing Letters, 80, 1, 25-31 (2001) · Zbl 0997.92018
[29] Rutten, J. J.M. M., Universal coalgebra: a theory of systems, Theoretical Computer Science, 249, 3-80 (2000) · Zbl 0951.68038
[30] Sangiorgi, D.; Walker, D., The \(π\)-Calculus: a Theory of Mobile Processes (2003), Cambridge University Press
[31] Turi, D.; Plotkin, G. D., Towards a mathematical operational semantics, (Proc. LICSʼ97 (1997), IEEE Computer Society Press), 280-291
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.