Abstracts

The following is a list of abstracts of and references to my papers, followed by addresses where they can be ordered.

0. Good Coverings

R.J. van Glabbeek (U. Leiden)

February 1985

In the cohomology theory of differentiable manifolds, e.g. in the proof of the De Rham-theorem and the treatment of Poincaré-duality, it is used that every open covering of a paracompact differentiable manifold has a refinement with the property that every non-empty intersection of a finite collection of its open sets is diffeomorphic with an open ball. A covering with this property is called "good". The existence of such good refinements is usually proved by referring to some theorems in differential geometry, which are out of the scope of cohomology theory. The aim of this paper is to show how to obtain good coverings in an elementary way, without using differential geometry.

Keywords: Cohomology, differentiable manifolds, open coverings, convexity, diffeomorphism.

1. Notes on the methodology of CCS and CSP

R.J. van Glabbeek (CWI)

August 1986

In this paper the methodology of some theories of concurrency (mainly CCS and CSP) is analysed, focusing on the following topics: the representation of processes, the identification issue, and the treatment of nondeterminism, communication, recursion, abstraction, divergence and deadlock behaviour. Process algebra turns out to be a useful instrument for comparing the various theories.

Keywords: Concurrency, process algebra, CCS, CSP, semantic equivalences

2. Bounded nondeterminism and the approximation induction principle in process algebra

R.J. van Glabbeek (CWI)

September 1986

This paper presents a new semantics of ACP_tau, the Algebra of Communicating Processes with abstraction. This leads to a term model of ACP_tau which is isomorphic [see erratum] to the model of process graphs modulo rooted tau-delta-bisimulation of Baeten, Bergstra & Klop [TCS 51], but in which no special rootedness condition is needed. Bisimilarity turns out to be a congruence in a natural way.
In this model, the Recursive Definition Principle (RDP), the Commutativity of Abstraction (CA) and Koomen's Fair Abstraction Rule (KFAR) are satisfied, but the Approximation Induction Principle (AIP) is not. The combination of these four principles is proven to be inconsistent, while any combination of three of them is not.
In [TCS 51] a restricted version of AIP is proved valid in the graph model. This paper proposes a simpler and less restrictive version of AIP, not containing guarded recursive specifications as a parameter, which is still valid. This infinitary rule is formulated with the help of a family B_n of unary predicates, expressing bounded nondeterminism.

Keywords: Concurrency, process algebra, ACP, Approximation Induction Principle, Recursion, Abstraction, Fairness, Liveness, Consistency, Bisimulation, Bounded Nondeterminism

3. Another look at abstraction in process algebra

J.C.M. Baeten (U. Amsterdam) & R.J. van Glabbeek (CWI)

January 1987

Central to theories of concurrency is the notion of abstraction. Abstraction from internal actions is the most important tool for system verification.
In this paper, we look at abstraction in the framework of the Algebra of Communicating Processes (ACP) of Bergstra & Klop. We introduce a hidden step eta, and construct a model for the resulting theory ACP_eta. We briefly look at recursive specifications, fairness and protocol verification in this theory, and discuss the relations with Milner's silent step tau.

Keywords: Concurrency, process algebra, ACP, abstraction, bisimulation

4. Merge and termination in process algebra

J.C.M. Baeten (U. Amsterdam) & R.J. van Glabbeek (CWI)

April 1987

In Vrancken, the empty process was added to the Algebra of Communicating Processes of Bergstra & Klop. Reconsidering the definition of the parallel composition operator merge, we found that it is preferable to explicitly state the termination option. This gives an extra summand in the defining equation of merge, using the auxiliary operator tick. We find that tick can be defined in terms of the encapsulation operator. We give an operational and a denotational semantics for the resulting system ACP-tick, and prove that they are equal. We consider the Limit Rule, and prove it holds in our models.

Keywords: Concurrency, process algebra, ACP, empty process, termination, tick, bisimulation

5. Abstraction and empty process in process algebra

J.C.M. Baeten (U. Amsterdam) & R.J. van Glabbeek (CWI)

April 1987

In this paper, we combine the hidden step eta of 3 with the empty process of Vrancken and 4. We formulate a system ACPc, which is a conservative extension of the systems ACP_eta and ACP-tick, but also of ACP_tau. Abstraction from internal steps can be achieved in two ways, in two stages: we can abstract to the hidden step eta, and then from eta to Milner's silent step tau.

Keywords: Concurrency, process algebra, ACP, abstraction, empty process, termination, bisimulation

6. Petri net models for algebraic theories of concurrency

R.J. van Glabbeek (CWI) & F.W. Vaandrager (CWI)

June 1987

In this paper we discuss the issue of interleaving semantics versus True concurrency in an algebraic setting. We present various equivalence notions on Petri nets which can be used in the construction of algebraic models:
  1. the occurrence net equivalence of Nielsen, Plotkin and Winskel;
  2. bisimulation equivalence, which leads to a model which is isomorphic to the graph model of Baeten, Bergstra & Klop;
  3. the concurrent bisimulation equivalence, which is also described by Nielsen & Thiagarajan, and Goltz;
  4. partial order equivalences which are inspired by work of Pratt, and Boudol & Castellani.
A central role in the paper will be played by the notion of real-time consistency. We show that, besides occurrence net equivalence, none of the equivalences mentioned above (including the partial order equivalences!) is real-time consistent. Therefore we introduce the notion of ST-bisimulation equivalence, which is real-time consistent. Moreover a complete proof system will be presented for those finite ST-bisimulation processes in which no action can occur concurrently with itself.

Keywords: Concurrency, process algebra, ACP, Petri nets, semantic equivalences, interleaving vs. partial orders, bisimulation, real-time consistency.

7. Modular specifications in process algebra - with curious queues

R.J. van Glabbeek (CWI) & F.W. Vaandrager (CWI)

May 1988

In recent years a wide variety of process algebras has been proposed in the literature. Often these process algebras are closely related: they can be viewed as homomorphic images, submodels or restrictions of each other. The aim of this paper is to show how the semantical reality, consisting of a large number of closely related process algebras, can be reflected, and even used, on the level of algebraic specifications and in process verifications. This is done by means of the notion of a module. The simplest modules are building blocks of operators and axioms, each block describing a feature of concurrency in a certain semantical setting. These modules can then be combined by means of a union operator +, an export operator [], allowing to forget some operators in a module, an operator H, changing semantics by taking homomorphic images, and an operator S which takes subalgebras. These operators enable us to combine modules in a subtle way, when the direct combination would be inconsistent. We show how auxiliary process algebra operators can be hidden when this is needed. Moreover it is demonstrated how new process combinators can be defined in terms of more elementary ones in a clean way. As an illustration of our approach, a methodology is presented that can be used to specify FIFO-queues, and that facilitates verification of concurrent systems containing these queues.

