Research in Structural Operational Semantics

From CERES
Jump to: navigation, search

Subject Area

Structural Operational Semantics (SOS) was introduced by Gordon Plotkin as a logical means to defining operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax oriented, view on operational semantics. Thanks to its intuitive look and easy to follow structure, SOS has gained great popularity and has become a de facto standard in defining formal semantics for programming and language constructs.

This enormous popularity and vast application of SOS has called (and still calls) for more theoretical work. Many researchers have responded to this call and have spent huge effort on laying firm mathematical foundations for different aspects of SOS. Our research effort in this area focuses on establishing a firm theoretical framework for defining SOS specifications and efficiently reasoning about them.

Selected Publications

  • D. Gebler, E.-I. Goriac, and M.R. Mousavi. Algebraic Meta-Theory of Processes with Data. Proceedings of the Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics (EXPRESS/SOS 2013), Buenos Aires, Argentina, Electronic Proceedings in Theoretical Computer Science, 2013.
  • L. Aceto, A. Ingolfsdottir, M.R. Mousavi and M.A. Reniers. Algebraic Properties for Free!, Bulletin of the European Association for Theoretical Computer Science (BEATCS), 99:81--104, October 2009.

Bibliography

In February 2006, we concluded a literature survey of the field of SOS meta-theory. In order to make the surveyed bibliography accessible and improve the results (through receiving comments from the people involved in this field), we decided to compose this web-page. A pre-print of our survey can be downloaded from here. The paper is also available via Science Direct (subscription required). Your comments and remarks (of any kind) are highly appreciated. Please send your comments to me (at [1]).

Introductory and General Survey Texts

SOS Pioneers

  • G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981. Also published in: Journal of Logic and Algebraic Programming, 60-61:17-140, 2004. (Preliminary version in .ps format; the JLAP version is proofread and improved)
  • Matthew Hennessy and Gordon D. Plotkin. Full abstraction for a simple parallel programming language. Proceedings of MFCS'79, volume 74 of LNCS, pages 108-120. Springer, 1979.
  • Gordon D. Plotkin. An operational semantics for CSO. Proceedings of the Conference on Logic of Programs and Their Applications, volume 148 of LNCS, pages 250-252. Springer, 1983.
  • G. Kahn, Natural Semantics, Proceedings of STACS'87, volume 247 of Lecture Notes in Computer Science, pages 22-39, Springer, 1987.
  • G.D. Plotkin. The origins of structural operational semantics. Journal of Logic and Algebraic Programming (JLAP), 60:3-15, 2004. .pdf


Surveys of SOS Meta Theory

  • M.R. Mousavi, M. A. Reniers, J.F. Groote. SOS Formats and Meta-Theory: 20 Years After. Theoretical Computer Science, 373:238-272, 2007. Preprint in .pdf. Preliminary version appeared as: A Hierarchy of SOS Rule Formats, Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS'05), Electronic Notes in Theoretical Computer Science, 156(1), Elsevier, 2006.
  • L. Aceto, W.J. Fokkink, and C. Verhoef. Structural operational semantics. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, Chapter 3, pages 197-292. Elsevier Science, 2001. .pdf


Semantics of TSS's (with Negative Premises)

  • R.J. van Glabbeek. The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming, 60-61:229-258, 2004. .pdf
  • R.N. Bol and J.F. Groote. The meaning of negative premises in transition system specifications. Journal of the ACM, 43(5):863-914, 1996.
  • J.F. Groote. Transition system specifications with negative premises. Theoretical Computer Science, 118(2):263-299, 1993.


(Pre-)Congruence Formats

Strong Bisimilarity

  • M.R. Mousavi, M.J. Gabbay, and M.A. Reniers. SOS for higher order processes. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of LNCS, pp. 308-322. Springer, 2005. .pdf
  • C.A. Middelburg. Variable binding operators in transition system specifications. Journal of Logic and Algebraic Programming}, 47(1):15-45, 2001. .ps.gz
  • K.L. Bernstein. A congruence theorem for structured operational semantics of higher-order languages. In IEEE Symposium on Logic In Computer Science (LICS'98), pages 153--164. IEEE Computer Society, 1998.
  • C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. Nordic Journal of Computing, 2(2):274--302, 1995. .ps
  • W.J. Fokkink and R.J. van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126(1):1--10, 1996. .pdf
  • J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202--260, 1992.
  • B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232--268, 1995.
  • R. de Simone. Higher-level synchronizing devices in MEIJE-SCCS. Theoretical Computer Science}, 37:245--267, 1985.


Weak Bisimilarities

  • R.J. van Glabbeek. On cool congruence formats for weak bisimulations (extended abstract). In D.V. Hung and M. Wirsing, editors, Proceedings International Colloquium on Theoretical Aspects of Computing (ICTAC05), volume 3722 of LNCS, pp. 331-346. Springer, 2005.
  • W.J. Fokkink. Rooted branching bisimulation as a congruence. Journal of Computer and System Science, 60(1):13-37, 2000.


