Cited By
View all- Goncharov SMilius SSchröder LTsampas SUrbat H(2023)Towards a Higher-Order Mathematical Operational SemanticsProceedings of the ACM on Programming Languages10.1145/35712157:POPL(632-658)Online publication date: 9-Jan-2023
Structural operational semantics for non-deterministic processes with quantitative aspects
Pages 135 - 154
Abstract
Recently, unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions) have been proposed with the aim of providing general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function GSOS (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and GSOS formats (e.g. GSOS, Weighted GSOS, Segala-GSOS).The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.
References
[1]
P. Aczel, N. Mendler, A final coalgebra theorem, in: LNCS Science, vol. 389, Springer, 1989, pp. 357-365.
[2]
G. Bacci, M. Miculan, Structural operational semantics for continuous state stochastic transition systems, J. Comput. System Sci., 81 (2015) 834-858.
[3]
M. Barr, Terminal coalgebras in well-founded set theory, Theoret. Comput. Sci., 114 (1993) 299-315.
[4]
F. Bartels, On generalised coinduction and probabilistic specification formats, CWI, Amsterdam, 2004.
[5]
M. Bernardo, R. De Nicola, M. Loreti, A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Inform. and Comput., 225 (2013) 29-82.
[6]
M. Bernardo, R. Gorrieri, A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time, Theoret. Comput. Sci., 202 (1998) 1-54.
[7]
B. Bloom, S. Istrail, A.R. Meyer, Bisimulation can't be traced, J. ACM, 42 (1995) 232-268.
[8]
F. Bonchi, S. Milius, A. Silva, F. Zanasi, Killing epsilons with a dagger: a coalgebraic study of systems with algebraic label structure, Theoret. Comput. Sci., 604 (2015) 102-126.
[9]
T. Brengos, M. Miculan, M. Peressotti, Behavioural equivalences for coalgebras with unobservable moves, J. Log. Algebraic Methods Program., 84 (2015) 826-852.
[10]
L. Cardelli, R. Mardare, The measurable space of stochastic processes, in: Proc. QEST, IEEE Computer Society, 2010, pp. 171-180.
[11]
M. David Lee, D. Gebler, P.R. D'Argenio, Tree rules in probabilistic transition system specifications with negative and quantitative premises, in: EPTCS, vol. 89, 2012, pp. 115-130.
[12]
R. De Nicola, D. Latella, M. Loreti, M. Massink, A uniform definition of stochastic process calculi, J. ACM, 46 (2013) 5.
[13]
M. Droste, W. Kuich, H. Vogler, Handbook of Weighted Automata, Springer, 2009.
[14]
H.P. Gumm, T. Schröder, Monoid-labeled transition systems, Electron. Notes Theor. Comput. Sci., 44 (2001) 185-204.
[15]
J. Hillston, A Compositional Approach to Performance Modelling, Cambridge University Press, 1996.
[16]
J. Hillston, Process algebras for quantitative analysis, in: LICS, IEEE Computer Society, 2005, pp. 239-248.
[17]
B. Klin, Bialgebraic methods and modal logic in structural operational semantics, Inform. and Comput., 207 (2009) 237-257.
[18]
B. Klin, Bialgebras for structural operational semantics: an introduction, Theoret. Comput. Sci., 412 (2011) 5043-5069.
[19]
B. Klin, B. Nachyla, Distributive laws and decidable properties of SOS specifications, in: EPTCS, vol. 160, 2014, pp. 79-93.
[20]
B. Klin, V. Sassone, Structural operational semantics for stochastic and weighted transition systems, Inform. and Comput., 227 (2013) 58-83.
[21]
K.G. Larsen, A. Skou, Bisimulation through probabilistic testing, Inform. and Comput., 94 (1991) 1-28.
[22]
D. Latella, M. Massink, E.P. de Vink, A definition scheme for quantitative bisimulation, in: Proc. QAPL, 2015.
[23]
M. Miculan, M. Peressotti, Weak bisimulations for labelled transition systems weighted over semirings, CoRR (2013). arXiv:1310.4106 abs
[24]
M. Miculan, M. Peressotti, GSOS for non-deterministic processes with quantitative aspects, in: EPCTS, vol. 154, 2014, pp. 17-33.
[25]
C. Priami, Stochastic pi-calculus, Comput. J., 38 (1995) 578-589.
[26]
J.J.M.M. Rutten, Universal coalgebra: a theory of systems, Theoret. Comput. Sci., 249 (2000) 3-80.
[27]
R. Segala, N.A. Lynch, Probabilistic simulations for probabilistic processes, Nordic J. Comput., 2 (1995) 250-273.
[28]
S. Staton, Relating coalgebraic notions of bisimulation, Log. Methods Comput. Sci., 7 (2011).
[29]
D. Turi, G. Plotkin, Towards a mathematical operational semantics, in: Proc. LICS, IEEE Computer Society Press, 1997, pp. 280-291.
- Structural operational semantics for non-deterministic processes with quantitative aspects
Recommendations
Structural operational semantics for continuous state stochastic transition systems
In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endofunctors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule ...
Bialgebraic methods and modal logic in structural operational semantics
Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of ...
Bialgebraic Methods in Structural Operational Semantics
Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational specifications. An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V.
Publisher
Elsevier Science Publishers Ltd.
United Kingdom
Publication History
Published: 06 December 2016
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 Dec 2024
Other Metrics
Citations
Cited By
View all- Goncharov SMilius SSchröder LTsampas SUrbat H(2023)Towards a Higher-Order Mathematical Operational SemanticsProceedings of the ACM on Programming Languages10.1145/35712157:POPL(632-658)Online publication date: 9-Jan-2023
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in