Keywords: Concurrency, process algebra, ACP, modular algebraic specifications, export operator, union of modules, homomorphism operator, subalgebra operator, FIFO-queues, chaining operator, communication protocols.

Note: Most of this material is also included in 22.

8. Combining Compositionality and Concurrency
Summary of a GMD-Workshop, Königswinter, March 1988

E.-R Olderog (U. Kiel), U. Goltz (GMD) & R.J. van Glabbeek (CWI), editors

June 1988

Keywords: Concurrency, compositionality, CCSP, Petri nets, event structures, pomsets, semantic equivalences, interleaving vs. partial orders, temporal logic, action refinement.

An operational non-interleaved process graph semantics of CCSP

R.J. van Glabbeek (CWI)

March 1988

In this talk I argue that, contrary to what is widely believed, process graphs, or labelled transition systems, have enough structure to model non-interleaved features of concurrency. Moreover a non-interleaved process graph semantics of the system description language CCSP (a combination of CCS and CSP) is provided, using Plotkin's structural operational approach. Furthermore, criteria for semantic equivalences for concurrent systems are proposed and evaluated.

Keywords: Concurrency, CCSP, process graphs, event structures, Petri nets, structural operational semantics, semantic equivalences.

9. An interpolation theorem in equational logic

P.H. Rodenburg (U. Amsterdam) & R.J. van Glabbeek (CWI)

October 1988

In a natural formulation, Craig's interpolation theorem is shown to hold for equational logic. We also discuss the prevalent claims that equational logic does not have the interpolation property.

Keywords: Interpolation, Craig's lemma, equational logic, similarity, module algebra, splitting interpolation.

10. Equivalence notions for concurrent systems and refinement of actions

R.J. van Glabbeek (CWI) & U. Goltz (GMD)

February 1989

We investigate equivalence notions for concurrent systems. We consider "linear time" approaches where the system behaviour is characterized as the set of possible runs as well as "branching time" approaches where the conflict structure of systems is taken into account. We show that the usual interleaving equivalences, and also the equivalences based on steps (multisets of concurrently executed actions) are not preserved by refinement of actions. We prove that "linear time" partial order semantics, where causality in runs is explicit, is invariant under refinement. Finally, we consider various bisimulation equivalences based on partial orders and show that the strongest one of them is preserved by refinement whereas the others are not.

Keywords: Concurrency, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement.

Note: This material is also included in 20 and in 41.

11. Branching time and abstraction in bisimulation semantics (extended abstract)

R.J. van Glabbeek (CWI) & W.P. Weijland (CWI)

April 1989

In comparative concurrency semantics, one usually distinguishes between linear time and branching time semantic equivalences. Milner's notion of observation equivalence is often mentioned as the standard example of a branching time equivalence. In this paper we investigate whether observation equivalence really does respect the branching structure of processes, and find that in the presence of the unobservable action tau of CCS this is not the case.
Therefore the notion of branching bisimulation equivalence is introduced which strongly preserves the branching structure of processes, in the sense that it preserves computations together with the potentials in all intermediate states that are passed through, even if silent moves are involved. On closed terms, branching bisimulation can be completely axiomatized by the two laws:

x;tau = x
x;((tau;(y+z))+y) = x;(y+z).

For a large class of processes it turns out that branching bisimulation and observation equivalence are the same. All protocols known to the authors that have been verified in the setting of observation equivalence happen to fit in this class, and hence are also valid in the stronger setting of branching bisimulation equivalence.

Keywords: Concurrency, process algebra, semantic equivalences, abstraction, branching time, bisimulation.

Note: This is an extended abstract of 23.

12. Refinement in branching time semantics

R.J. van Glabbeek (CWI) & W.P. Weijland (CWI)

April 1989

In this paper we consider branching time semantics for finite sequential processes with silent moves. We show that Milner's notion of observation equivalence is not preserved under refinement of actions, even when no interleaving operators are considered; however the authors' notion of branching bisimulation is.

Keywords: Concurrency, process algebra, semantic equivalences, abstraction, branching time, bisimulation, action refinement.

Note: This paper is included in 23.

13. The processes of De Bakker and Zucker represent bisimulation equivalence classes

R.J. van Glabbeek (CWI) & J.J.M.M. Rutten (CWI)

April 1989

The domain of De Bakker and Zucker processes is the unique complete metric space (up to isometry) satisfying a reflexive domain equation for metric spaces. We give a straightforward translation from image finite labelled transition systems to processes in this domain, such that two labelled transition systems are bisimilar iff they translate to the same process. The isometries in this translation can be dispensed with after selecting a canonical representative of the metric domain within Aczel's universe of non-well-founded sets. Then the translation generalizes to systems which are not required to be image finite, in which case it may yield processes outside the metric space however.

Keywords: Concurrency, labelled transition systems, bisimulation, domain equations, metric space, fixed points, non-well-founded sets.

14. Partial order semantics for refinement of actions
-neither necessary nor always sufficient but appropriate when used with care-

R.J. van Glabbeek (CWI) & U. Goltz (GMD)

July 1989

In this note we argue:

Keywords: Concurrency, Petri nets, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement.

Note: This is an informal summary of 10 and 15, using Petri nets instead of event structures.

15. The refinement theorem for ST-bisimulation semantics

R.J. van Glabbeek (CWI)

January 1990

In this paper I prove that ST-bisimulation equivalence, as introduced in 6, is preserved under refinement of actions. This implies that it is possible to abstract from the causal structure of concurrent systems without assuming action atomicity.

Keywords: Concurrency, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement.

16. Refinement of actions in causality based models

R.J. van Glabbeek (CWI) & U. Goltz (GMD)

January 1990

We consider an operator for refinement of actions to be used in the design of concurrent systems. Actions on a given level of abstraction are replaced by more complex processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We define this refinement operation for causality based models like event structures and Petri nets. For Petri nets, we relate it to other approaches for refining transitions.

Keywords: Concurrency, Petri nets, event structures, action refinement.

Note: This paper is included in 41.

17. Comparative concurrency semantics and refinement of actions

R.J. van Glabbeek (CWI -> TU München)

May 1990

Keywords: Concurrency, process algebra, ACP, modular algebraic specifications, communication protocols, semantic equivalences, linear time, branching time, abstraction, bisimulation, labelled transition systems, event structures, Petri nets, interleaving vs. partial orders, action refinement

Note: This thesis combines the material of 19, 7, 11, 12, 23, 16, 14, 10, 20 and 15.

18. Reactive, generative, and stratified models of probabilistic processes

R.J. van Glabbeek (CWI), S.A. Smolka (SUNY at Stony Brook), B. Steffen (Aarhus U.) & C.M.N. Tofts (U. Edinburgh)

May 1990

