Structural operational semantics
A short description of structural operational semantics occurs at the top of
this page.
An overview of work in this area and further references can be found in
- L. Aceto, W.J. Fokkink and C. Verhoef (2001): Structural operational
semantics, in J.A. Bergstra, A. Ponse & S.A. Smolka, eds: Handbook
of Process Algebra, Elsevier, pp. 197-292.
My own contributions to this area are
-
Full Abstraction in Structural Operational Semantics (extended abstract), 1993
This is my first paper proposing congruence formats for several concrete
(= not giving special treatment to the silent action τ)
semantic equivalences. These are syntactic criteria on the transition
rules of the structural operational semantics of a language, ensuring that the
equivalence is a congruence. Moreover, for several formats it is determined
what is the coarsest congruence with respect to all operators in this
format that is finer than partial or completed trace equivalence.
-
On the Expressiveness of ACP (extended abstract), 1994
This paper develops a notion of expressiveness of process
calculi through equivalence-preserving translations.
It shows how all de Simone languages can be expressed in aprACP
(a version of ACP with action prefixing instead of sequential composition),
even when preserving various notions of computability.
-
The Meaning of Negative Premises in Transition System Specifications II, 1995, 2003
This paper reviews several methods to associate transition relations
to transition system specifications with negative premises in
Plotkin's structural operational style. Besides a formal comparison
on generality and relative consistency, the methods are also
evaluated on their taste in determining which specifications are
meaningful and which are not. Additionally, this paper contributes a
proof theoretic characterisation of the well-founded semantics.
- (with W.J. Fokkink)
Ntyft/ntyxt Rules Reduce to Ntree Rules, 1995
Groote and Vaandrager introduced the tyft/tyxt format for Transition
System Specifications (TSSs), and established that for each TSS in
this format that is well-founded, the bisimulation equivalence it
induces is a congruence. In this paper, we construct for each TSS in
tyft/tyxt format an equivalent TSS that consists of tree rules
only. As a corollary we can give an affirmative answer to an open
question, namely whether the well-foundedness condition in the
congruence theorem for tyft/tyxt can be dropped. These results
extend to tyft/tyxt with negative premises and predicates.
- (with B. Bloom & W.J. Fokkink)
Precongruence Formats for Decorated Trace Preorders, 2000
This paper proposes several congruence formats for concrete
semantic equivalences and preorders. The formats are derived using the modal
characterizations of the corresponding preorders.
This method of modal decomposition is used in
the purple-coloured papers below to obtain
congruence formats for concrete semantics, and in
the "divide and congruence" series to
obtain congruence formats for abstract semantics (that give a
special treatment to the hidden action τ).
- (with B. Bloom & W.J. Fokkink)
Precongruence Formats for Decorated Trace Semantics, 2002
Full version of the extended abstract above.
- (with W.J. Fokkink & P. de Wind)
Compositionality of Hennessy-Milner Logic through Structural
Operational Semantics, 2003
The method of modal decomposition is extended to the ntyft/ntyxt format without lookahead.
- (with W.J. Fokkink & P. de Wind)
Compositionality of Hennessy-Milner Logic by Structural Operational
Semantics, 2005
The method of modal decomposition is further extended, also dealing with lookahead.
-
On Cool Congruence Formats for Weak Bisimulations (extended abstract), 2005
-
On Cool Congruence Formats for Weak Bisimulations, 2011
- (with W.J. Fokkink & P. de Wind)
Divide and Congruence: From Decomposition of Modalities to
Preservation of Branching Bisimulation, 2005
- (with W.J. Fokkink & P. de Wind)
Divide and Congruence Applied to η-Bisimulation, 2005
- (with W.J. Fokkink & P. de Wind)
Divide and Congruence: From Decomposition of Modal Formulas
to Preservation of Branching and η-Bisimilarity, 2011
Full version of the two extended abstracts above.
- (with W.J. Fokkink)
Divide and Congruence II: Delay and Weak Bisimilarity, 2016
- (with W.J. Fokkink)
Divide and Congruence II: From Decomposition of Modal Formulas to
Preservation of Delay and Weak Bisimilarity, 2016
Full version of the extended abstract above.
- (with W.J. Fokkink)
Precongruence Formats with Lookahead through Modal Decomposition, 2017
-
Lean and Full Congruence Formats for Recursion, 2017
I establish that bisimilarity is a lean (pre)congruence for recursion
for all languages with a structural operational semantics in the
ntyft/ntyxt format. Additionally, it is a full congruence for the
tyft/tyxt format.
- (with W.J. Fokkink & B. Luttik)
Divide and Congruence III: Stability & Divergence, 2017
- (with W.J. Fokkink & B. Luttik)
Divide and Congruence III: From Decomposition of Modal Formulas to
Preservation of Stability and Divergence, 2017
Full version of the extended abstract above.
-
On the Meaning of Transition System Specifications, 2019
I propose an interpretation of Transition
System Specifications that associates with each operator an
operation on process graphs that is independent of the context in
which it is employed.
- (with P. Höfner & W. Wang)
A Lean-Congruence Format for EP-Bisimilarity, 2023
This paper presents the first congruence
format for a non-interleaving equivalence. It alsdo covers recursion.
In addition, I have edited three collections on Structural Operational
Semantics:
Rob van Glabbeek
rvg@CS.Stanford.EDU