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
2018
2017
2016
2012
2011
Rob van Glabbeek On cool congruence formats for weak bisimulations Theoretical Computer Science, Volume 412, Number 28, pp. 3283–3302, June, 2011 |
2009
Rob van Glabbeek and Peter D. Mosses Preface, special issue on structural operational semantics Information and Computation, pp. 83–84, Elsevier, 2009 |