We introduce three models of probabilistic processes, namely, reactive, generative, and stratified. These models are investigated within the context of PCCS, a dialect of Milner's SCCS in which each summand of a process summation expression is guarded by a probability and the sum of these probabilities is 1. For each model we present an operational semantics of PCCS and a notion of bisimulation equivalence which we prove to be a congruence. We also show that the models form a hierarchy: the reactive model is derivable from the generative model by abstraction of the relative probabilities of different actions, and the generative model is derivable from the stratified model by abstraction of the purely probabilistic branching structure.

Keywords: Concurrency, probabilistic processes, SCCS, structural operational semantics, bisimulation.

Note: This paper is included in 30.

19. The linear time - branching time spectrum

R.J. van Glabbeek (CWI -> TU München)

July 1990

In this paper various semantics in the linear time - branching time spectrum are presented in a uniform, model-independent way. Restricted to the domain of finitely branching, concrete, sequential processes, only twelve of them turn out to be different, and most semantics found in the literature that can be defined uniformly in terms of action relations coincide with one of these twelve. Several testing scenarios, motivating these semantics, are presented, phrased in terms of `button pushing experiments' on generative and reactive machines. Finally ten of these semantics are applied to a simple language for finite, concrete, sequential, nondeterministic processes, and for each of them a complete axiomatization is provided.

Keywords: Concurrency, Linear time, Branching time, Button pushing experiments, Generative machines, Reactive machines, Bisimulation semantics, Trace semantics, Failure semantics, Failure trace semantics, Readiness semantics, Ready trace semantics, Simulation semantics, Ready simulation semantics, Nondeterminism, Complete axiomatizations.

Note: This paper is included in 43.

20. Equivalences and refinement

R.J. van Glabbeek (TU München) & U. Goltz (GMD)

July 1990

Note: This is an extended and updated version of 10. The extension consists of considering equivalences and refinement for the domain of flow event structures - instead of the subdomain of prime event structures - and allowing also infinite refinements and refinements with conflict. This paper is included in 41.

Keywords: Concurrency, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement.

21. A deadlock-sensitive congruence for action refinement

R.J. van Glabbeek (TU München) & U. Goltz (GMD)

November 1990

We consider flow event structures as a model for concurrent systems. They are suited for defining a compositional refinement operation, replacing actions in system descriptions on a higher level by more complex processes on a lower level. We discuss sequential composition and the treatment of deadlocks in flow event structures. We propose an equivalence notion which takes account of deadlocks and is a congruence for the refinement operator.

Keywords: Concurrency, deadlock, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement.

Note: This paper is included in 41.

22. Modular specification of process algebras

R.J. van Glabbeek (TU München) & F.W. Vaandrager (CWI)

December 1990

This paper proposes a modular approach to the algebraic specification of process algebras. This is done by means of the notion of a module. The simplest modules are building blocks of operators and axioms, each block describing a feature of concurrency in a certain semantical setting. These modules can then be combined by means of a union operator +, an export operator [], allowing to forget some operators in a module, an operator H, changing semantics by taking homomorphic images, and an operator S which takes subalgebras. These operators enable us to combine modules in a subtle way, when the direct combination would be inconsistent. We give a presentation of equational logic, infinitary conditional equational logic - of which we also proof the completeness - and first order logic and show how the notion of a formal proof of a formula from a theory can be generalized to that of a proof of a formula from a module. This module logic is then applied in process algebra. We show how auxiliary process algebra operators can be hidden when this is needed. Moreover we demonstrate how new process combinators can be defined in terms of more elementary ones in a clean way. As an illustration of our approach we specify some FIFO-queues and verify several of their properties.

Keywords: Concurrency, process algebra, modular algebraic specifications, export operator, union of modules, homomorphism operator, subalgebra operator, FIFO-queues, chaining operator

Note: This is a substantial revision of part of 7. This revision intends to be an improvement; however, for more applications of our module approach, e.g. to the specification of more curious queues and to the verification of the concurrent alternating bit protocol, as well as for the treatment of many-sorted module logic, we refer to the old version.

23. Branching time and abstraction in bisimulation semantics

R.J. van Glabbeek (CWI -> TU München) & W.P. Weijland (CWI)

December 1990

See 11 and 12. Moreover the differences and similarities between branching bisimulation, tau-bisimulation (weak bisimulation, observation equivalence), eta-bisimulation (see 3) and delay bisimulation are investigated. Besides branching bisimulation with fair abstraction also branching bisimulation with explicit divergence and a branching bisimulation preorder are introduced. Complete axiomatizations of branching bisimulation on closed BPA-, CCS- and ACP-terms are provided. Whereas CCS has only action prefixing, BPA and ACP have general sequential composition; but only ACP distinguishes between deadlock and successful termination. For CCS the axiomatization consists of the single axiom scheme

a.((tau.(y+z))+y) = a.(y+z)

(where a ranges over all actions) and the usual laws of strong congruence.

Keywords: Concurrency, process algebra, semantic equivalences, abstraction, branching time, bisimulation, action refinement, divergence, deadlock, termination, tick.

Note: This paper properly contains 11 and 12. An updated version appeared in JACM 43(3), 1996, pp. 555-600.

24. Interleaving semantics and action refinement with atomic choice

I. Czaja (GMD), R.J. van Glabbeek (Stanford) & U. Goltz (GMD)

November 1991

We investigate how to restrict the concept of action refinement such that established interleaving equivalences for concurrent systems are preserved under these restricted refinements. We show that interleaving bisimulation is preserved under refinement if we do not allow to refine action occurrences deciding choices and action occurrences involved in autoconcurrency. On the other hand, interleaving trace equivalence is still not preserved under these restricted refinements.

Keywords: Concurrency, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, action refinement, atomicity.

25. A complete axiomatization for branching bisimulation congruence of finite-state behaviours

R.J. van Glabbeek (Stanford)

April 1993

This paper offers a complete inference system for branching bisimulation congruence on a basic sublanguage of CCS for representing regular processes with silent moves. Moreover, complete axiomatizations are provided for the guarded expressions in this language, representing the divergence-free processes, and for the recursion-free expressions, representing the finite processes. Furthermore it is argued that in abstract interleaving semantics (at least for finite processes) branching bisimulation congruence is the finest reasonable congruence possible. The argument is that for closed recursion-free process expressions, in the presence of some standard process algebra operations like partially synchronous parallel composition and relabelling, branching bisimulation congruence is completely axiomatized by the usual axioms for strong congruence together with Milner's first tau-law.

Keywords: Concurrency, regular processes, branching bisimulation, CCS, structural operational semantics, recursion, complete axiomatizations.

26. The linear time - branching time spectrum II
The semantics of sequential processes with silent moves

R.J. van Glabbeek (Stanford)

April 1993

This paper studies semantic equivalences and preorders for sequential systems with silent moves, restricting attention to the ones that abstract from successful termination, stochastic and real-time aspects of the investigated systems, and the structure of the visible actions systems can perform. It provides a parameterized definition of such a preorder, such that most such preorders and equivalences found in the literature are obtained by a suitable instantiation of the parameters. Other instantiations yield preorders that combine properties from various semantics. Moreover, the approach shows several ways in which preorders that were originally only considered for systems without silent moves, most notably the ready simulation, can be generalized to an abstract setting. All preorders come with--or rather as--a modal characterization, and when possible also a relational characterization. Moreover they are motivated by means of an (also parameterized) testing scenario, phrased in terms of `button pushing experiments' on generative and reactive machines. The testing scenarios for branching bisimulation, eta-bisimulation and coupled simulation and the corresponding modal characterizations are especially new.

