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
|
Publications
2019
|
 |
Wan Fokkink, Rob van Glabbeek and Bas Luttik Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence Information and Computation, Volume 268, October, 2019 |
|
|
|
Rob van Glabbeek On the meaning of transition system specifications Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics, pp. 69–85, Amsterdam, The Netherlands, August, 2019 |
2018
|
|
|
Rob van Glabbeek, Peter Hoefner and Djurre van der Wal Analysing AWN-specifications using mCRL2 (extended abstract) 14th International Conference on integrated Formal Methods, pp. 398-418, Maynooth, September, 2018 |
2017
|
|
|
Rob van Glabbeek and Wan Fokkink Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity Information and Computation, Volume 257, pp. 79-113, December, 2017 |
|
|
|
Wan Fokkink, Rob van Glabbeek and Bas Luttik Divide and congruence III: Stability & divergence International Conference on Concurrency Theory (CONCUR), pp. 15:1-15:16, Berlin, Germany, September, 2017 |
|
|
|
Wan Fokkink and Rob van Glabbeek Precongruence formats with lookahead through modal decomposition 26th EACSL Annual Conference on Computer Science Logic (CSL'17), Stockholm, Sweden, August, 2017 |
|
|
|
Rob van Glabbeek Lean and full congruence formats for recursion Annual IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, August, 2017 |
2016
|
|
|
Wan Fokkink and Rob van Glabbeek Divide and congruence II: delay and weak bisimilarity Annual IEEE Symposium on Logic in Computer Science, pp. 778–787, New York City, USA, July, 2016 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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, Volume 214, Number , pp. 59–85, May, 2012 |