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) η-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.

Note: This is an extended abstract of 88.

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.

Note: The material of this paper is included in 92.

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.

Note: The material of this paper is included in 92.

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, Semantic Equivalences, Recursive Specification Principle.

67. Branching Bisimilarity with Explicit Divergence

R.J. van Glabbeek (NICTA), B. Luttik (TU Eindhoven) & N. Trčka (TU Eindhoven)

December 2008
(A revision of a paper presented here in June 2006)

We consider the relational characterisation of branching bisimilarity with explicit divergence. We prove that it is an equivalence and that it coincides with the original definition of branching bisimilarity with explicit divergence in terms of coloured traces. We also establish a correspondence with several variants of an action-based modal logic with until- and divergence modalities.

Keywords: Concurrency, labelled transition systems, modal logic, branching bisimilarity, divergence, coloured traces.

68a. Preliminary Proceedings of the 3rd Workshop on Structural Operational Semantics, Bonn, Germany, 26 August 2006

R.J. van Glabbeek (NICTA) & P.D. Mosses (Swansea U.), editors

August 2006

68b. Proceedings of the 3rd Workshop on Structural Operational Semantics, Bonn, Germany, 26 August 2006

R.J. van Glabbeek (NICTA) & P.D. Mosses (Swansea U.), editors

November 2006

69. Remarks on Testing Probabilistic Processes

Y. Deng (UNSW), R.J. van Glabbeek (NICTA), M. Hennessy (U. Sussex), C.C. Morgan (UNSW) & C. Zhang (NICTA)

February 2007
(Preliminary report: September 2006)

We develop a general testing scenario for probabilistic processes, giving rise to two theories: probabilistic may testing and probabilistic must testing. These are applied to a simple probabilistic version of the process calculus CSP. We examine the algebraic theory of probabilistic testing, and show that many of the axioms of standard testing are no longer valid in our probabilistic setting; even for non-probabilistic CSP processes, the distinguishing power of probabilistic tests is much greater than that of standard tests. We develop a method for deriving inequations valid in probabilistic may testing based on a probabilistic extension of the notion of simulation. Using this, we obtain a complete axiomatisation for non-probabilistic processes subject to probabilistic may testing.

Keywords: Probabilistic processes, nondeterminism, CSP, transition systems, testing equivalences, simulation, complete axiomatisations, structural operational semantics.

70. Scalar Outcomes Suffice for Finitary Probabilistic Testing

Y. Deng (UNSW), R.J. van Glabbeek (NICTA), C.C. Morgan (UNSW) & C. Zhang (NICTA)

February 2007

The question of equivalence has long vexed research in concurrency, leading to many different denotational- and bisimulation-based approaches; a breakthrough occurred with the insight that tests expressed within the concurrent framework itself, based on a special ``success action'', yield equivalences that make only inarguable distinctions.

When probability was added, however, it seemed necessary to extend the testing framework beyond a direct probabilistic generalisation in order to remain useful. An attractive possibility was the extension to multiple success actions that yielded vectors of real-valued outcomes.

Here we prove that such vectors are unnecessary when processes are finitary, that is finitely branching and finite-state: single scalar outcomes are just as powerful. Thus for finitary processes we can retain the original, simpler testing approach and its direct connections to other naturally scalar-valued phenomena.

Keywords: Probabilistic processes, nondeterminism, probabilistic automata, testing equivalences, reward testing, hyperplanes, compactness, Markov Decision Processes.

71. Characterising Testing Preorders for Finite Probabilistic Processes

Y. Deng (UNSW), R.J. van Glabbeek (NICTA), M. Hennessy (U. Sussex), C.C. Morgan (UNSW) & C. Zhang (NICTA)

April 2007

In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.

Keywords: Probabilistic processes, nondeterminism, CSP, transition systems, testing equivalences, simulation, failure simulation, modal characterisations, complete axiomatisations.

Note: This is an extended abstract of 79.

72a. Preliminary Proceedings of the 4th Workshop on Structural Operational Semantics, Wroclaw, Poland, 9 July 2007