Keywords: Concurrency, Labelled transition systems, Nondeterminism, Abstraction, Divergence, Underspecification, Liveness, Fairness, Recursion, Semantic equivalences, Linear time, Branching time, Generative and reactive systems, Button pushing experiments, May and must preorders, Modal Characterizations, Relational Characterizations, Trace semantics, Failure semantics, Failure trace semantics, Readiness semantics, Ready trace semantics, Simulation, Ready simulation, Stable bisimulation, Contrasimulation, Coupled simulation, Weak and branching bisimulation.

27. What is branching time and why to use it?

R.J. van Glabbeek (Stanford)

August 1993

The concept of branching time in the semantics of concurrent systems is well known and well understood. Still a formal definition of what it means for a model or equivalence to respect branching time has never explicitly be given. This note proposes such a definition. Additionally the opportunity is taken to voice an old but poorly understood argument for using branching time semantics instead of models or equivalences that are fully abstract with respect to some notion of observability.

Keywords: Concurrency, semantic equivalences, linear time, branching time, labelled transition systems, branching bisimulation.

28. Full Abstraction in Structural Operational Semantics (extended abstract)

R.J. van Glabbeek (Stanford)

December 1993

This paper explores the connection between semantic equivalences for concrete sequential processes, represented by means of transition systems, and formats of transition system specifications using Plotkin's structural approach. For several equivalences in the linear time - branching time spectrum a format is given, as general as possible, such that this equivalence is a congruence for all operators specifiable in that format. And 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.

Keywords: Concurrency, structural operational semantics, labelled transition systems, semantic equivalences.

Note: This is an extended abstract of material that has been elaborated in 33, 48, and a paper yet to be written.

29. Axiomatising ST-bisimulation equivalence

N. Busi (U. Siena), R.J. van Glabbeek (Stanford) & R. Gorrieri (U. Bologna)

December 1993

A simple ST operational semantics for a process algebra is provided, by defining a set of operational rules in Plotkin's style. This algebra comprises TCSP parallel composition, ACP sequential composition and a refinement operator, which is used for replacing an action with an entire process, thus permitting hierarchical specification of systems. We prove that ST-bisimulation equivalence is a congruence, resorting to standard techniques on rule formats. Moreover, we provide a set of axioms that is sound and complete with respect to ST-bisimulation. The intriguing case of the forgetful refinement (i.e., when an action is refined into the properly terminated process) is dealt with in a new, improved manner.

Keywords: Concurrency, complete axiomatizations, labelled transition systems, structural operational semantics, bisimulation, action refinement, empty process, termination

30. Reactive, generative and stratified models of probabilistic processes

R.J. van Glabbeek (Stanford), S.A. Smolka (SUNY at Stony Brook) & B. Steffen (U. Passau)

July 1994

We introduce three models of probabilistic processes, namely, reactive, generative and stratified. These models are investigated within the context of PCCS, an extension of Milner's SCCS in which each summand of a process summation expression is guarded by a probability and the sum of these probabilities is 1. For each model we present a structural operational semantics of PCCS and a notion of bisimulation equivalence which we prove to be a congruence. We also show that the models form a hierarchy: the reactive model is derivable from the generative model by abstraction of the relative probabilities of different actions, and the generative model is derivable from the stratified model by abstraction of the purely probabilistic branching structure. Moreover the classical nonprobabilistic model is derivable from each of these models by abstraction from all probabilities.

Keywords: Concurrency, probabilistic processes, SCCS, structural operational semantics, semantic equivalences, bisimulation.

Note: This paper properly contains 18.

31. On the expressiveness of ACP (extended abstract)

R.J. van Glabbeek (Stanford)

August 1994

De Simone showed that a wide class of languages, including CCS, SCCS, CSP and ACP, are expressible up to strong bisimulation equivalence in Meije. He also showed that every recursively enumerable process graph is representable by a Meije expression. Meije in turn is expressible in aprACP (ACP with action prefixing instead of sequential composition).
Vaandrager established that both results crucially depend on the use of unguarded recursion, and its noncomputable consequences. Effective versions of CCS, SCCS, Meije and ACP, not using unguarded recursion, are incapable of expressing all effective De Simone languages. And no effective language can denote all computable process graphs.
In this paper I recreate De Simone's results in aprACP without using unguarded recursion. The price to be payed for this is the use of a partial recursive communication function and--for the second result--a single constant denoting a simple infinitely branching process. Due to the noncomputable communication function, the version of aprACP employed is still not effective.
However, I also define a wide class of De Simone languages that are expressible in an effective version of aprACP. This class includes the effective versions of CCS, SCCS, ACP, Meije and most other languages proposed in the literature, but not CSP. An even wider class, including CSP, turns out to be expressible in an effective version of aprACP to which an effective relational renaming operator has been added.

Keywords: Concurrency, process algebra, ACP, Meije, CCS, CSP, SCCS, CCSP, relational relabelling, labelled transition systems, structural operational semantics, bisimulation.

32. The Meaning of Negative Premises in Transition System Specifications II

R.J. van Glabbeek (Stanford)

February 1995

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.

Keywords: Structural operational semantics, logic programming, negative premises, negation as failure.

Note: A mild revision with added emphasis on 3-valued interpretations appeared as 53.

33. Ntyft/ntyxt Rules Reduce to Ntree Rules

W.J. Fokkink (CWI) & R.J. van Glabbeek (Stanford)

February 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.

Keywords: Concurrency, labelled transition systems, structural operational semantics, bisimulation.

34. Configuration Structures (extended abstract)

R.J. van Glabbeek (Stanford) & G.D. Plotkin (U. Edinburgh)

June 1995

Configuration structures provide a model of concurrency generalising the families of configurations of event structures. They can be considered logically, as classes of propositional models; then sub-classes can be axiomatised by formulae of simple prescribed forms. Several equivalence relations for event structures are generalised to configuration structures, and also to general Petri nets. Every configuration structure is shown to be ST-bisimulation equivalent to a prime event structure with binary conflict; this fails for the tighter history preserving bisimulation. Finally, Petri nets without self-loops under the collective token interpretation are shown behaviourally equivalent to configuration structures, in the sense that there are translations in both directions respecting history preserving bisimulation. This fails for nets with self-loops.

