Structural Operational Semantics (SOS) Meta-Theory: A 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: m.r.mousavi atsign tue dot nl.

• Introductory and General Survey Texts:

  • SOS Pioneers: (not necessarily about the meta-theory)

    • 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

    • Congruence for 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. .pdf
      • W.J. Fokkink. Rooted branching bisimulation as a congruence. Journal of Computer and System Science, 60(1):13-37, 2000. .pdf
      
      
      

    • 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. .pdf
      • B. Bloom. Can LCF be Topped? Flat Lattice Models of Typed lambda-Calculus. Information and Computation, 87(1/2): 263-300, 1990.
      
      
      

    • Other Notions of Behavioral Equivalence (Pre-order)

      • 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). Pre-print in .pdf format.
      • Probabilistic Bisimilarity
        • 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. .pdf
      • Testing Pre-order
      • Should Testing 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-�, 1994. .ps
  • J.C.M. Baeten and E.P. de Vink. Axiomatizing GSOS with termination. Journal of Logic and Algebraic Programming, 60-61:323-351, 2004. .ps
  • L. Aceto. Deriving complete inference systems for a class of GSOS languages generating regular behaviours. In B. Jonsson and J. Parrow, editors, Proceedings of the 5th International Conference on Concurrency Theory (CONCUR'94), volume 836 of LNCS, pages 449-464. Springer, 1994. Tech. Rep. version: .ps.Z
  
  
  

  • Axioms for Other Notions of Bisimilarity

  • 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 (ICTAC'05), volume 3722 of LNCS, pp. 331-346. Springer, 2005. .pdf
  • Testing Pre-order I. Ulidowski. Finite Axiom Systems for Testing Preorder and De Simone Process Languages. Theoretical Computer Science, 239(1), pp 97-139, 2000. .ps.gz
  • Refusal Simulation I. Ulidowski. Equivalences on observable processes. Proceedings of the 7th IEEE Symposium on Logic in Computer Science (LICS'92), pages 148-159, IEEE Computer Society, 1992. .ps
  
  
  

  • Rewrite Theories

  • I. Ulidowski. Priority Rewrite Systems for OSOS Process Languages. In R. Amadio and D. Lugiez, editors, Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), volume 2761 of LNCS, pp. 87-102. Springer, 2003. .ps
  
  
  

• Ordered SOS

  • M.R. Mousavi, I.C.C. Phillips, M.A. Reniers, I. Ulidowski. Semantics and Expressiveness of Ordered SOS. Information and Computation, 2008. To appear. Preprint in .pdf Preliminary version appeared in the Proceedings of FSTTCS'06.
  • I. Ulidowski and I.C.C. Phillips. Ordered SOS rules and process languages for branching and eager bisimulations. Information and Computation, 178(1):180-213, 2002. .ps
  
  
  

• Time

  • I.Ulidowski and S.Yuen. Process languages with discrete time based on the Ordered SOS format and rooted eager bisimulation. Journal of Logic and Algebraic Programming, 60-61:401-461, 2004.
  • M. Kick. Coalgebraic Modelling of Timed Processes. Ph.D. Thesis, LFCS, School of Informatics, University of Edinburgh, 2002. .pdf
  
  
  

• Stochastics and Probability

  • B. Klin and V. Sassone. Structural operational semantics for stochastic process calculi, Proceeding of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'08). Pre-print in .pdf format.
  • F. Bartels. GSOS for probabilistic transition systems. Proceedings of the 5th International Workshop on Coalgebraic Methods in Computer Science (CMCS'02), volume 65 of ENTCS, pages 1-25, 2002. .pdf
  • R. Lanotte and S. Tini. Probabilistic congruence for semistochastic generative processes. In Vladimiro Sassone, editor, Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'05), volume 3441 of LNCS, pages 63-78. Springer, 2005.
  
  
  

• Security

  • Simone Tini Rule Formats for Compositional Non Interference Properties, JLAP, 60-61(3):353-400, Elsevier, 2004. Preliminary version appeared in the Proceedings of ESOP'03.

• Reasoning

  • W.J. Fokkink, R.J. van Glabbeek and P. de Wind. Compositionality of {Hennessy-Milner} logic by structural operational semantics. Theoretical Computer Science, 354(3):421-440, 2006..pdf
  • A. Simpson. Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS. Journal of Logic and Algebraic Programming, 60-61:287-322, 2004. .pdf
  • K.G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. Journal of Logic and Computation, 1(6):761-795, 1991.
  
  
  

• Implementation

  • M.R. Mousavi and M.A. Reniers. Prototyping SOS Meta-theory in Maude. In P.D. Mosses and I. Ulidowski, editors, Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS'05), ENTCS, 156(1), Elservier Science, 2006. .pdf
  • A. Verdejo and N. Marti-Oliet. Two Case Studies of Semantics Execution in Maude: CCS and LOTOS. Formal Methods in System Design 27(1-2):113-172, 2005.
  • C. de O. Braga, E. H. Haeusler, J. Meseguer, and P. D. Mosses. Mapping modular {SOS} to rewriting logic. In Michael Leuschel, editor, Proceedings of the 12th International Workshop on Logic Based Program Synthesis and Transformation (LOPSTR'02), volume 2664 of LNCS, pages 262-277. Springer, 2002.
  • P. Borras, D. Clement, T. Despeyroux, J. Incerpi, G. Kahn, B. vLang, and V. Pascual. CENTAUR: The system. SIGPLAN Notices, 24(2):14-24, 1988. Centaur can be downloaded from here.
  • Pieter H. Hartel. LETOS - a lightweight execution tool for operational semantics. Software, Practice and Experience, 29(15):1379-1416, 1999.

Back to Publications

Back to Home