R.J. van Glabbeek (NICTA) & M. Hennessy (U. Sussex), editors

June 2007

72b. Proceedings of the 4th Workshop on Structural Operational Semantics, Wroclaw, Poland, 9 July 2007

R.J. van Glabbeek (NICTA) & M. Hennessy (U. Sussex), editors

September 2007

73. Computation Tree Logic with Deadlock Detection

R.J. van Glabbeek (NICTA), B. Luttik (TU Eindhoven) & N. Trčka (TU Eindhoven)

January 2008 and December 2009

We study the equivalence relation on states of labelled transition systems of satisfying the same formulas in Computation Tree Logic without the next state modality (CTL-X). This relation is obtained by De Nicola & Vaandrager by translating labelled transition systems to Kripke structures, while lifting the totality restriction on the latter. They characterised it as divergence sensitive branching bisimulation equivalence.

We find that this equivalence fails to be a congruence for interleaving parallel composition. The reason is that the proposed application of CTL-X to non-total Kripke structures lacks the expressiveness to cope with deadlock properties that are important in the context of parallel composition. We propose an extension of CTL-X, or an alternative treatment of non-totality, that fills this hiatus. The equivalence induced by our extension is characterised as branching bisimulation equivalence with explicit divergence, which is, moreover, shown to be the coarsest congruence contained in divergence sensitive branching bisimulation equivalence.

Keywords: Concurrency, temporal logic, Kripke structures, labelled transition systems, stuttering equivalence, branching bisimulation, divergence, deadlock.

74. Correcting a Space-Efficient Simulation Algorithm

R.J. van Glabbeek (NICTA) & B. Ploeger (TU Eindhoven)

January 2008

Although there are many efficient algorithms for calculating the simulation preorder on finite Kripke structures, only two have been proposed of which the space complexity is of the same order as the size of the output of the algorithm. Of these, the one with the best time complexity exploits the representation of the simulation problem as a generalised coarsest partition problem. It is based on a fixed-point operator for obtaining a generalised coarsest partition as the limit of a sequence of partition pairs. We show that this fixed-point theory is flawed, and that the algorithm is incorrect. Although we do not see how the fixed-point operator can be repaired, we correct the algorithm without affecting its space and time complexity.

Keywords: Concurrency, verification, algorithms, time and space complexity, simulation preorder, Kripke structures, generalised coarsest partition problem.

75. Five Determinisation Algorithms

R.J. van Glabbeek (NICTA) & B. Ploeger (TU Eindhoven)

May 2008

Determinisation of nondeterministic finite automata is a well-studied problem that plays an important role in compiler theory and system verification. In the latter field, one often encounters automata consisting of millions or even billions of states. On such input, the memory usage of analysis tools becomes the major bottleneck. In this paper we present several determinisation algorithms, all variants of the well-known subset construction, that aim to reduce memory usage and produce smaller output automata. One of them produces automata that are already minimal. We apply our algorithms to determinise automata that describe the possible sequences appearing after a fixed-length run of cellular automaton 110, and obtain a significant improvement in both memory and time efficiency.

Keywords: Automata, determinisation, minimisation, algorithms, running time, memory use.

76. Special Issue of Information and Computation on Structural Operational Semantics

R.J. van Glabbeek (NICTA) & P.D. Mosses (Swansea U.), editors

June 2008

77. Symmetric and Asymmetric Asynchronous Interaction

R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & J.-W. Schicke (TU Braunschweig)

July 2008

We investigate classes of systems based on different interaction patterns with the aim of achieving distributability. As our system model we use Petri nets. In Petri nets, an inherent concept of simultaneity is built in, since when a transition has more than one preplace, it can be crucial that tokens are removed instantaneously. When modelling a system which is intended to be implemented in a distributed way by a Petri net, this built-in concept of synchronous interaction may be problematic. To investigate the problem we assume that removing tokens from places can no longer be considered as instantaneous. We model this by inserting silent (unobservable) transitions between transitions and their preplaces. We investigate three different patterns for modelling this type of asynchronous interaction. Full asynchrony assumes that every removal of a token from a place is time consuming. For symmetric asynchrony, tokens are only removed slowly in case of backward branched transitions, hence where the concept of simultaneous removal actually occurs. Finally we consider a more intricate pattern by allowing to remove tokens from preplaces of backward branched transitions asynchronously in sequence (asymmetric asynchrony).