Keywords: Concurrency, Configuration structures, Event structures, Petri nets, Semantic equivalences, Bisimulation.

35. The difference between splitting in n and n+1

R.J. van Glabbeek (Stanford) & F.W. Vaandrager (CWI)

July 1995

It is established that durational and structural aspects of actions can in general not be modeled in interleaving semantics, even when time-consuming actions are represented by pairs of instantaneous actions denoting their start and finish. By means of a series of counterexamples it is shown that, for any n, it makes a difference whether actions are split in n or in n+1 parts.

Owl example:

				  *
				 / \
				1   2
			       /     \
                              *	      *
			     / \     / \
			    0   2   1   0
			   /  -	 \ /  @	 \
			  *	  *	  *
			   \	 / \	 /
		       ,*.  2	0   0   1  ,*.
		    ,0'   `2.\ /     \ /,1'   `0.
		 .*'         `*  `-'  *'         `*.
	      ,1'   `2.   ,0'/ \     / \`0.   ,1'   `2.
	    *'	       `*'  1 	0   0  	2  `*'	       ,*
	      `2.    ,1'   /	 \ /     \    `2.   ,1'
		 `*'	  *	  *	  *   	 `*'
			  \	 / \	 /
			    0   1   2   0
			     \ /     \ /
			      *	      *
			       \     /
				2   1
				 \ /
				  *

Keywords: Concurrency, pomsets, event structures, process graphs, semantic equivalences, interleaving vs. partial orders, bisimulation, real-time consistency, action refinement, splitting.

iii. History Preserving Process Graphs

R.J. van Glabbeek (Stanford)

Draft

In this paper I argue that, contrary to what is widely believed, process graphs, or labelled transition systems, have enough structure to model non-interleaved features of concurrency.* To this end I introduce a class of process graphs obeying the restriction that any state not only uniquely characterizes the future of a concurrent behaviour, but also its concurrent history. These history preserving process graphs capture branching time, conjunctive (partial order) causality and disjunctive causality, just like Winskel's event structures, as well as phenonema like resolved conflict that can not be modelled by event structures. They generalize the Scott domains which arise as the duals of general event structures and can be regarded as a step towards a geometric model of concurrency.

Keywords: Concurrency, Process graphs, Event automata, Configuration structures, Event structures, Causality.

36. Branching Bisimulation as a Tool in the Analysis of Weak Bisimulation

R.J. van Glabbeek (Stanford)

September 1995

It is shown that the analysis of weak congruence can sometimes be simplified by means of a similar analysis of branching congruence as an intermediate step. This point is made through a completeness proof for an equational axiomatization of basic CCS with prefix iteration.

Keywords: Concurrency, process algebra, complete axiomatizations, weak and branching bisimulation, prefix iteration.

37. Axiomatizing prefix iteration with silent steps

L. Aceto (U. Aalborg), W.J. Fokkink (U. Utrecht), R.J. van Glabbeek (Stanford) & A. Ingólfsdóttir (U. Aalborg)

November 1995

Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. branching congruence, eta-congruence, delay congruence and weak congruence. The completeness proofs for eta-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e., terms that may contain process variables. As a byproduct, the omega-completeness of the axiomatizations is obtained as well as their completeness for closed terms.

Keywords: Concurrency, process algebra, basic CCS, prefix iteration, branching bisimulation, eta-bisimulation, delay bisimulation, weak bisimulation, equational logic, complete axiomatizations.

38. Axiomatizing flat iteration

R.J. van Glabbeek (Stanford)

April 1997

Flat iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be a sum of atomic actions. It generalizes prefix iteration, in which the first argument is a single action. Complete finite equational axiomatizations are given for five notions of bisimulation congruence over basic CCS with flat iteration, viz. strong congruence, branching congruence, eta-congruence, delay congruence and weak congruence. Such axiomatizations were already known for prefix iteration and are known not to exist for general iteration. The use of flat iteration has two main advantages over prefix iteration:
  1. The current axiomatizations generalize to full CCS, whereas the prefix iteration approach does not allow an elimination theorem for an asynchronous parallel composition operator.
  2. The greater expressiveness of flat iteration allows for much shorter completeness proofs.
In the setting of prefix iteration, the most convenient way to obtain the completeness theorems for eta-, delay, and weak congruence was by reduction to the completeness theorem for branching congruence. In the case of weak congruence this turned out to be much simpler than the only direct proof found. In the setting of flat iteration on the other hand, the completeness theorems for delay and weak (but not eta-) congruence can equally well be obtained by reduction to the one for strong congruence, without using branching congruence as an intermediate step. Moreover, the completeness results for prefix iteration can be retrieved from those for flat iteration, thus obtaining a second indirect approach for proving completeness for delay and weak congruence in the setting of prefix iteration.

Keywords: Concurrency, process algebra, CCS, flat iteration, strong bisimulation, branching bisimulation, eta-bisimulation, delay bisimulation, weak bisimulation, complete axiomatizations.

39. Computing Natural Language

Atocha Aliseda (Stanford), Rob van Glabbeek (Stanford) & Dag Westerståhl (U. Stockholm), editors

March 1998

Computing Natural Language pursues the recent upsurge of research along the interface of logic, language, and computation, with applications to artificial intelligence and machine learning. It contains a variety of contributions to the logical and computational analysis of natural language. A wide range of logical and computational tools are employed, and applied to such varied areas as context-dependency, linguistic discourse, and formal grammar.

This volume is a collection of papers illustrating state-of-the-art interdisciplinary research connecting logic, language, computation and AI. The papers in this volume deal with context-dependency from philosophical, computational, and logical points of view; a logical framework for combining dynamic discourse semantics and preferential reasoning in AI; negative polarity items in connection with affective predicates; Head-Driven Phrase Structure Grammar from a perspective of type theory and category theory; and an axiomatic theory of machine learning of natural language, with applications to physics word problems.

Keywords: Logic, Language, Computation, Philosophy, Artificial Intelligence, Context, Indexicals, Unarticulated Constituents, Discourse, Modal Logic, Dynamic Logic, Nonmonotonic Logic, Polarity, Monotonicity, Head-driven Phase Structure Grammar, Type Theory, Universality, Machine Learning, Physics Word Problems.

40. Scheduling Algebra

Rob van Glabbeek (Stanford) & Peter Rittgen (U. Koblenz-Landau)

March 1998; updated December 1998

