A rule that specifies a labelled transition system over a (first-order) term/process language is a GSOS rule whenever it is of the form
where
Turi and Plotkin [1997] discovered that a set of GSOS rules can be reformulated as a GSOS law, i.e. a natural transformation
where
A tutorial introduction to this correspondence is given by Klin [2011].
Bloom, Bard, Sorin Istrail, and Albert R. Meyer. 1995. ‘Bisimulation Can’t Be Traced’. Journal of the ACM 42 (1): 232–68. https://doi.org/10.1145/200836.200876.
@article{bloom_bisimulation_1995,
title = {Bisimulation can't be traced},
volume = {42},
doi = {10.1145/200836.200876},
number = {1},
journal = {Journal of the ACM},
author = {Bloom, Bard and Istrail, Sorin and Meyer, Albert R.},
year = {1995},
pages = {232--268}
}
Klin, Bartek. 2011. ‘Bialgebras for Structural Operational Semantics: An Introduction’. Theoretical Computer Science 412 (38): 5043–69. https://doi.org/10.1016/j.tcs.2011.03.023. [pdf]
@article{klin_bialgebras_2011,
title = {Bialgebras for structural operational semantics: {An} introduction},
volume = {412},
doi = {10.1016/j.tcs.2011.03.023},
number = {38},
journal = {Theoretical Computer Science},
author = {Klin, Bartek},
year = {2011},
pages = {5043--5069}
}
Turi, D., and G. Plotkin. 1997. ‘Towards a Mathematical Operational Semantics’. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 280–91. Warsaw, Poland: IEEE Comput. Soc. https://doi.org/10.1109/LICS.1997.614955. [pdf]
@inproceedings{turi_towards_1997,
address = {Warsaw, Poland},
title = {Towards a mathematical operational semantics},
doi = {10.1109/LICS.1997.614955},
booktitle = {Proceedings of {Twelfth} {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {IEEE Comput. Soc},
author = {Turi, D. and Plotkin, G.},
year = {1997},
pages = {280--291}
}