We investigate the effect of these different transformations of instantaneous interaction into asynchronous interaction patterns by comparing the behaviours of nets before and after insertion of the silent transitions. We exhibit for which classes of Petri nets we obtain equivalent behaviour with respect to failures equivalence.

It turns out that the resulting hierarchy of Petri net classes can be described by semi-structural properties. In case of fully symmetric asynchrony and symmetric asynchrony, we obtain precise characterisations; for asymmetric asynchrony we obtain lower and upper bounds.

We briefly comment on possible applications of our results to Message Sequence Charts.

Keywords: Concurrency, Petri nets, distributed systems, asynchronous interaction, semantic equivalences.

78. On Synchronous and Asynchronous Interaction in Distributed Systems

R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & J.-W. Schicke (TU Braunschweig)

July 2008

When considering distributed systems, it is a central issue how to deal with interactions between components. In this paper, we investigate the paradigms of synchronous and asynchronous interaction in the context of distributed systems. We investigate to what extent or under which conditions synchronous interaction is a valid concept for specification and implementation of such systems. We choose Petri nets as our system model and consider different notions of distribution by associating locations to elements of nets. First, we investigate the concept of simultaneity which is inherent in the semantics of Petri nets when transitions have multiple input places. We assume that tokens may only be taken instantaneously by transitions on the same location. We exhibit a hierarchy of `asynchronous' Petri net classes by different assumptions on possible distributions. Alternatively, we assume that the synchronisations specified in a Petri net are crucial system properties. Hence transitions and their preplaces may no longer placed on separate locations. We then answer the question which systems may be implemented in a distributed way without restricting concurrency, assuming that locations are inherently sequential. It turns out that in both settings we find semi-structural properties of Petri nets describing exactly the problematic situations for interactions in distributed systems.

Keywords: Concurrency, Petri nets, distributed systems, reactive systems, asynchronous interaction, semantic equivalences.

79. Characterising Testing Preorders for Finite Probabilistic Processes

Y. Deng (Shanghai Jiao Tong University), R.J. van Glabbeek (NICTA), M. Hennessy (Trinity College Dublin) & C.C. Morgan (UNSW)

July 2008

In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.

Keywords: Probabilistic processes, nondeterminism, CSP, transition systems, testing equivalences, simulation, failure simulation, modal characterisations, complete axiomatisations.

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

80. Ready to Preorder: The Case of Weak Process Semantics

T. Chen (CWI), W.J. Fokkink (VU) & R.J. van Glabbeek (NICTA)

August 2008

Recently, Aceto, Fokkink & Ingólfsdóttir proposed an algorithm to turn any sound and complete axiomatisation of any preorder listed in the linear time – branching time spectrum at least as coarse as the ready simulation preorder, into a sound and complete axiomatisation of the corresponding equivalence—its kernel. Moreover, if the former axiomatisation is ω-complete, so is the latter. Subsequently, de Frutos Escrig, Gregorio Rodríguez & Palomino generalised this result, so that the algorithm is applicable to any preorder at least as coarse as the ready simulation preorder, provided it is initials preserving. The current paper shows that the same algorithm applies equally well to weak semantics: the proviso of initials preserving can be replaced by other conditions, such as weak initials preserving and satisfying the second τ-law. This makes it applicable to all 87 preorders surveyed in "the linear time – branching time spectrum II" that are at least as coarse as the ready simulation preorder. We also extend the scope of the algorithm to infinite processes, by adding recursion constants. As an application of both extensions, we provide a complete axiomatisation of the CSP failures equivalence for BCCS processes with divergence.

Keywords: Concurreny, process algebra, BCCS, labelled transition systems, semantic equivalences and preorders, equational axiomatisations, ω-completeness; failures equivalence

81. On Finite Bases for Weak Semantics: Failures versus Impossible Futures

T. Chen (CWI), W.J. Fokkink (VU,CWI) & R.J. van Glabbeek (NICTA)

October 2008

We provide a finite basis for the (in)equational theory of the process algebra BCCS modulo the weak failures preorder and equivalence. We also give positive and negative results regarding the axiomatizability of BCCS modulo weak impossible futures semantics.

Keywords: Concurrency, Process Algebra, BCCS, labeled transition systems, complete axiomatizations, failures semantics, impossible futures semantics.

82. Configuration Structures, Event Structures and Petri Nets

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

May 2009

In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without self-loops, under the collective token interpretation. To this end we propose a more general form of event structure, matching the expressive power of such nets. These new event structures and nets are connected by relating both notions with configuration structures, which can be regarded as representations of either event structures or nets that capture their behaviour in terms of action occurrences and the causal relationships between them, but abstract from any auxiliary structure.

A configuration structure can also be considered logically, as a class of propositional models, or - equivalently - as a propositional theory in disjunctive normal from. Converting this theory to conjunctive normal form is the key idea in the translation of such a structure into a net.

For a variety of classes of event structures we characterise the associated classes of configuration structures in terms of their closure properties, as well as in terms of the axiomatisability of the associated propositional theories by formulae of simple prescribed forms, and in terms of structural properties of the associated Petri nets.

Keywords: Concurrency, Configuration structures, Event structures, Petri nets, Propositional Logic.

  • Available as dvi, ps, pdf and tex file.
  • Archived at http://arxiv.org/abs/0912.4023.
  • Theoretical Computer Science 410(41) (2009), pp. 4111-4159. DOI: 10.1016/j.tcs.2009.06.014
  • This abstract: http://theory.stanford.edu/~rvg/abstracts.html#82

    83. Testing Finitary Probabilistic Processes (extended abstract)

    Y. Deng (Shanghai Jiao Tong University), R.J. van Glabbeek (NICTA), M. Hennessy (Trinity College Dublin) & C.C. Morgan (UNSW)

    June 2009

    We provide both modal- and relational characterisations of may- and must-testing preorders for recursive CSP processes with divergence, featuring probabilistic as well as nondeterministic choice. May testing is characterised in terms of simulation, and must testing in terms of failure simulation. To this end we develop weak transitions between probabilistic processes, elaborate their topological properties, and express divergence in terms of partial distributions.

    Keywords: Probabilistic processes, nondeterminism, CSP, transition systems, testing equivalences, simulation, failure simulation, modal characterisations, divergence.

    84. On CSP and the Algebraic Theory of Effects

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

    February 2010

    We consider CSP from the point of view of the algebraic theory of effects, which classifies operations as effect constructors or effect deconstructors; it also provides a link with functional programming, being a refinement of Moggi's seminal monadic point of view. There is a natural algebraic theory of the constructors whose free algebra functor is Moggi's monad; we illustrate this by characterising free and initial algebras in terms of two versions of the stable failures model of CSP, one more general than the other. Deconstructors are dealt with as homomorphisms to (possibly non-free) algebras.

    One can view CSP's action and choice operators as constructors and the rest, such as concealment and concurrency, as deconstructors. Carrying this programme out results in taking deterministic external choice as constructor rather than general external choice. However, binary deconstructors, such as the CSP concurrency operator, provide unresolved difficulties. We conclude by presenting a combination of CSP with Moggi's computational λ-calculus, in which the operators, including concurrency, are polymorphic. While the paper mainly concerns CSP, it ought to be possible to carry over similar ideas to other process calculi.

    Keywords: Concurrency, functional programming, computational lambda-calculus, free algebras, (de)constructors, stable failures model.

    85. The Coarsest Precongruences Respecting Safety and Liveness Properties

    R.J. van Glabbeek (NICTA)

    July 2010

    This paper characterises the coarsest refinement preorders on labelled transition systems that are precongruences for renaming and partially synchronous interleaving operators, and respect all safety, liveness, and conditional liveness properties, respectively.

    Keywords: Safety properties, liveness properties, conditional liveness properties, refinement preorders, labelled transition systems, full abstraction, process algebra, partially synchronous interleaving operator, abstraction, state operator, deadlock, divergence.

    86. Characterising Probabilistic Processes Logically

    Y. Deng (Shanghai Jiao Tong University) & R.J. van Glabbeek (NICTA)

    September 2010

    In this paper we work on (bi)simulation semantics of processes that exhibit both nondeterministic and probabilistic behaviour. We propose a probabilistic extension of the modal mu-calculus and show how to derive characteristic formulae for various simulation-like preorders over finite-state processes without divergence. In addition, we show that even without the fixpoint operators this probabilistic mu-calculus can be used to characterise these behavioural relations in the sense that two states are equivalent if and only if they satisfy the same set of formulae.

    Keywords: Concurreny, Probabilistic Processes, Modal mu-calculus, simulation, bisimulation, characteristic formulae.

    87. Real-Reward Testing for Probabilistic Processes (extended abstract)

    Y. Deng (Shanghai Jiao Tong University), R.J. van Glabbeek (NICTA), M. Hennessy (Trinity College Dublin) & C.C. Morgan (UNSW)

    February 2011

    We introduce a notion of real-valued reward testing for probabilistic processes by extending the traditional nonnegative-reward testing with negative rewards. In this richer testing framework, the may and must preorders turn out to be inverses. We show that for convergent processes with finitely many states and transitions, but not in the presence of divergence, the real-reward must-testing preorder coincides with the nonnegative-reward must-testing preorder. To prove this coincidence we characterise the usual resolution-based testing in terms of the weak transitions of processes, without having to involve policies, adversaries, schedulers, resolutions, or similar structures that are external to the process under investigation. This requires establishing the continuity of our function for calculating testing outcomes.

    Keywords: Probabilistic processes, nondeterminism, transition systems, testing equivalences, reward testing, failure simulation, divergence.

    88. On Cool Congruence Formats for Weak Bisimulations

    R.J. van Glabbeek (NICTA)

    February 2011

    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) η-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, and an extension of Bloom's formats for this type of operator 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, CSP, compositionality, branching bisimulation, η-bisimulation, delay bisimulation, weak bisimulation, complete axiomatizations.

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

    89. Abstract Processes of Place/Transition Systems

    R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & J.-W. Schicke (TU Braunschweig)

    February 2011

    A well-known problem in Petri net theory is to formalise an appropriate causality-based concept of process or run for place/transition systems. The so-called individual token interpretation, where tokens are distinguished according to their causal history, giving rise to the processes of Goltz and Reisig, is often considered too detailed. The problem of defining a fully satisfying more abstract concept of process for general place/transition systems has so-far not been solved. In this paper, we recall the proposal of defining an abstract notion of process, here called BD-process, in terms of equivalence classes of Goltz-Reisig processes, using an equivalence proposed by Best and Devillers. It yields a fully satisfying solution for at least all one-safe nets. However, for certain nets which intuitively have different conflicting behaviours, it yields only one maximal abstract process. Here we identify a class of place/transition systems, called structural conflict nets, where conflict and concurrency due to token multiplicity are clearly separated. We show that, in the case of structural conflict nets, the equivalence proposed by Best and Devillers yields a unique maximal abstract process only for conflict-free nets. Thereby BD-processes constitute a simple and fully satisfying solution in the class of structural conflict nets.

    Highlights:

    Note: This paper ends with an open question that is answered in 90.

    Keywords: Concurrency, Petri nets, PT-systems, causal semantics, processes.

    90. On Causal Semantics of Petri Nets

    R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & J.-W. Schicke (TU Braunschweig)

    June 2011

    We consider approaches for causal semantics of Petri nets, explicitly representing dependencies between transition occurrences. For one-safe nets or condition/event-systems, the notion of process as defined by Carl Adam Petri provides a notion of a run of a system where causal dependencies are reflected in terms of a partial order. A well-known problem is how to generalise this notion for nets where places may carry several tokens. Goltz and Reisig have defined such a generalisation by distinguishing tokens according to their causal history. However, this so-called individual token interpretation is often considered too detailed. A number of approaches have tackled the problem of defining a more abstract notion of process, thereby obtaining a so-called collective token interpretation. Here we give a short overview on these attempts and then identify a subclass of Petri nets, called structural conflict nets, where the interplay between conflict and concurrency due to token multiplicity does not occur. For this subclass, we define abstract processes as equivalence classes of Goltz-Reisig processes. We justify this approach by showing that we obtain exactly one maximal abstract process if and only if the underlying net is conflict-free with respect to a canonical notion of conflict.

    Keywords: Concurrency, Petri nets, PT-systems, causal semantics, processes.

    Note: This paper continues and completes the work started in 89. Together, these papers show that a structural conflict net is conflict-free if and only if it has exactly one maximal run—equivalently formalised as maximal BD-run, a maximal BD-process or a maximal GR-process up to swapping equivalence. The "if" direction stems from 89, and "only if", together with taxonomy of suitable notions of maximality, from 90.

    91. Modelling and Analysis of AODV in UPPAAL

    A. Fehnker (NICTA), R.J. van Glabbeek (NICTA), P. Höfner (NICTA), A.K. McIver (Macquarie University), M. Portmann (NICTA) & W.L. Tan (NICTA)

    October 2011

    This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in ad hoc wireless networks. We give a brief overview of a model of AODV implemented in the UPPAAL model checker, and describe experiments carried out to explore AODV's behaviour in two network topologies. We were able to locate automatically and confirm some known problematic and undesirable behaviours. We believe this use of model checking as a diagnostic tool complements other formal methods based protocol modelling and verification techniques, such as process algebras. Model checking is in particular useful for the discovery of protocol limitations and in the development of improved variations.

    Keywords: wireless mesh networks; mobile ad-hoc networks; routing protocols; AODV; model checking, UPPAAL, process algebra, AWN.

    92. Divide and Congruence: From Decomposition of Modal Formulas to Preservation of Branching and η-Bisimilarity

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

    November 2011

    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 two weak and rooted weak semantics: branching and η-bisimilarity.

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

    Note: This paper properly contains the material of 64 and 62.

    93. A Process Algebra for Wireless Mesh Networks

    A. Fehnker (NICTA), R.J. van Glabbeek (NICTA), P. Höfner (NICTA), A.K. McIver (Macquarie University), M. Portmann (NICTA) & W.L. Tan (NICTA)

    December 2011

    We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.

    Keywords: wireless mesh networks; mobile ad-hoc networks; process algebra; local braodcast; routing protocols; AODV; loop freedom.

    94. Automated Analysis of AODV using UPPAAL

    A. Fehnker (NICTA), R.J. van Glabbeek (NICTA), P. Höfner (NICTA), A.K. McIver (Macquarie University), M. Portmann (NICTA) & W.L. Tan (NICTA)

    December 2011

    This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.

    We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.

    Keywords: wireless mesh networks; mobile ad-hoc networks; routing protocols; AODV; model checking, UPPAAL, process algebra, AWN.

    Note: First steps towards this analysis appeared in 91.

    95. On Distributability of Petri Nets

    R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & J.-W. Schicke-Uffmann (TU Braunschweig)

    To appear.

    We formalise a general concept of distributed systems as sequential components interacting asynchronously. We define a corresponding class of Petri nets, called LSGA nets, and precisely characterise those system specifications which can be implemented as LSGA nets up to branching ST-bisimilarity with explicit divergence.

    Keywords: Concurrency, Petri nets, distributed systems, reactive systems, asynchronous interaction, semantic equivalences.

    SFB-reports of the TU Munich (19-23) can be obtained from: The original version of my dissertation can be ordered through me, and costs $11 or 7 euro. The second edition can be ordered through your bookstore, or from CWI.
    The book 39 can be ordered through your bookstore, or from CSLI, Stanford University, CA 94305, USA.
    All other papers are available through me (free).

    Rob van Glabbeek

    rvg@CS.Stanford.EDU