The goal of this paper is to develop an algebraic theory of process scheduling. We specify a syntax for denoting processes composed of actions with given durations. Subsequently, we propose axioms for transforming any specification term of a scheduling problem into a term of all valid schedules. Here a schedule is a process in which all (implementational) choices (e.g. precise timing) are resolved. In particular, we axiomatize an operator restricting attention to the efficient schedules. These schedules turn out to be representable as trees, because in an efficient schedule actions start only at time zero or when a resource is released, i.e. upon termination of the action binding a required resource. All further delay would be useless. Nevertheless, we do not consider resource constraints explicitly here. We show that a normal form exists for every term of the algebra and establish soundness of our axiom system with respect to a schedule semantics, as well as completeness for efficient processes.

Keywords: Scheduling, efficiency, time, GANTT chart.

41. Refinement of Actions and Equivalence Notions for Concurrent Systems

Rob van Glabbeek (Stanford) & Ursula Goltz (U. Hildesheim)

April 1998

We study an operator for refinement of actions to be used in the design of concurrent systems. Actions on a given level of abstraction are replaced by more complicated processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We recall that interleaving models of concurrent systems are not suited for defining such an operator in its general form. Instead, we define this operator on several causality based, event oriented models, taking into account the distinction between deadlock and successful termination. Then we investigate the interplay of action refinement with abstraction in terms of equivalence notions for concurrent systems, considering both linear time and branching time approaches. We show that besides the interleaving equivalences, also the equivalences based on steps are not preserved under refinement of actions. We prove that linear time partial order semantics are invariant under refinement. Finally we consider various bisimulation equivalences based on partial orders and show that the finest two of them are preserved under refinement whereas the others are not. Termination sensitive versions of these equivalences are even congruences for action refinement.

Keywords: Concurrency, action refinement, event structures, semantic equivalences, interleaving vs. partial orders, bisimulation, termination, deadlock.

Note: This paper combines and extends the material of 10, 16, 20 and 21, except for the part in 16 on refinement of transitions in Petri nets and the discussion of TCSP-like parallel composition in 21. An informal presentation of some basic ingredients of this paper appeared as 14. Among others, the treatment of action refinement in stable and non-stable event structures is new.

42. Petri Nets, Configuration Structures and Higher Dimensional Automata

R.J. van Glabbeek (Stanford)

June 1999

In this talk, translations between several models of concurrent systems are reviewed c.q. proposed. The models considered capture causality, branching time, and their interplay, and these features are preserved by the translations. To the extent that the models are intertranslatable, this yields support for the point of view that they are all different representations of the same phenomena. The translations can then be applied to reformulate any issue that arises in the context of one model into one expressed in another model, which might be more suitable for analysing that issue. To the extent that the models are not intertranslatable, my investigations are aimed at classifying them w.r.t. their expressiveness in modelling phenomena in concurrency.

Keywords: Concurrency, Petri nets, configuration structures, labelled transition systems, higher dimensional automata, causality, branching time, individual vs. collective token interpretation of nets.

43. The Linear Time - Branching Time Spectrum I
The Semantics of Concrete, Sequential Processes

R.J. van Glabbeek (CWI -> TU München -> Stanford)

March 2000

