Completed Research Projects
This page describes the status of my research projects in
mathematics and computer science completed by 1996.
Branching bisimulation
The concept of branching (bisimulation) equivalence was invented by
Peter Weijland and myself as an alternative to Milner's notion of weak
(bisimulation) equivalence, also known as observation equivalence.
Our findings are reported in the paper(s) Branching time and abstraction in bisimulation
semantics, of which the following versions appeared:
- April 1989: an extended abstract
(proceedings 1989 IFIP World Computer Congress),
- May 1990: Chapter III of my Ph.D. Thesis,
- December 1990: A technical report of the TU
München (1990) and CWI (1991),
- 1996 (written end 1993): Chapter III of the second edition of my Ph.D. Thesis,
- 1996: the final version in the JACM.
The first is most suitable as historical reference; the last as
standard reference. The full list of inclusions is 1 in 2 in 3 in 4.
The introduction,
basic definitions,
conclusion and
references of 5 are also available
as hypertext document. The main new results in 4 are listed
here, items 16 to 34.
I'm not able to give a complete list of all papers on branching
bisimulation here; some of the more fundamental ones are discussed in 5.
Besides the above, my own contributions in this area are (included in):
- (with W.P. Weijland) Refinement in
branching time semantics, also included in 2-5 above,
- A complete axiomatization for branching
bisimulation congruence of finite-state behaviours,
- The linear time - branching time
spectrum II; the semantics of sequential processes with silent moves,
- What is branching time and why to
use it?,
- Branching Bisimulation as a Tool in the
Analysis of Weak Bisimulation,
- (with L. Aceto, W.J. Fokkink & A. Ingófsdóttir) Axiomatizating prefix iteration with silent steps,
- Axiomatizating flat iteration,
- Bisimulation,
-
On Cool Congruence Formats for Weak Bisimulations (extended abstract),
-
On Cool Congruence Formats for Weak Bisimulations,
- (with W.J. Fokkink & P. de Wind)
Divide and Congruence: From Decomposition of Modalities to
Preservation of Branching Bisimulation,
- (with W.J. Fokkink & P. de Wind)
Divide and Congruence: From Decomposition of Modal Formulas
to Preservation of Branching and η-Bisimilarity,
- (with W.J. Fokkink & B. Luttik)
Divide and Congruence III: Stability & Divergence,
- (with W.J. Fokkink & B. Luttik)
Divide and Congruence III: From Decomposition of Modal Formulas to
Preservation of Stability and Divergence,
- (with B. Luttik & N. Trčka)
Branching Bisimulation with Explicit Divergence,
- (with B. Luttik & N. Trčka)
Computation Tree Logic with Deadlock Detection,
- (with B. Luttik & L. Spaninks)
Rooted Divergence-Preserving Branching Bisimilarity is a Congruence.
Probabilistic processes
we introduce three models of probabilistic processes, and show how
they form a hierarchy. The former paper is properly included in the latter.
Modular specification
The following two papers by Frits Vaandrager and myself propose and
apply a modular approach to the algebraic specification of process algebras:
Although the second is a substantial revision of the first, it does
not include all its results. The first paper also appears as Chapter
II in my Ph.D. Thesis; its main new
results are listed here, items 6 to
15.
Interpolation
In An interpolation theorem in equational
logic Piet Rodenburg and I show that in a natural formulation,
Craig's interpolation theorem holds for equational logic. We also
discuss the prevalent claims that equational logic does not have the
interpolation property.
Differential topology
My contribution to this area is my master thesis.