Applicative Bisimilarity

  • D.J. Howe. Proving Congruence of Bisimulation in Functional Programming Languages. Information and Computation, 124(2):103-112, 1996.
  • D. Sands. From SOS rules to proof principles: An operational metatheory for functional languages. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL'97), pp. 428-441, ACM Press, 1997.
  • B. Bloom. Can LCF be Topped? Flat Lattice Models of Typed lambda-Calculus. Information and Computation, 87(1/2): 263-300, 1990.



Probabilistic and Stochastic Bisimilarity

  • Bartek Klin and Vladimiro Sassone. Structural operational semantics for stochastic process calculi, Proceeding of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'08).
  • Falk Bartels. On Generalised Coinduction and Probabilistic Specification Formats. PhD thesis, VU University Amsterdam, 2004.
  • Ruggero Lanotte and Simone Tini. Probabilistic bisimulation as a congruence. ACM TOCL, 10:1-48, 2009.
  • Simone Tini. Non-expansive epsilon-bisimulations for probabilistic pro- cesses. Theor. Comput. Sci., 411:2202-2222, 2010.
  • Matias David Lee, Daniel Gebler, and Pedro R. D'Argenio. Tree rules in probabilistic transition system specifications with negative and quantitative premises. In Bas Luttik and Michel A. Reniers, editors, Proc. EXPRESS/SOS'12, volume 89 of EPTCS, pages 115--130. Open Publishing Association, 2012.

Decorated Traces Pre-orders

Readiness, ready traces, failure pre-orders:

  • B. Bloom, W.J. Fokkink, and R.J. van Glabbeek. Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic, 5(1):26-78, 2004.

Testing Pre-orders

  • Xiaowei Huang, Li Jiao and Weiming Lu. A precongruence format for should testing preorder, Theoretical Computer Science, Journal of Logic and Algebraic Programming, 79(3-5):245-263, 2010.
  • I. Ulidowski, Finite Axiom Systems for Testing Preorder and De Simone Process Languages. Theoretical Computer Science, 239(1), pp 97-139, 2000. .ps.gz

Open Bisimilarity

  • A. Ziegler, D. Miller, and C. Palamidessi. A Congruence Format for Name-Passing Calculi. In P.D. Mosses and I. Ulidowski, editors, Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS'05), Electronic Notes in Computer Science. 156(1), Elsevier, 2006. .pdf
  • Quasi-Open Bisimilarity M. Fiore S. Staton. A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics. In Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS'06), IEEE CS, 2006.
  • Higher-Order Bisimilarity M.R. Mousavi, M.J. Gabbay, and M.A. Reniers. SOS for higher order processes. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of LNCS, pp. 308-322. Springer, 2005. .pdf
  • Bisimilarities with Data M.R. Mousavi, M.A. Reniers, J.F. Groote. Notions of Bisimulation and Congruence Formats for SOS with Data, Information and Computation (I&C), 200(1):107--147, Elsevier, 2005.

Completed Trace Equivalence B. Klin. From Bialgebraic Semantics to Congruence Formats. In L. Aceto, W.J. Fokkink and I. Ulidowski, editors, Proceedings of the 1st Workshop on Structural Operational Semantics (SOS'04), volume 128 of ENTCS, pages 3-37, Elsevier, 2005. .pdf


Conservativeness

  • W.J. Fokkink and C. Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24-54, 1998. .pdf
  • C.A. Middelburg. An alternative formulation of operational conservativity with binding terms. Journal of Logic and Algebraic Programming, 55(1/2):1--19, 2003. .ps.gz
  • M.R. Mousavi, M.A. Reniers, Orthogonal Extensions in Structural Operational Semantics, Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), volume 3580 of Lecture Notes in Computer Science, pp. 1214-1225, Springer, 2005. .pdf
  • Pedro R. D'Argenio, C. Verhoef: A General Conservative Extension Theorem in Process Algebras with Inequalities. Theoretical Computer Science 177(2): 351-380, 1997. .pdf


Generating Equational Theories and Rewrite Systems

Axioms for Strong Bisimilarity

  • L. Aceto, A. Ingolfsdottir, M.R. Mousavi and M.A. Reniers. Algebraic Properties for Free!, Bulletin of the European Association for Theoretical Computer Science (BEATCS), 99:81--104, October 2009. .pdf
  • L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into equations. Information and Computation, 111:1-„1¤7, 1994. .ps
  • J.C.M. Baeten and E.P. de Vink. Axiomatizing GSOS with termination.

Contact

Mohammad Mousavi, Professor of Computer Systems Engineering

Retrieved from "https://wiki.hh.se/ceres/index.php?title=Research_in_Structural_Operational_Semantics&oldid=2879"