In this paper various semantics in the linear time -- branching time spectrum are presented in a uniform, model-independent way. Restricted to the class of finitely branching, concrete, sequential processes, only fifteen of them turn out to be different, and most semantics found in the literature that can be defined uniformly in terms of action relations coincide with one of these fifteen. Several testing scenarios, motivating these semantics, are presented, phrased in terms of `button pushing experiments' on generative and reactive machines. Finally twelve of these semantics are applied to a simple language for finite, concrete, sequential, nondeterministic processes, and for each of them a complete axiomatization is provided.

Keywords: Concurrency, Labelled transition systems, Nondeterminism, Semantic equivalences, Linear time, Branching time, Generative and reactive systems, Button pushing experiments, Modal Characterizations, Relational Characterizations, Trace semantics, Failures semantics, Failure trace, Ready trace, Simulation, Ready simulation, Bisimulation, Complete axiomatizations, Compositionality, Full abstraction, Renaming, Deadlock, Termination, Sequencing, Recursive Specification Principle, Non-well-founded sets.

Note: This is an extension of 19.

44. Precongruence Formats for Decorated Trace Preorders

B. Bloom (Cornell -> IBM), W.J. Fokkink (CWI) & R.J. van Glabbeek (Stanford)

April 2000

This paper explores the connection between semantic equivalences and preorders for concrete sequential processes, represented by means of labelled transition systems, and formats of transition system specifications using Plotkin's structural approach. For several preorders in the linear time - branching time spectrum a format is given, as general as possible, such that this preorder is a precongruence for all operators specifiable in that format. The formats are derived using the modal characterizations of the corresponding preorders.

Keywords: Concurrency, structural operational semantics, labelled transition systems, semantic equivalences and preorders, compositionality, full abstraction.

Note: This paper refers for the full proofs to reference [6]. However, that paper turned out to become too large, and has been split into 48 and the full version of 28. The current paper is an extended abstract of 48, except that there we do not include the full abstraction results mentioned here. Those results originated from 28 and are planned to appear in a full version of 28.

45. Bisimulation

R.J. van Glabbeek (Stanford)

August 2000

Bisimulation equivalence is a semantic equivalence relation on labelled transition systems, which are used to represent distributed systems. It identifies systems with the same branching structure.

Keywords: Concurrency, labelled transition systems, modal logic, Kripke structures, bisimulation, non-well-founded sets, abstraction, weak and branching bisimulation.

46. Well-behaved Flow Event Structures for Parallel Composition and Action Refinement

R.J. van Glabbeek (Stanford) & U. Goltz (TU Braunschweig)

March 2002

Flow event structures were introduced as a model for giving semantics to process algebras. However it turned out that certain restrictions have to be made to make them suitable for this purpose. In this paper, we investigate subclasses of flow event structures which are both suited for the process algebraic composition operators, and for action refinement as a means of regarding processes on different levels of abstraction.

First, suitable subclasses are characterised. Then two specific subclasses are proposed. The larger class generalises the one from [CZ], which is not suitable for action refinement. The smaller one is still sufficiently expressive for dealing with all standard process algebras and action refinement.

Keywords: Concurrency, flow event structures, parallel composition, action refinement.

47. Token-controlled place refinement in hierarchical Petri nets with application to active document workflow

D.G. Stork (Ricoh) & R.J. van Glabbeek (Stanford)

March 2002

We propose extensions to predicate/transition nets to allow tokens to carry both data and control information, where such control can refine special "refinable place nodes" in the net. These formal extensions find use in active document workflow, in which documents themselves specify portions of the overall processing within a workflow net. Our approach enables the workflow designer to specify which places of the target predicate/transition net may be refined and enables the document author to specify how these places will be refined (via attachment of a token-generated "refinement net"). This apportionment of the overall task allows the workflow designer to set general constraints within which the document author can control the processing; it prevents conflicts between them in foreseeable practical cases. Refinable places are augmented with a permission structure specifying which document authors can refine that place and which document tokens can execute a node's refinement net. Our refined nets have a hierarchical structure which can be represented by bipartite trees.

Keywords: Active document workflow, Petri nets, hierarchical predicate/transition nets, token-controlled place refinement.

48. Precongruence Formats for Decorated Trace Semantics

B. Bloom (Cornell -> IBM), W.J. Fokkink (CWI) & R.J. van Glabbeek (Stanford)

April 2002

This paper explores the connection between semantic equivalences and preorders for concrete sequential processes, represented by means of labelled transition systems, and formats of transition system specifications using Plotkin's structural approach. For several preorders in the linear time - branching time spectrum a format is given, as general as possible, such that this preorder is a precongruence for all operators specifiable in that format. The formats are derived using the modal characterizations of the corresponding preorders.

Keywords: Concurrency, structural operational semantics, labelled transition systems, semantic equivalences and preorders, compositionality.

Note: This paper subsumes part of the material summarized in 28. An extended abstract of this paper appeared as 44, except that in the current paper we do not include the full abstraction results mentioned there. Those results originated from 28 and are planned to appear in a full version of 28.

49. Query Nets: Interacting Workflow Modules that Ensure Global Termination

R.J. van Glabbeek (Ricoh) & D.G. Stork (Ricoh)

March 2003

We address cross-organizational workflows, such as document workflows, which consist of multiple workflow modules each of which can interact with others by sending and receiving messages. Our goal is to guarantee that the global workflow network has properties such as termination while merely requiring properties that can be checked locally in individual modules. The resulting query nets are based on predicate/transition Petri nets and implement formal constructs for business rules, thereby ensuring such global termination. Our method does not require the notion of a global specification, as employed by Kindler, Martens and Reisig.

Keywords: Cross-organizational workflow, Petri nets, predicate/transition nets, soundness, proper termination, case independence.

50. Proof Nets for Unit-free Multiplicative-Additive Linear Logic (extended abstract)

D.J.D. Hughes (Stanford) & R.J. van Glabbeek (Stanford)

April 2003

A cornerstone of the theory of proof nets for unit-free multiplicative linear logic (MLL) is the abstract representation of cut-free proofs modulo inessential commutations of rules. The only known extension to additives, based on monomial weights, fails to preserve this key feature: a host of cut-free monomial proof nets can correspond to the same cut-free proof. Thus the problem of finding a satisfactory notion of proof net for unit-free multiplicative-additive linear logic (MALL) has remained open since the inception of linear logic in 1986. We present a new definition of MALL proof net which remains faithful to the cornerstone of the MLL theory.

Keywords: Linear logic, proof nets, additives, cut elimination.

Note: This is an extended abstract of 57.

51. Compositionality of Hennessy-Milner Logic through Structural Operational Semantics

W.J. Fokkink (CWI), R.J. van Glabbeek (CWI) & P. de Wind (VU)

May 2003

This paper presents a method for the decomposition of HML formulae. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulae, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is that an earlier decomposition method from Larsen for the De Simone format is extended to the more general ntyft/ntyxt format without lookahead.

Keywords: Concurrency, Structural Operational Semantics, Compositionality, Hennessy-Milner Logic, Modal Decomposition.

Note: This paper is included in 61.

52. Bundle Event Structures and CCSP

R.J. van Glabbeek (NICTA) & F.W. Vaandrager (U. Nijmegen)

June 2003

We investigate which event structures can be denoted by means of closed CCS + CSP expressions. Working up to isomorphism we find that Up to hereditary history preserving bisimulation equivalence finitary conflict can be expressed in terms of binary conflict. In this setting all countable stable event structures are denotable.

Keywords: Concurrency, event structures, CCSP, expressiveness.

53. The Meaning of Negative Premises in Transition System Specifications II

R.J. van Glabbeek (Stanford)

July 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 for logic programs.

Keywords: Structural operational semantics, logic programming, negative premises, negation as failure.

Note: This is a mild revision of 32 with added emphasis on 3-valued interpretations.

ix. Liveness respecting semantics

R.J. van Glabbeek (INRIA)

July 2003

In this talk I investigate, in a setting without real-time or probabilities, which semantical equivalences respect liveness properties. Many semantics proposed in the literature do not, which makes them less suitable for verification purposes. In fact, I argue that in interleaving semantics liveness properties are preserved only in the presence of global fairness assumptions. I'll give an overview of the interleaving semantics that respect liveness, and discuss their complexity and equational axiomatizations. When global fairness assumptions are not warranted, non-interleaving semantics are needed to preserve liveness properties in the presence of a parallel composition. I speculate about the possibilities in this regard.

Keywords: Concurrency, semantic equivalences, liveness, progress, fairness, justness, priority, parallel composition, interleaving semantics, Recursive Specification Principle, compositionality, impossible futures, real-time consistency, ST-failure trace semantics, complete axiomatizations.

54. Nested Semantics over Finite Trees are Equationally Hard

L. Aceto (U. Aalborg), W.J. Fokkink (CWI), R.J. van Glabbeek (INRIA) & A. Ingólfsdóttir (U. Aalborg & deCODE Genetics)

August 2003

This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based.

Keywords: Concurrency, process algebra, BCCSP, nested simulation, possible futures, nested trace semantics, equational logic, complete axiomatizations, non-finitely based algebras, Hennessy-Milner logic.

55. Event Structures for Resolvable Conflict

R.J. van Glabbeek (U. Edinburgh) & G.D. Plotkin (U. Edinburgh)

June 2004

We propose a generalisation of Winskel's event structures, matching the expressive power of arbitrary Petri nets. In particular, our event structures capture resolvable conflict, besides disjunctive and conjunctive causality.

Keywords: Concurrency, Event structures, Petri nets, Causality, Resolvable conflict.

56. On the Expressiveness of Higher Dimensional Automata (extended abstract)

R.J. van Glabbeek (NICTA)

November 2004 and April 2005

In this paper I compare the expressive power of several models of concurrency based on their ability to represent causal dependence. To this end, I translate these models, in behaviour preserving ways, into the model of higher dimensional automata, which is the most expressive model under investigation. In particular, I propose four different translations of Petri nets, corresponding to the four different computational interpretations of nets found in the literature.

I also extend various equivalence relations for concurrent systems to higher dimensional automata. These include the history preserving bisimulation, which is the coarsest equivalence that fully respects branching time, causality and their interplay, as well as the ST-bisimulation, a branching time respecting equivalence that takes causality into account to the extent that it is expressible by actions overlapping in time. Through their embeddings in higher dimensional automata, it is now well-defined whether members of different models of concurrency are equivalent.

Keywords: Concurrency, expressiveness, causality, higher dimensional automata, Petri nets, event structures, history preserving bisimulation, ST-bisimulation.

Note: This is an extended abstract of 63.

57. Proof Nets for Unit-free Multiplicative-Additive Linear Logic

D.J.D. Hughes (Stanford) & R.J. van Glabbeek (Stanford)

January 2005

A cornerstone of the theory of proof nets for unit-free multiplicative linear logic (MLL) is the abstract representation of cut-free proofs modulo inessential rule commutation. The only known extension to additives, based on monomial weights, fails to preserve this key feature: a host of cut-free monomial proof nets can correspond to the same cut-free proof. Thus the problem of finding a satisfactory notion of proof net for unit-free multiplicative-additive linear logic (MALL) has remained open since the inception of linear logic in 1986. We present a new definition of MALL proof net which remains faithful to the cornerstone of the MLL theory.

Keywords: Linear logic, proof nets, additives, cut elimination.

Note: An extended abstract of this paper appeared as 50.

58. On Cool Congruence Formats for Weak Bisimulations (extended abstract)

R.J. van Glabbeek (NICTA)

May 2005

In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner's "observational congruence"), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom's results in a more accessible form and contributes analogues for (rooted) eta-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom's formats fall short and further improvement is called for.

Keywords: Concurrency, structural operational semantics, CCS, compositionality, branching bisimulation, η-bisimulation, delay bisimulation, weak bisimulation, complete axiomatizations.

59. The Individual and Collective Token Interpretations of Petri Nets

R.J. van Glabbeek (NICTA)

May 2005

Starting from the opinion that the standard firing rule of Petri nets embodies the collective token interpretation of nets rather than their individual token interpretation, I propose a new firing rule that embodies the latter. Also variants of both firing rules for the self-sequential interpretation of nets are studied. Using these rules, I express the four computational interpretations of Petri nets by semantic mappings from nets to labelled step transition systems, the latter being event-oriented representations of higher dimensional automata. This paper totally orders the expressive power of the four interpretations, measured in terms of the classes of labelled step transition systems up to isomorphism of reachable parts that can be denoted by nets under each of the interpretations. Furthermore, I extend the unfolding construction of place/transition nets into occurrence net to nets that may have transitions without incoming arcs.

Keywords: Concurrency, Petri nets, higher dimensional automata, unfolding, expressiveness, causality.

60. On Specifying Timeouts

R.J. van Glabbeek (NICTA)

June 2005

This paper raises the question on how to specify timeouts in process algebra, and finds that the basic formalisms fall short in this task.

Keywords: Concurrency, Process Algebra, Liveness, Fairness, Timeouts, Priorities, Petri nets.

61. Compositionality of Hennessy-Milner Logic by Structural Operational Semantics

W.J. Fokkink (CWI), R.J. van Glabbeek (CWI -> NICTA) & P. de Wind (VU)

June 2005

This paper presents a method for the decomposition of HML formulas. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulas, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is the extension of an earlier decomposition method for the De Simone format from the PhD thesis of Kim G. Larsen in 1986, to more general formats.

Keywords: Concurrency, Structural Operational Semantics, Compositionality, Hennessy-Milner Logic, Modal Decomposition.

Note: This paper properly contains 51.

62. Divide and Congruence Applied to η-Bisimulation

W.J. Fokkink (VU,CWI), R.J. van Glabbeek (NICTA) & P. de Wind (VU)

June 2005 and October 2005

We present congruence formats for η- and rooted η-bisimulation equivalence. These formats are derived using a method for decomposing modal formulas in process algebra. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra.

Keywords: Concurrency, Structural Operational Semantics, Compositionality, Congruence, η-Bisimulation, Modal Logic, Modal Decomposition.

63. On the Expressiveness of Higher Dimensional Automata

R.J. van Glabbeek (NICTA)

July 2005

In this paper I compare the expressive power of several models of concurrency based on their ability to represent causal dependence. To this end, I translate these models, in behaviour preserving ways, into the model of higher dimensional automata, which is the most expressive model under investigation. In particular, I propose four different translations of Petri nets, corresponding to the four different computational interpretations of nets found in the literature.

I also extend various equivalence relations for concurrent systems to higher dimensional automata. These include the history preserving bisimulation, which is the coarsest equivalence that fully respects branching time, causality and their interplay, as well as the ST-bisimulation, a branching time respecting equivalence that takes causality into account to the extent that it is expressible by actions overlapping in time. Through their embeddings in higher dimensional automata, it is now well-defined whether members of different models of concurrency are equivalent.

Keywords: Concurrency, expressiveness, causality, higher dimensional automata, Petri nets, event structures, history preserving bisimulation, ST-bisimulation.

Note: An extended abstract of this paper appeared as 56.

x. Higher-Dimensional Automata and Other Models of Concurrency (abstract of presentation)

R.J. van Glabbeek (NICTA)

August 2005

I will compare the expressiveness of several models of concurrency that could be thought of as formalisations of higher dimensional automata: cubical sets, presheaves over a category of bipointed sets, automata with a predicate on hypercube-shaped subgraphs, labelled step transition systems, and higher dimensional transition systems. A series of counterexamples will illustrate the limitations of each of these models. Additionally I recall a few results relating higher dimensional automata to ordinary automata, Petri nets, and various kinds of event structures.

Keywords: Concurrency, expressiveness, causality, higher dimensional automata, Petri nets, event structures, history preserving bisimulation.

64. Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation

W.J. Fokkink (VU,CWI), R.J. van Glabbeek (NICTA) & P. de Wind (VU)

November 2005

We present a method for decomposing modal formulas for processes with the internal action τ. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for branching and rooted branching bisimulation equivalence.

Keywords: Concurrency, Structural Operational Semantics, Compositionality, Congruence, Branching Bisimulation, Modal Logic, Modal Decomposition.

65. A Characterisation of Weak Bisimulation Congruence

R.J. van Glabbeek (NICTA)

December 2005

This paper shows that weak bisimulation congruence can be characterised as rooted weak bisimulation equivalence, even without making assumptions on the cardinality of the sets of states or actions of the processes under consideration.

Keywords: Concurrency, process algebra, process graphs, weak bisimulation, root condition, Fresh Atom Principle.

66. Liveness, Fairness and Impossible Futures

R.J. van Glabbeek (NICTA) & M. Voorhoeve (TU Eindhoven)

June 2006

Impossible futures equivalence is the semantic equivalence on labelled transition systems that identifies systems iff they have the same "AGEF" properties: temporal logic properties saying that reaching a desired outcome is not doomed to fail. We show that this equivalence, with an added root condition, is the coarsest congruence containing weak bisimilarity with explicit divergence that respects deadlock/livelock traces (or fair testing, or any liveness property under a global fairness assumption) and assigns unique solutions to recursive equations.

Keywords: Concurrency, Process Algebra, Lifeness, Fairness, AGEF properties, Labelled Transition Systems, Se