Skip to main content

Structural Operational Semantics

Structural Operational Semantics

  • Aim: Ensuring proper behaviour through syntactic requirements in operational specifications of processes.
  • Context: Structural operational semantics (SOS) provides a framework for giving operational semantics to programming and specification languages. A growing number of programming languages from commercial and academic spheres have been given usable semantic descriptions by means of structural operational semantics. Because of its intuitive appeal and flexibility, structural operational semantics has found considerable application in the study of the semantics of concurrent processes. Moreover, it is becoming a viable alternative to denotational semantics in the static analysis of programs, and in proving compiler correctness.
           Recently, structural operational semantics has been successfully applied as a formal tool to establish results that hold for classes of process description languages. This has allowed for the generalisation of well-known results in the field of process algebra, and for the development of a meta-theory for process calculi based on the realization that many of the results in this field only depend upon general semantic properties of language constructs.
           Compositionality is a crucial requirement for the efficient analysis of concurrent systems and the verification of their properties. It allows derivation of properties of a composite system from suitable properties verified for each of the components. This is one of the most successful tools in combatting the state space problem in verification. In the context of process algebras, compositionality is achieved by ensuring that a relevant semantic equivalence or refinement preorder between processes is a congruence (or precongruence).
  • Approach: This project aims at finding syntactic criteria on the structural operational specification of system description languages or process algebras, that guarantee compositionality. We aim to do this for a wide range of suitable semantic equivalences and preorders.
  • Collaboration: VU Amsterdam

People

Current

Past

  • Matthew Hennessy
  • Paulien de Wind

Publications

2017

Abstract to be published Wan Fokkink, Rob van Glabbeek and Bas Luttik
Divide and congruence III: Stability & divergence
28th International Conference on Concurrency Theory (CONCUR'17), pp. 15:1-15:16, Berlin, Germany, September, 2017
Abstract PDF Rob van Glabbeek
Lean and full congruence formats for recursion
Proceedings 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, June, 2017

2016

Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: delay and weak bisimilarity
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 778–787, New York City, USA, July, 2016
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing (extended abstract)
European Symposium on Programming, pp. 95–122, Eindhoven, The Netherlands, April, 2016
Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
Technical Report 9351, NICTA, April, 2016
Abstract PDF Emile Bres, Rob van Glabbeek and Peter Hoefner
A timed process algebra for wireless networks with an application in routing
Technical Report, NICTA, February, 2016

2012

Abstract PDF Wan Fokkink, Rob van Glabbeek and Paulien de Wind
Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity
Information and Computation (I&C), Volume 214, Number , pp. 59–85, May, 2012

2011

Abstract PDF Rob van Glabbeek
On cool congruence formats for weak bisimulations
Theoretical Computer Science, Volume 412, Number 28, pp. 3283–3302, June, 2011

2009

Abstract PDF Rob van Glabbeek and Peter D. Mosses
Preface, special issue on structural operational semantics
Information and Computation, pp. 83–84, Elsevier, 2009

2007

Abstract PDF Rob van Glabbeek and Matthew Hennessy
Preface, proceedings of the 4th workshop on structural operational semantics
Electronic Notes in Theoretical Computer Science, pp. 1–3, Elsevier, 2007
Abstract PDF Rob van Glabbeek and Peter D. Mosses
Preface, proceedings of the 3rd workshop on structural operational semantics
Electronic Notes in Theoretical Computer Science, pp. 1–2, Elsevier, 2007

Contact

Rob van Glabbeek, Robert.vanGlabbeek <at> data61.csiro.au
Served by Apache on Linux on seL4.