Abstracts

The following is a list of abstracts of and references to my papers, followed by addresses where they can be ordered.
Here is a list of just the papers. Here are the references in bibtex format. And here are pointers to my papers sorted by subject.

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.

i. De semantiek van eindige, sequentiële processen met interne acties,

R.J. van Glabbeek (CWI)

Keywords: Concurrency, Labelled transition systems, Nondeterminism, Abstraction, Semantic equivalences, Linear time, Branching time, Trace semantics, Failure semantics, Failure trace semantics, Readiness semantics, Ready trace semantics, Stable bisimulation, Weak bisimulation, BCCS, BCSP, Complete axiomatisations.

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.

ii. Bisimulations for higher dimensional automata

R.J. van Glabbeek (Stanford)

July 1991

This message defines higher dimensional automata, a notion of (history preserving) bisimulation between them, directed homotopy between paths in an HDA, and the unfolding of HDA.

Keywords: Higher dimensional automata, cubical sets, (history preserving) bisimulation, homotopy, unfolding.

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.

iv. Petri Nets, Configuration Structures, Propositional Theories and History Preserving Process Graphs (abstract of presentation)

R.J. van Glabbeek (Stanford)

May 1996

Translations between several models of concurrency are reviewed cq. proposed. The models considered capture causality and branching time (and their interplay) and this behaviour is preserved by the translations.

Keywords: Concurrency, Petri nets, event structures, configuration structures, Scott domains, propositional theories, labelled transition systems, history preserving process graphs, higher dimensional automata, causality, branching time, individual vs. collective token interpretation of nets.

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.

vi. On the Relative Expressiveness of Petri Nets, Event Structures and Process Algebras (abstract of presentation)

R.J. van Glabbeek (Stanford)

February 1998

In this talk I consider mappings from expressions in system description languages like CCS and CSP to Petri nets and vice versa. I recall two methods for associating a Petri net to such a process expression: the standard compositional approach where recursion is dealt with using fixed point techniques, and a variant due to Ursula Goltz in which recursion is implemented by redirecting arcs backwards to initial places. The former approach always yields a so-called safe flow net; recursion typically gives rise to infinite nets. The latter approach works for the subclass of process expressions where in the scope of a recursion construct only prefixing, independent parallel composition and guarded choice is allowed; but always yields finite S/T-nets. The two approaches are identical for recursion-free process expressions; in general they agree up to fully concurrent bisimulation equivalence. Here I extend the latter approach to deal with unguarded recursion. I also show that for every finite S/T-net there exists a process expression in the mentioned subclass whose semantics, up to fully concurrent bisimulation, is that net. Moreover, every finite safe flow net is denoted up to event-structure isomorphism by a recursion-free process expression.

Keywords: Concurrency, Petri nets, process algebra, CCS, CSP, denotational semantics,recursion, fully concurrent bisimulation.

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.

P1. The third millennium starts on January 1 of the year 2001

R.J. van Glabbeek (Stanford)

December 2, 1999

In this note I argue that the 3rd millennium starts on the the first of January of the year 2001, rather than on the first of January of the year 2000.

Keywords: Millennium, calendar, counting.

P2. Do we count from 0 or from 1?
The ordinal use of cardinal expressions

R.J. van Glabbeek (Stanford)

December 6, 1999

Keywords: Counting, ordinal numbers, cardinal numbers, inclusive versus exclusive counting, millennium, calendar.

vii. Preface
Special issue of Information and Computation dedicated to EXPRESS'97

C. Palamidessi (Pennsylvania State U.), J. Parrow (Royal Institute of Technology, Sweden) & R.J. van Glabbeek (Stanford)

January 2000

Keywords: Concurrency, expressiveness.

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.

Note: The hyperlinks in the above document work perfectly. In fact, this may very well be the only latex paper ever written with correct hyperlinks. Here correct is defined as to adhere the hyperref standard, as advertised on various (changing) websites since the end of the 20th century. Unfortunately, the latex hyperref package does not adhere to this standard, even though it was written by the same people that developed the hyperref standard.

The only document reader I know of that abides by the hyperref standard, and thus correctly displays the above document, is xdvi. This reader went out of fashion in the early part of the 21th century, perhaps exactly because it correctly interpreted the hyperref standard. If you now use xdvi you really run xdvik, which used to be a competitor of xdvi that follows the hyperref package rather than the hyperref standard.

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.

C1. Decidability
An introduction to decidability theory without invoking Church' thesis

R.J. van Glabbeek (Stanford)

February 23, 2001

Keywords: Decidability, formal language, algorithms, halting, enumerability, recognizability

C2. The undefinability of definability

R.J. van Glabbeek (Stanford)

February 23, 2001

Keyword: undefinable languages.

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.

Dedication: to Jan Willem Klop, on the occasion of his 60th birthday.

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.

Dedication: to Gordon Plotkin, on the occasion of his 60th birthday.

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.

Note: The material in this paper reappears in 109, but with rather different proofs.

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.

    xi. The Linear Time – Branching Time Spectrum after 20 years

    Full abstraction for safety and liveness properties

    R.J. van Glabbeek (NICTA)

    2nd September 2009

    If I had to pick just one semantic preorder with a good scope of useful applications, I'd say it should be the coarsest preorder that respects all safety and (conditional) liveness properties, and is compositional for standard operators such as hiding and partially synchronous parallel composition. Such a preorder is called fully abstract.
    1. May-testing equivalence is fully abstract for safety properties.
    2. Must testing is fully abstract for liveness properties (w.r.t. abstraction, renaming and interleaving) [DH84].
    3. The may-testing preorder as stated is less useful; its inverse is fully abstract for safety properties.
    4. The must-testing preorder is not strong enough. It is fully abstract for liveness properties but misses out on conditional liveness properties, which are just as important.
    5. I present a finer semantics that is fully abstract for safety and conditional liveness properties w.r.t. abstraction and interleaving.
    6. I also characterise respect for conditional liveness properties by means of reward testing, where positive or negative real-valued rewards can be allocated to states of test-processes.
    7. Due to the use of interleaving operators, must-testing and related semantics make distinctions that are wholly unobservable when using merely parallel composition.
    8. I propose a new semantics that is fully abstract for safety and (conditional) liveness properties w.r.t. hiding and parallel composition.
    I also reflect on other grounds for selecting particular equivalences from the the Linear Time – Branching Time Spectrum.

    Keywords: Safety properties, liveness properties, conditional liveness properties, refinement preorders, labelled transition systems, full abstraction, process algebra, partially synchronous interleaving operator, parallel composition, abstraction, may- and must-testing preorders, reward testing, deadlock, livelock, divergence.

    Note: Contributions 1–4 were later published as 85.

    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.

    Dedication: to Tony Hoare, in honor of his 75th birthday.

    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.

    Erratum, 2018: A reference to Lamport has been corrected into one to Alpern & Schneider.

    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.

    Note: This is an extended abstract of 99.

    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.

    Dedication: to Jan Bergstra, on the occasion of his 60th birthday.

    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 a taxonomy of suitable notions of maximality, is contributed here.

    The main results of this paper appear again, with different proofs, in 151 and 152.

    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; AWN; local broadcast; routing protocols; AODV; loop freedom.

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

    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)

    June 2012

    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.

    Note: A further elaborated version of this paper appeared as 101.

    96. Celebrating the 60th Birthday of Carroll Morgan
    Special issue of Formal Aspects of Computing

    P. Höfner (NICTA), R.J. van Glabbeek (NICTA) & I.J. Hayes (U. Queensland), editors

    July 2012

    This triple issue of Formal Aspects of Computing constitutes a Festschrift dedicated to Professor Charles Carroll Morgan, on the occasion of his sixtieth birthday. The Festschrift consists of an invited paper and 23 scientific research papers, all related to Carroll's own research interests.

    Keywords: Carroll Morgan, Laws of Programming, Refinement Calculus, Refinement of Ignorance, Herman's Ring, Security, Probability and Nondeterminism.

    97. A Rigorous Analysis of AODV and its Variants

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

    July 2012

    In this paper we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Networks), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.

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

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

    98. Musings on Encodings and Expressiveness

    R.J. van Glabbeek (NICTA)

    July 2012

    This paper proposes a definition of what it means for one system description language to encode another one, thereby enabling an ordering of system description languages with respect to expressive power. I compare the proposed definition with other definitions of encoding and expressiveness found in the literature, and illustrate it on a case study: comparing the expressive power of CCS and CSP.

    Keywords: Expressiveness, encodings, languages, translations, compositionality, semantic equivalences, CCS, CSP.

    99. Real-Reward Testing for Probabilistic Processes

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

    May 2013

    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.

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

    100. Sequence Numbers Do Not Guarantee Loop Freedom —AODV Can Yield Routing Loops—

    R.J. van Glabbeek (NICTA), P. Höfner (NICTA), W.L. Tan (NICTA) & M. Portmann (NICTA)

    August 2013

    In the area of mobile ad-hoc networks and wireless mesh networks, sequence numbers are often used in routing protocols to avoid routing loops. It is commonly stated in protocol specifications that sequence numbers are sufficient to guarantee loop freedom if they are monotonically increased over time. A classical example for the use of sequence numbers is the popular Ad hoc On-Demand Distance Vector (AODV) routing protocol. The loop freedom of AODV is not only a common belief, it has been claimed in the abstract of its RFC and at least two proofs have been proposed. AODV-based protocols such as AODVv2 (DYMO) and HWMP also claim loop freedom due to the same use of sequence numbers.

    In this paper we show that AODV is not a priori loop free; by this we counter the proposed proofs in the literature. In fact, loop freedom hinges on non-evident assumptions to be made when resolving ambiguities occurring in the RFC. Thus, monotonically increasing sequence numbers, by themselves, do not guarantee loop freedom.

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

    Note: The material of this paper is included in 102, although the presentation of the material is somewhat different.

    101. On Characterising Distributability

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

    September 2013

    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.

    Note: This paper is adapted from 95; it characterises distributability for a slightly larger range of semantic equivalence relations, and incorporates various remarks stemming from 78.

    102. A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV

    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 2013

    Route finding and maintenance are critical for the performance of networked systems, particularly when mobility can lead to highly dynamic and unpredictable environments; such operating contexts are typical in wireless mesh networks. Hence correctness and good performance are strong requirements of routing protocols.

    In this paper we propose AWN (Algebra for Wireless Networks), a process algebra tailored to the modelling of Mobile Ad hoc Network (MANET) and Wireless Mesh Network (WMN) protocols. It combines novel treatments of local broadcast, conditional unicast and data structures.

    In this framework, we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) protocol, a popular routing protocol designed for MANETs and WMNs, and one of the four protocols currently defined as an RFC (request for comments) by the IETF MANET working group.

    We give a complete and unambiguous specification of this protocol, thereby formalising the RFC of AODV, the de facto standard specification, given in English prose. In doing so, we had to make non-evident assumptions to resolve ambiguities occurring in that specification. Our formalisation models the exact details of the core functionality of AODV, such as route maintenance and error handling, and only omits timing aspects.

    The process algebra allows us to formalise and (dis)prove crucial properties of mesh network routing protocols such as loop freedom and packet delivery. We are the first to provide a detailed proof of loop freedom of AODV. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. Due to ambiguities and contradictions the RFC specification allows several readings. For this reason, we analyse multiple interpretations. In fact we show for more than 5000 interpretations whether they are loop free or not. Thereby we demonstrate how the reasoning and proofs can relatively easily be adapted to protocol variants.

    Using our formal and unambiguous specification, we find some shortcomings of AODV that can easily affect performance. Examples are non-optimal routes established by AODV and the fact that some routes are not found at all. These problems are analysed and improvements are suggested. As the improvements are formalised in the same process algebra, carrying over the proofs is again relatively easy.

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

    Note: This paper includes the material of [93, 97, 100, 114], although the presentation of the material is somewhat different. The loop freedom proof described herein has been mechanised in the theorem prover Isabelle/HOL in [103, 104].

    103. Showing invariance compositionally for a process algebra for network protocols

    T. Bourke (INRIA), R.J. van Glabbeek (NICTA) & P. Höfner (NICTA)

    April 2014

    This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.

    Keywords: wireless mesh networks; mobile ad-hoc networks; process algebra; AWN; interactive theorem proving; Isabelle/HOL; invariants; compositional lifting technique

    Note: This is an extended abstract of 112.

    104. A mechanized proof of loop freedom of the (untimed) AODV routing protocol

    T. Bourke (INRIA), R.J. van Glabbeek (NICTA) & P. Höfner (NICTA)

    July 2014

    The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is 'loop free' if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.

    Keywords: wireless mesh networks; mobile ad-hoc networks; routing protocols; AODV; loop freedom; process algebra; AWN; interactive theorem proving; Isabelle/HOL; invariants; compositional lifting technique

    105. Special issue on “Combining Compositionality and Concurrency”: part 1

    R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & E.-R. Olderog (U. Oldenburg)

    December 2014

    In March 1988, we organised a workshop on “Combining Compositionality and Concurrency” in Königswinter near Bonn, Germany. We were motivated by the following dichotomy. One the one hand, a theory of concurrency was initiated by Carl Adam Petri, with notions like causality, conflict, and concurrency. One the other hand, a theory of communicating processes was developed by Robin Milner and Tony Hoare, where the emphasis was put on composing processes by algebraic operators like sequential, nondeterministic, and parallel composition.

    For quite a some time little interaction took place between the followers of these two lines of research. Then it was more and more realized that a full understanding, analysis or construction of parallel processes is impossible without combining the best from concurrency and compositionality. The idea of the workshop was therefore to invite researchers active in the area of combining compositionality and concurrency.

    In the meantime the relationships between these two directions have been carefully investigated. Today, the elements of the different semantic approaches are freely mixed. Also, the scope of systems that are modelled by concurrent or process algebraic means is much extended, for example, to mobile and probabilistic systems.

    In 2013, we called for a workshop “25 Years of Combining Compositionality and Concurrency”. We received very enthusiastic responses, and the jubilee workshop took place in August 2013 at the very same venue in Königswinter as the first one.1 This special issue results from a call for papers sent out right after the workshop. It comes in two parts: this first part comprises three papers.

    The paper Revisiting Causality, Coalgebraically by Roberto Bruni, Ugo Montanari, and Matteo Sammartino recasts a causal semantics of concurrency originally defined by Darondeau and Degano in a coalgebraic setting. By exploiting the equivalence between coalgebras over a class of presheaves and history dependent automata, they derive a compact model.

    The paper Synthesis and Reengineering of Persistent Systems by Eike Best and Raymond Devillers considers synthesis and reengineering problems in the framework of finite-state labelled transitions systems and place/transition Petri nets. They obtain exact conditions for a finite persistent transition system to be isomorphically implementable by a bounded Petri net exhibiting persistence in a structural way. Moreover, they derive an efficient algorithm to find such a net if it exists.

    The paper Revisiting Bisimilarity and its Modal Logic for Nondeterministic and Probabilistic Processes by Marco Bernado, Rocco De Nicola, and Michele Loretti investigates new notions of bi-similarity that correspond to extensions of the logic PML to probabilistic processes with internal nondeterminism; PML itself is a probabilistic version of Hennessy–Milner logic introduced by Larsen and Skou to characterise bisimilarity over probabilistic processes without internal nondeterminism.

    Keywords: concurrency, compositionality, causality, coalgebras, synthesis, Petri nets, bisimilarity, probabilistic processes.

    106. Progress, Fairness and Justness in Process Algebra

    R.J. van Glabbeek (NICTA) & P. Höfner (NICTA)

    January 2015

    To prove liveness properties of concurrent systems, it is often necessary to postulate progress, fairness and justness properties. This paper investigates how the necessary progress, fairness and justness assumptions can be added to or incorporated in a standard process-algebraic specification formalism. We propose a formalisation that can be applied to a wide range of process algebras. The presented formalism is used to reason about route discovery and packet delivery in the setting of wireless networks.

    Keywords: progress; justness; fairness; liveness; process algebra; labelled transition systems; Linear-time Temporal Logic; CCS, broadcast communication; fairness specifications.

    107. CCS: It's not Fair!
    Fair Schedulers cannot be implemented in CCS-like languages
    even under progress and certain fairness assumptions

    R.J. van Glabbeek (NICTA) & P. Höfner (NICTA)

    April 2015

    In the process algebra community it is sometimes suggested that, on some level of abstraction, any distributed system can be modelled in standard process-algebraic specification formalisms like CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful and provides a mechanism for interaction. This paper counters that sentiment by presenting a simple fair scheduler—one that in suitable variations occurs in many distributed systems—of which no implementation can be expressed in CCS, unless CCS is enriched with a fairness assumption.

    Since Dekker's and Peterson's mutual exclusion protocols implement fair schedulers, it follows that these protocols cannot be rendered correctly in CCS without imposing a fairness assumption. Peterson expressed this algorithm correctly in pseudocode without resorting to a fairness assumption, so it furthermore follows that CCS lacks the expressive power to accurately capture such pseudocode.

    Keywords: process algebra; CCS; expressiveness, fair schedulers, progress; justness; fairness; Petri nets; labelled transition systems; Linear-time Temporal Logic; mutual exclusion protocols.

    Dedication: It is our great pleasure to dedicate this paper to Walter Vogler on the occasion of his 60th birthday. We have combined two of Walter's main interests: Petri nets and process algebra. In fact, we proved a result about Petri nets that had been proven before by Walter, but in a restricted form, as we discovered only after finishing our proof. We also transfer this result to the process algebra CCS.

    Beyond foundational research in the theory of concurrent systems, Walter achieved excellent results in related subjects such as temporal logic and efficiency. In addition to being a dedicated researcher, he is also meticulous in all of his endeavours, including his writing. As a consequence his scientific papers tend to contain no flaws, which is just one of the reasons that makes reading them so enjoyable.

    It's fair to say: ``CCS Walter!'' –Congratulations and Continuous Success!

    108. Special issue on “Combining Compositionality and Concurrency”: part 2

    R.J. van Glabbeek (NICTA), U. Goltz (TU Braunschweig) & E.-R. Olderog (U. Oldenburg)

    May 2014

    This is the second part of the special issue motivated by the workshop "25 Years of Combining Compositionality and Concurrency" that we organised in August 2013 in Königswinter near Bonn, Germany. The first part was published in Acta Informatica (2015) 52(1):3-106. For an introduction to the topic see our editorial there. This second part comprises four papers.

    The paper Richer Interface Automata with Optimistic and Pessimistic Compatibility by Gerald Lüttgen, Walter Vogler, and Sascha Fendrich addresses component-based reasoning for concurrent systems via modal interface automata (MIA). The authors study optimistic and pessimistic MIA variants with internal must-transitions. They define conjunction and disjunction on interfaces as well as mechanisms for extending alphabets.

    The paper Compositional Verification of Asynchronous Concurrent Systems using CADP by Hubert Garavel, Frédéric Lang, and Radu Mateescu investigates how various compositional techniques help to fight the state-space explosion in the verification of asynchronous message-passing systems. The techniques are implemented in the toolbox CADP (Construction and Analysis of Distributed Processes). The authors compare the different approaches using a common case study.

    The paper Denotational Fixed-Point Semantics for Constructive Scheduling of Synchronous Concurrency by Joaquín Aguado, Michael Mendler, Reinhard von Hanxleden, and Insa Fuhrmann defines an abstract semantic domain and an associated denotational semantics for synchronous programs. The semantics induces three notions of constructiveness, among them the new notion of Input Berry-constructiveness (IBC) for these programs. The authors study behavioural properties of IBC programs.

    The paper Compositional Construction of Most General Controllers by Joachim Klein, Christel Baier, and Sascha Klüppelholz considers for given transitions systems conjunctions of linear-time objectives to be achieved by a controller. The authors present game-based algorithms for the compositional construction of most general controllers for invariance, reachability, and ω-regular objectives.

    Keywords: concurrency, compositionality, modal interface automata, asynchronous systems, CADP, denotational semantics, synchronous programs, most general controllers.

    109. On the Axiomatizability of Impossible Futures

    T. Chen (Middlesex University London), W.J. Fokkink (VU) & R.J. van Glabbeek (NICTA)

    May 2015

    A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no finite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is infinite, then the aforementioned ground-complete axiomatizations are shown to be omega-complete. If the alphabet is finite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a finite basis.

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

    Note: The results on complete axiomatizations, and their absence, for weak failures and weak impossible futures semantics occurred before in 81, but without the proof strategy of distilling axiomatizations for weak semantics from those of concrete semantics.

    110. Analysing and Comparing Encodability Criteria

    K. Peters (TU Berlin) & R.J. van Glabbeek (NICTA)

    August 2015

    Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are augmented with quality criteria. There exists a bunch of different criteria and different variants of criteria in order to reason in different settings. This leads to incomparable results. Moreover it is not always clear whether the criteria used to obtain a result in a particular setting do indeed fit to this setting. We show how to formally reason about and compare encodability criteria by mapping them on requirements on a relation between source and target terms that is induced by the encoding function. In particular we analyse the common criteria full abstraction, operational correspondence, divergence reflection, success sensitiveness, and respect of barbs; e.g. we analyse the exact nature of the simulation relation (coupled simulation versus bisimulation) that is induced by different variants of operational correspondence. This way we reduce the problem of analysing or comparing encodability criteria to the better understood problem of comparing relations on processes.

    Keywords: Process Algebra, expressiveness, encodings, reduction semantics, barbs, operational correspondence, semantic equivalences, bisimulation, coupled simulation.

    Note: All claims in this paper have been proved using the interactive theorem prover Isabelle/HOL. The Isabelle implementation of the theories is available in the Archive of Formal Proofs, at http://afp.sourceforge.net/entries/Encodability_Process_Calculi.shtml

    111. Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP

    R.J. van Glabbeek (NICTA)

    September 2015

    In 1987 Ernst-Rüdiger Olderog provided an operational Petri net semantics for a subset of CCSP, the union of Milner's CCS and Hoare's CSP. It assigns to each process term in the subset a labelled, safe place/transition net. To demonstrate the correctness of the approach, Olderog established agreement (1) with the standard interleaving semantics of CCSP up to strong bisimulation equivalence, and (2) with standard denotational interpretations of CCSP operators in terms of Petri nets up to a suitable semantic equivalence that fully respects the causal structure of nets. For the latter he employed a linear-time semantic equivalence, namely having the same causal nets.

    This paper strengthens (2), employing a novel branching-time version of this semantics–structure preserving bisimilarity–that moreover preserves inevitability. I establish that it is a congruence for the operators of CCSP.

    Keywords: Concurrency, Petri nets, process algebra, CCSP, operational semantics, semantic equivalences, linear time, branching time, bisimulation, interleaving vs. partial orders, inevitability, action refinement, real-time consistency, causality, causal nets, progress, justness.

    Dedication: to Ernst-Rüdiger Olderog, on the occasion of his 60th birthday.

    112. Mechanizing a Process Algebra for Network Protocols

    T. Bourke (INRIA), R.J. van Glabbeek (NICTA) & P. Höfner (NICTA)

    October 2015

    This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.

    Keywords: interactive theorem proving; Isabelle/HOL; process algebra; AWN; wireless mesh networks; mobile ad-hoc networks; compositional invariant proofs

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

    113. Proceedings Workshop on Models for Formal Analysis of Real Systems, Suva, Fiji, November 23, 2015

    R.J. van Glabbeek (NICTA) & J.F. Groote (TU Eindhoven) & P. Höfner (NICTA), editors

    November 2015

    This volume contains the proceedings of MARS 2015, the first workshop on Models for Formal Analysis of Real Systems, held on November 23, 2015 in Suva, Fiji, as an affiliated workshop of LPAR 2015, the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning.

    The workshop emphasises modelling over verification. It aims at discussing the lessons learned from making formal methods for the verification and analysis of realistic systems. Examples are:
    (1) Which formalism is chosen, and why?
    (2) Which abstractions have to be made and why?
    (3) How are important characteristics of the system modelled?
    (4) Were there any complications while modelling the system?
    (5) Which measures were taken to guarantee the accuracy of the model?

    We invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. Alternative formal descriptions of the systems presented at this workshop are encouraged, which should foster the development of improved specification formalisms.

    114. Modelling and Verifying the AODV Routing Protocol

    R.J. van Glabbeek (NICTA), P. Höfner (NICTA), M. Portmann (U. Queensland) & W.L. Tan (Griffith U.)

    December 2015

    This paper presents a formal specification of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.

    Keywords: Wireless mesh networks; mobile ad-hoc networks; routing protocols; AODV; process algebra; AWN; loop freedom.

    Note: Most of the material of this paper is included in 102, although the presentation is somewhat different.

    115. A Timed Process Algebra for Wireless Networks with an Application in Routing

    E. Bres (École Polytechnique), R.J. van Glabbeek (NICTA) & P. Höfner (NICTA)

    January 2016

    This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc On-Demand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.

    Keywords: Wireless mesh networks; mobile ad-hoc networks; timed process algebra; AWN; routing protocols; AODV; loop freedom.

    xii. Ensuring Liveness Properties of Distributed Systems
    (A Research Agenda)

    R. J. van Glabbeek (NICTA)

    March 2016

    Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations these lead to false conclusions.

    This document presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models, as well as treatments of real-time. The agenda also includes developing a methodology that allows successful application of this theory to the specification, analysis and verification of realistic distributed systems, including routing protocols for wireless networks.

    Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating new treatments of time and probability.

    Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.

    Keywords: Liveness, fairness, justness, progress, distributed systems, concurrency, process algebra, temporal logic, labelled transition systems, Petri nets, semantic equivalences, strong bisimulation, fair schedulers, mutual exclusion, expressiveness, routing protocols, wireless mesh networks, structural operational semantics, probabilistic processes, real-time, approximation induction principle, recursive specification principle.

    Note: Most of the material of this paper is included in 138, although the presentation is somewhat different.

    116. Divide and Congruence II: Delay and Weak Bisimilarity

    W.J. Fokkink (VU) & R.J. van Glabbeek (NICTA)

    April 2016

    Earlier we presented a method to decompose modal formulas for processes with the internal action τ; congruence formats for branching and η-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that formulas in the modal characterisation of this semantics are always decomposed into formulas in this modal characterisation. Here the decomposition method is enhanced to deal with modal characterisations that contain a modality <τ*a>φ, to derive congruence formats for delay and weak bisimilarity.

    Keywords: Structural operational semantics, congruence formats, weak bisimilarity, modal characterisation.

    Note: This is an extended abstract of 117.

    117. Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity

    W.J. Fokkink (VU) & R.J. van Glabbeek (NICTA)

    April 2016

    Earlier we presented a method to decompose modal formulas for processes with the internal action τ, and congruence formats for branching and η-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. In this follow-up paper the decomposition method is enhanced to deal with modal characterisations that contain a modality <τ*a>φ, to derive congruence formats for delay and weak bisimilarity.

    Keywords: Structural operational semantics, congruence formats, weak bisimilarity, modal characterisation.

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

    Erratum: With Definition 20.4b(i) as formulated originally, Proposition 5 does not hold. A corrected Definition 20.4b appears in the revision below.

    118. MALL proof nets identify proofs modulo rule commutation

    R.J. van Glabbeek (Data61, CSIRO) & D.J.D. Hughes (Stanford)

    July 2016

    We show that the proof nets introduced in [50, 57] for MALL (Multiplicative Additive Linear Logic, without units) identify cut-free proofs modulo rule commutation: two cut-free proofs translate to the same proof net if and only if one can be obtained from the other by a succession of rule commutations. This result holds with and without the mix rule, and we extend it with cut.

    Keywords: Linear logic, proof nets, additives, rule commutations.

    119. An Algebraic Treatment of Recursion

    R.J. van Glabbeek (Data61, CSIRO)

    December 2016

    I review the three principal methods to assign meaning to recursion in process algebra: the denotational, the operational and the algebraic approach, and I extend the latter to unguarded recursion.

    Keywords: Process algebra, unguarded recursion, denotational semantics, operational semantics, algebraic semantics.

    Dedication: Jan Bergstra has put his mark on theoretical computer science by a consistent stream of original ideas, controversial opinions, and novel approaches. He sometimes reorganised the arena, enabling others to follow. I, for one, might never have entered computer science if it wasn't for Jan's support and encouragement, and will never forget the team spirit in the early days of process algebra in his group at CWI. This paper is dedicated to Jan, at the occasion of his 65th birthday and retirement.

    120. A Branching Time Model of CSP

    R.J. van Glabbeek (Data61, CSIRO)

    January 2017

    I present a branching time model of CSP that is finer than all other models of CSP proposed thus far. It is obtained by taking a semantic equivalence from the linear time – branching time spectrum, namely divergence-preserving coupled similarity, and showing that it is a congruence for the operators of CSP. This equivalence belongs to the bisimulation family of semantic equivalences, in the sense that on transition systems without internal actions it coincides with strong bisimilarity. Nevertheless, enough of the equational laws of CSP remain to obtain a complete axiomatisation for closed, recursion-free terms.

    Keywords: Process algebra, CSP, branching time, coupled similarity, complete axiomatisation.

    Dedication: to Bill Roscoe, on the occasion of his 60th birthday.

    121. Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack

    R.J. van Glabbeek (Data61, CSIRO) & P. Höfner (Data61, CSIRO)

    February 2017

    We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an in-built mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.

    Keywords: CAN bus, fragmentation protocol, priority inversion, process algebra, AWN.

    122. Precongruence Formats with Lookahead through Modal Decomposition

    W.J. Fokkink (VU) & R.J. van Glabbeek (Data61, CSIRO)

    March 2017

    Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

    Keywords: Structural operational semantics, compositionality, congruence formats, modal characterisation, lookahead.

    123. Lean and Full Congruence Formats for Recursion

    R.J. van Glabbeek (Data61, CSIRO)

    April 2017

    In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions.

    I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.

    Keywords: Structural Operational Semantics, Congruence formats, Recursion, Bisimulation.

    124. Divide and Congruence III: Stability & Divergence

    W.J. Fokkink (VU), R.J. van Glabbeek (Data61, CSIRO) & B. Luttik (TU Eindhoven)

    July 2017

    In two earlier papers we derived congruence formats for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. Here this work is extended with important stability and divergence requirements. Stability refers to the absence of a tau-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. Divergence, which refers to the presence of an infinite sequence of tau-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

    Keywords: Structural operational semantics, compositionality, congruence formats, modal characterisation, divergence, weak semantics, branching bisimulation

    Note: This is an extended abstract of 125.

    125. Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence

    W.J. Fokkink (VU), R.J. van Glabbeek (Data61, CSIRO) & B. Luttik (TU Eindhoven)

    August 2017

    In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a tau-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of tau-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

    Keywords: Structural operational semantics, compositionality, congruence formats, modal characterisation, divergence, weak semantics, branching bisimulation

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

    126. Analysing Mutual Exclusion using Process Algebra with Signals

    V. Dyseryn (Ecole Polytechnique), R.J. van Glabbeek (Data61, CSIRO) & P. Höfner (Data61, CSIRO)

    August 2017

    In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counter-intuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.

    Keywords: mutual exclusion protocols, liveness, process algebra, CCS, signals, non-blocking reading, progress, justness, fairness, expressiveness, structural operational semantics, memory models.

    127. Rooted Divergence-Preserving Branching Bisimilarity is a Congruence

    R.J. van Glabbeek (Data61, CSIRO), B. Luttik (TU Eindhoven) & L. Spaninks (TU Eindhoven)

    January 2018

    We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of 0, action prefix, choice, and the recursion construct μX._.

    Keywords: Process algebra; Recursion; Branching bisimulation; Divergence; Congruence.

    128. On the Validity of Encodings of the Synchronous in the Asynchronous π-calculus

    R.J. van Glabbeek (Data61, CSIRO)

    February/April 2018

    Process calculi may be compared in their expressive power by means of encodings between them. A widely accepted definition of what constitutes a valid encoding for (dis)proving relative expressiveness results between process calculi was proposed by Gorla. Prior to this work, diverse encodability and separation results were generally obtained using distinct, and often incompatible, quality criteria on encodings.

    Textbook examples of valid encoding are the encodings proposed by Boudol and by Honda & Tokoro of the synchronous choice-free π-calculus into its asynchronous fragment, illustrating that the latter is no less expressive than the former. Here I formally establish that these encodings indeed satisfy Gorla's criteria.

    Keywords: Process calculi, expressiveness, quality criteria for encodings, valid encoding, π-calculus

    129. A Case Study on Evaluating Encodings Between Process Calculi

    C. Lippert (TU Braunschweig), S. Mennicke (TU Braunschweig), R.J. van Glabbeek (Data61, CSIRO) & U. Goltz (TU Braunschweig)

    April 2018

    Two process calculi may be compared in their expressive power using encodings between them. Not every such translation is meaningful and therefore quality criteria are necessary. There are several frameworks to assess the quality of encodings. A rather prominent approach consists of five criteria for valid encodings collected by Gorla. An alternative notion of validity up to a semantic equivalence was proposed by one of the authors. Here the quality of the encoding is measured by the strength of the semantic equivalence that makes it valid.

    In this paper we analyse two well-known translations from the synchronous into the asynchronous π-calculus, both meeting Gorla's criteria, and evaluate the encodings' validity up to different semantic equivalences.

    While Honda and Tokoro's translation is valid only for the weakest of the considered behavioural equivalences, Boudol's encoding also respects stronger ones. One could hence argue that Boudol's translation is more faithful.

    Keywords: Process calculi, expressiveness, quality criteria for encodings, π-calculus

    Note: The material of the paper has been incorporated in 141.

    130. A Theory of Encodings and Expressiveness

    R.J. van Glabbeek (Data61, CSIRO)

    February/May 2018

    This paper proposes a definition of what it means for one system description language to encode another one, thereby enabling an ordering of system description languages with respect to expressive power. I compare the proposed definition with other definitions of encoding and expressiveness found in the literature, and illustrate it on a well-known case study: the encoding of the synchronous in the asynchronous π-calculus.

    Keywords: Expressiveness, encodings, languages, translations, compositionality, semantic equivalences, π-calculus.

    131. Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, Thessaloniki, Greece, 20th April 2018

    J.P. Gallagher (Roskilde University and IMDEA), R.J. van Glabbeek (Data61, CSIRO) & W. Serwe (INRIA), editors

    March 2018

    This volume contains the joint proceedings of MARS 2018, the third workshop on Models for Formal Analysis of Real Systems, and VPT 2018, the sixth international workshop on Verification and Program Transformation, held together on April 20, 2018 in Thessaloniki, Greece, as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software.

    MARS emphasises modelling over verification. It aims at discussing the lessons learned from making formal methods for the verification and analysis of realistic systems. Examples are:
    (1) Which formalism is chosen, and why?
    (2) Which abstractions have to be made and why?
    (3) How are important characteristics of the system modelled?
    (4) Were there any complications while modelling the system?
    (5) Which measures were taken to guarantee the accuracy of the model?

    We invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. Alternative formal descriptions of the systems presented at this workshop are encouraged, which should foster the development of improved specification formalisms.

    VPT aims to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. These interactions have been beneficial in both directions. On the one hand, methods and tools developed in the field of program transformation, such as partial deduction, partial evaluation, fold/unfold transformations, and supercompilation, are applied with success to verification, in particular to the verification of infinite state and parameterized systems. On the other hand, methods developed in program verification, such as model checking, abstract interpretation, SAT and SMT solving, and automated theorem proving, are used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.

    132. Analysing AWN-specifications using mCRL2 (extended abstract)

    R.J. van Glabbeek (Data61, CSIRO), P. Höfner (Data61, CSIRO) & Djurre van der Wal (Data61, CSIRO)

    July 2018

    We develop and implement a translation from the process Algebra for Wireless Networks (AWN) into the milli Common Representation Language (mCRL2). As a consequence of the translation, the sophisticated toolset of mCRL2 is now available for AWN-specifications. We show that the translation respects strong bisimilarity; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.

    Keywords: process algebra; AWN; wireless mesh networks; mobile ad-hoc networks; routing protocols; mCRL2; translation; bisimulation modulo renaming up to data congruence.

    xiii. Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk)

    R. J. van Glabbeek (Data61, CSIRO)

    September 2018

    A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent.

    In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however.

    This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.

    Keywords: Mutual exclusion, speed independence, concurrent reading and writing, liveness, justness.

    133. Progress, Justness and Fairness

    R.J. van Glabbeek (Data61, CSIRO) & P. Höfner (Data61, CSIRO)

    October 2018

    Fairness assumptions are a valuable tool when reasoning about systems. In this paper, we classify several fairness properties found in the literature and argue that most of them are too restrictive for many applications. As an alternative we introduce the concept of justness.

    Keywords: Survey paper; Fairness, Progress, Justness, Liveness, Labelled Transition Systems.

    134. Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours

    N. Fischer (Saarland U.) & R.J. van Glabbeek (Data61, CSIRO)

    October 2018

    In concurrency theory, weak bisimilarity is often used to relate processes exhibiting the same observable behaviour. The probabilistic environment gives rise to several generalisations; we study the infinitary semantics, which abstracts from a potentially unbounded number of internal actions being performed when something observable happens. Arguing that this notion yields the most desirable properties, we provide a sound and complete axiomatisation capturing its essence. Previous research has failed to achieve completeness in the presence of unguarded recursion, as only the finitary variant has been axiomatised, yet.

    Keywords: Axiomatisation, Process algebra, Probability, Recursion.

    135. Justness: A Completeness Criterion for Capturing Liveness Properties

    R. J. van Glabbeek (Data61, CSIRO)

    February 2019

    This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture relevant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.

    Keywords: Justness, progress, fairness, completeness criteria, liveness, distributed systems, process algebra, labelled transition systems with concurrency, CCS, broadcast communication, signals.

    136. A Process Algebra for Link Layer Protocols

    R.J. van Glabbeek (Data61, CSIRO), P. Höfner (Data61, CSIRO) and Michael Markl (U. Augsburg)

    March 2019

    We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.

    Keywords: Link layer protocols; CSMA/CA; virtual carrier sensing; packet delivery; process algebra; ALL.

    137. Reward Testing Equivalences for Processes

    R. J. van Glabbeek (Data61, CSIRO)

    July 2019

    May and must testing were introduced by De Nicola and Hennessy to define semantic equivalences on processes. May-testing equivalence exactly captures safety properties, and must-testing equivalence liveness properties. This paper proposes reward testing and shows that the resulting semantic equivalence also captures conditional liveness properties. It is strictly finer than both the may- and must-testing equivalence.

    Keywords: Reward testing, Semantic equivalences, Conditional liveness properties, Labelled transition systems, Process algebra, CCS, Axiomatisations, Recursion, Congruence, Divergence.

    Dedication: to Rocco De Nicola, on the occasion of his 65th birthday. Rocco's work has been a source of inspiration to my own.

    138. Ensuring Liveness Properties of Distributed Systems: Open Problems

    R. J. van Glabbeek (Data61, CSIRO)

    July 2019

    Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations they lead to false conclusions.

    This document presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models. The agenda also includes the development of a methodology and tools that allow successful application of this theory to the specification, analysis and verification of realistic distributed systems.

    Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating matching treatments of time and probability.

    Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.

    Keywords: Liveness, fairness, justness, progress, distributed systems, concurrency, process algebra, temporal logic, labelled transition systems, Petri nets, semantic equivalences, strong bisimulation, fair schedulers, mutual exclusion, expressiveness, routing protocols, wireless mesh networks, structural operational semantics, probabilistic processes, real-time, approximation induction principle, recursive specification principle.

    Note: An earlier version of this paper appeared as xii.

    139. On the Meaning of Transition System Specifications

    R.J. van Glabbeek (Data61, CSIRO)

    August 2019

    Transition System Specifications provide programming and specification languages with a semantics. They provide the meaning of a closed term as a process graph: a state in a labelled transition system. At the same time they provide the meaning of an n-ary operator, or more generally an open term with n free variables, as an n-ary operation on process graphs. The classical way of doing this, the closed-term semantics, reduces the meaning of an open term to the meaning of its closed instantiations. It makes the meaning of an operator dependent on the context in which it is employed. Here I propose an alternative process graph semantics of TSSs that does not suffer from this drawback.

    Semantic equivalences on process graphs can be lifted to open terms conform either the closed-term or the process graph semantics. For pure TSSs the latter is more discriminating.

    I consider five sanity requirements on the semantics of programming and specification languages equipped with a recursion construct: compositionality, applied to n-ary operators, recursion and variables, invariance under α-conversion, and the recursive definition principle, saying that the meaning of a recursive call should be a solution of the corresponding recursion equations. I establish that the satisfaction of four of these requirements under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics.

    Keywords: Structural operational semantics, transition system specifications, open terms, process graph semantics, compositionality.

    140. Proceedings 30th International Conference on Concurrency Theory,
    CONCUR 2019, Amsterdam, the Netherlands, August 27-30, 2019

    W.J. Fokkink (VU) & R.J. van Glabbeek (Data61, CSIRO), editors

    August 2019

    141. Stronger Validity Criteria for Encoding Synchrony

    R.J. van Glabbeek (Data61, CSIRO), U. Goltz (TU Braunschweig), C. Lippert (TU Braunschweig) & S. Mennicke (TU Braunschweig)

    November 2019

    We analyse two translations from the synchronous into the asynchronous π-calculus, both without choice, that are often quoted as standard examples of valid encodings, showing that the asynchronous π-calculus is just as expressive as the synchronous one. We examine which of the quality criteria for encodings from the literature support the validity of these translations. Moreover, we prove their validity according to much stronger criteria than considered previously in the literature.

    Keywords: Process calculi, expressiveness, translations, quality criteria for encodings, valid encodings, compositionality, operational correspondence, semantic equivalences, asynchronous π-calculus.

    Dedication: This paper is dedicated to Catuscia Palamidessi, on the occasion of her birthday. It has always been a big pleasure and inspiration to discuss with her.

    Note: This paper contains the material of 129.

    142. A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice (extended abstract)

    R.J. van Glabbeek (Data61, CSIRO), J.F. Groote (TU Eindhoven) & E.P. de Vink (TU Eindhoven)

    November 2019

    This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding notion of rooted branching probabilistic bisimilarity, an equational theory is proposed for a basic, recursion-free process language with non-deterministic as well as probabilistic choice. The proof of completeness of the axiomatization builds on the completeness of strong probabilistic bisimilarity on the one hand and on the notion of a concrete process, i.e. a process that does not display (partially) inert τ-moves, on the other hand. The approach is first presented for the non-deterministic fragment of the calculus and next generalized to incorporate probabilistic choice, too.

    Keywords: Process algebra, probabilistic processes, nondeterminism, branching bisimulation, complete axiomatisation.

    Dedication: to Catuscia Palamidessi, on the occasion of her 60th birthday.

    143. Cross-Chain Payment Protocols with Success Guarantees

    R.J. van Glabbeek (Data61, CSIRO), V. Gramoli (U. Sydney) & P. Tholoniat (U. Sydney)

    December 2019

    In this paper, we consider the problem of cross-chain payment whereby customers of different escrows—implemented by a bank or a blockchain smart contract—successfully transfer digital assets without trusting each other. Prior to this work, cross-chain payment problems did not require this success or any form of progress. We introduce a new specification formalism called Asynchronous Networks of Timed Automata to formalise such protocols. We present the first cross-chain payment protocol that ensures termination in a bounded amount of time and works correctly in the presence of clock skew. We then demonstrate that it is impossible to solve this problem without assuming synchrony, in the sense that each message is guaranteed to arrive within a known amount of time. Yet, we solve an eventually terminating weaker variant of this problem, where success is conditional on the patience of the participants, without assuming synchrony, and in the presence of Byzantine failures. We also discuss the relation with the recently defined cross-chain deals.

    Keywords: Cross-chain payment protocols, distributed systems, fault tolerance, blockchain, asynchronous networks of timed automata, asynchronous communication, clock skew, safety and liveness properties, cross-chain deals.

    Note: A 3-page summary of this paper appaers as 147.

    144. Failure Trace Semantics for a Process Algebra with Time-outs

    R.J. van Glabbeek (Data61, CSIRO)

    February/September 2020

    This paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra, in the sense that the progress of time is not quantified. Trace and failures equivalence fail to be congruences for this operator; their congruence closure is characterised as failure trace equivalence.

    Keywords: Concurrency, process algebra, time-outs, priority, CCSP, labelled transition systems, semantic equivalences, linear time, branching time, failure trace semantics, absolute expressiveness, full abstraction, safety properties, may testing.

    145. Formalising the Optimised Link State Routing Protocol

    R. Barry (UNSW), R.J. van Glabbeek (Data61, CSIRO) & P. Höfner (ANU)

    April 2020

    Routing protocol specifications are traditionally written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Formal methods techniques, such as process algebras, avoid these problems, thus leading to more precise and verifiable descriptions of protocols. In this paper we use the timed process algebra T-AWN for modelling the Optimised Link State Routing protocol (OLSR) version 2.

    Keywords: Wireless mesh networks, mobile ad-hoc networks, timed process algebra, AWN, routing protocols, OLSR.

    146. On Infinite Guarded Recursive Specifications in Process Algebra

    R.J. van Glabbeek (Data61, CSIRO) & C.A. Middelburg (U. of Amsterdam)

    May 2020

    In most presentations of ACP with guarded recursion, recursive specifications are finite or infinite sets of recursion equations of which the right-hand sides are guarded terms. The completeness with respect to bisimulation equivalence of the axioms of ACP with guarded recursion has only been proved for the special case where recursive specifications are finite sets of recursion equations of which the right-hand sides are guarded terms of a restricted form known as linear terms. In this note, we widen this completeness result to the general case.

    Keywords: process algebra, guarded recursion, completeness, infinitary conditional logic.

    147. Feasibility of Cross-Chain Payment with Success Guarantees

    R.J. van Glabbeek (Data61, CSIRO), V. Gramoli (U. Sydney) & P. Tholoniat (U. Sydney)

    May 2020

    We consider the problem of cross-chain payment whereby customers of different escrows—implemented by a bank or a blockchain smart contract—successfully transfer digital assets without trusting each other. Prior to this work, cross-chain payment problems did not require this success, or any form of progress. We demonstrate that it is possible to solve this problem when assuming synchrony, in the sense that each message is guaranteed to arrive within a known amount of time, but impossible to solve without assuming synchrony. Yet, we solve a weaker variant of this problem, where success is conditional on the patience of the participants, without assuming synchrony, and in the presence of Byzantine failures. We also discuss the relation with the recently defined cross-chain deals.

    Keywords: Cross-chain payment protocols, distributed systems, fault tolerance, blockchain, asynchronous networks of timed automata, asynchronous communication, clock skew, safety and liveness properties, cross-chain deals.

    Note: This is a 3-page summary of 143.

    148 Reactive Bisimulation Semantics for a Process Algebra with Time-Outs

    R.J. van Glabbeek (Data61, CSIRO)

    August 2020

    This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.

    Keywords: Concurrency, process algebra, time-outs, CCSP, labelled transition systems, reactive bisimulation semantics, modal characterisations, congruence, recursion, complete axiomatisations.

    Note: This paper has been published under a slightly different title as 159.

    149 Reactive Temporal Logic

    R.J. van Glabbeek (Data61, CSIRO)

    August 2020

    Whereas standard treatments of temporal logic are adequate for closed systems, having no run-time interactions with their environment, they fall short for reactive systems, interacting with their environments through synchronisation of actions. This paper introduces reactive temporal logic, a form of temporal logic adapted for the study of reactive systems. I illustrate its use by applying it to formulate definitions of a fair scheduler, and of a correct mutual exclusion protocol. Previous definitions of these concepts were conceptually much more involved or less precise, leading to debates on whether or not a given protocol satisfies the implicit requirements.

    Keywords: Concurrency, reactive systems, temporal logic, LTL, process algebra, labelled transition systems, Kripke structures, Petri nets, fair schedulers, mutual exclusion.

    150. Selected Papers of the 30th International Conference on Concurrency Theory (CONCUR 2019)

    W.J. Fokkink (VU) & R.J. van Glabbeek (Data61, CSIRO), editors

    February/March 2021

    151. Abstract Processes and Conflicts in Place/Transition Systems

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

    February 2021

    For one-safe Petri nets or condition/event-systems, a 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. Goltz and Reisig have generalised this concept for nets where places carry multiple tokens, by distinguishing tokens according to their causal history. However, this so-called individual token interpretation is often considered too detailed. Here we identify a subclass of Petri nets, called structural conflict nets, where no interplay between conflict and concurrency due to token multiplicity occurs. For this subclass, we define abstract processes as equivalence classes of Goltz-Reisig processes. We justify this approach by showing that there is a largest abstract process if and only if the underlying net is conflict-free with respect to a canonical notion of conflict.

    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—formalised as a largest abstract process. The "if" direction stems from 89, and "only if" is contributed here.

    The results of this paper appeared before in 90. However, there they were formulated differently, as in that paper we didn't have the canonical preorder $\sqsubseteq_1^\infty$ on Goltz-Reisig processes that is introduced here—inducing a partial order on abstract processes—and thus neither the concept of a largest abstract process. Our current proofs are conceptually much simpler than the ones in 90, as they are carried out directly on abstract processes, rather than via the auxiliary concepts of BD-runs and FS-runs.

    What is called "abstract process" above is called "BD-process" in the abstracts of 89 and 152.

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

    152. Abstract Processes in the Absence of Conflicts in General Place/Transition Systems

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

    April 2021

    Goltz and Reisig generalised Petri's concept of processes of one-safe Petri nets to general nets where places carry multiple tokens. BD-processes are equivalence classes of Goltz-Reisig processes connected through the swapping transformation of Best and Devillers; they can be considered as an alternative representation of runs of nets. Here we present an order respecting bijection between the BD-processes and the FS-processes of a countable net, the latter being defined—in an analogous way—as equivalence classes of firing sequences. Using this, we show that a countable net without binary conflicts has a (unique) largest BD-process.

    Note: The result that a Petri net $N$ without binary conflicts has a largest BD-process was obtained in 151 for the special case that $N$ is a structural conflict net. Here it is generalised to arbitrary countable nets. (It does not hold for arbitrary uncountable nets, although 151 includes the case of uncountable structural conflict nets).

    The above result appeared before in 90. However, there it was formulated differently, as in that paper we didn't have the canonical preorder $\sqsubseteq_1^\infty$ on Goltz-Reisig processes that was introduced in 151—inducing a partial order on BD-processes—and thus neither the concept of a largest BD-process. Our current proofs are conceptually simpler than the ones in 90, as they avoid the auxiliary concepts of BD-runs and FS-runs.

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

    153. Comparing the expressiveness of the π-calculus and CCS

    R.J. van Glabbeek (Data61, CSIRO)

    April 2021

    This paper shows that the π-calculus with implicit matching is no more expressive than CCSγ, a variant of CCS in which the result of a synchronisation of two actions is itself an action subject to relabelling or restriction, rather than the silent action τ. This is done by exhibiting a compositional translation from the π-calculus with implicit matching to CCSγ that is valid up to strong barbed bisimilarity.

    The full π-calculus can be similarly expressed in CCSγ enriched with the triggering operation of Meije.

    I also show that these results cannot be recreated with CCS in the role of CCSγ, not even up to reduction equivalence, and not even for the asynchronous π-calculus without restriction or replication.

    Finally I observe that CCS cannot be encoded in the $\pi$-calculus.

    Keywords: Process calculi, expressiveness, π-calculus, CCS, mobility, translations, valid encodings, compositionality, strong barbed bisimilarity.

    154. Coinductive Validity

    R.J. van Glabbeek (Data61, CSIRO)

    April 2021

    This note formally defines the concept of coinductive validity of judgements, and contrasts it with inductive validity. For both notions it shows how a judgement is valid iff it has a formal proof. Finally, it defines and illustrates the notion of a proof by coinduction.

    Keywords: Coinduction, Formal proof, Process Algebra.

    155. Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom

    R.J. van Glabbeek (Data61, CSIRO), P. Höfner (ANU) and R. Horne (U. Luxembourg)

    April 2021

    We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.

    Keywords: Session types, lock-freedom, fairness, justness, sound and complete type systems.

    156 Modelling Mutual Exclusion in a Process Algebra with Time-outs

    R.J. van Glabbeek (Data61, CSIRO)

    June 2021

    I show that in a standard process algebra extended with time-outs one can correctly model mutual exclusion in such a way that starvation-freedom holds without assuming fairness or justness, even when one makes the problem more challenging by assuming memory accesses to be atomic. This can be achieved only when dropping the requirement of speed independence.

    Keywords: Mutual exclusion, safe registers, overlapping reads and writes, atomicity, speed independence, reactive temporal logic, LTL, Kripke structures, progress, justness, fairness, safety properties, blocking, fair schedulers, process algebra, CCS, time-outs, labelled transition systems, Petri nets, asymmetric concurrency relations, Peterson's protocol.

    157. Enabling Preserving Bisimulation Equivalence

    R.J. van Glabbeek (Data61, CSIRO), P. Höfner (ANU) and W. Wang (ANU)

    July 2021

    Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.

    Keywords: Concurrency, bisimilarity, liveness properties, fairness assumptions, process algebra, justness, labelled transition systems with successors, CCS, broadcast communication, signals.

    158 CONCUR Test-Of-Time Award 2021

    N. Bertrand (Inria, Rennes), L. de Alfaro (UC Santa Cruz), R.J. van Glabbeek (Data61, CSIRO) C. Palamidessi (Inria, Paris) & N. Yoshida (Imperial College, London)

    July 2021

    This short article announces the recipients of the CONCUR Test-of-Time Award 2021.

    Keywords: Concurrency, CONCUR Test-of-Time Award.

    159 Reactive Bisimulation Semantics for a Process Algebra with Timeouts

    R.J. van Glabbeek (Data61, CSIRO)

    April 2022

    This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with timeout transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.

    Keywords: Concurrency, process algebra, time-outs, CCSP, labelled transition systems, reactive bisimulation semantics, modal characterisations, congruence, recursion, complete axiomatisations.

    Note: An extended abstract of this paper, as well as the full version with slightly different title, appeared as 148.

    160 Fair Must Testing for I/O Automata

    R.J. van Glabbeek (UNSW)

    September 2022

    The concept of must testing is naturally parametrised with a chosen completeness criterion or fairness assumption. When taking weak fairness as used in I/O automata, I show that it characterises exactly the fair preorder on I/O automata as defined by Lynch & Tuttle.

    Keywords: I/O automata, Must-testing, Fairness

    Dedication: to Frits Vaandrager, on the occasion of his 60th birthday.

    161 Just Testing

    R.J. van Glabbeek (U. Edinburgh)

    October 2022

    The concept of must testing is naturally parametrised with a chosen completeness criterion, defining the complete runs of a system. Here I employ justness as this completeness criterion, instead of the traditional choice of progress. The resulting must-testing preorder is incomparable with the default one, and can be characterised as the fair failure preorder of Vogler. It also is the coarsest precongruence preserving linear time properties when assuming justness.

    As my system model I here employ Petri nets with read arcs. Through their Petri net semantics, this work applies equally well to process algebras. I provide a Petri net semantics for a standard process algebra extended with signals; the read arcs are necessary to capture those signals.

    Keywords: Must-testing, justness, linear-time properties, Petri nets, process algebra.

    162. A Cancellation Law for Probabilistic Processes

    R.J. van Glabbeek (U. Edinburgh), J.F. Groote (TU Eindhoven) & E.P. de Vink (TU Eindhoven)

    August 2023

    We show a cancellation property for probabilistic choice. If µ ⊕ ρ and ν ⊕ ρ are branching probabilistic bisimilar, then µ and ν are also branching probabilistic bisimilar. We do this in the setting of a basic process language involving non-deterministic and probabilistic choice and define branching probabilistic bisimilarity on distributions. Despite the fact that the cancellation property is very elegant and concise, we failed to provide a short and naturalcombinatorial proof. Instead we provide a proof using metric topology. Our major lemma is that every distribution can be unfolded into an equivalent stable distribution, where the topological arguments are required to deal with uncountable branching.

    Keywords: Process algebra, probabilistic processes, nondeterminism, branching bisimulation, cancellation, sequential compactness.

    163. A Lean-Congruence Format for EP-Bisimilarity

    R.J. van Glabbeek (U. Edinburgh), P. Höfner (ANU) and W. Wang (ANU)

    September 2023

    Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.

    Keywords: Concurrency, bisimilarity, liveness properties, process algebra, labelled transition systems with successors, structural operational semantics, congruence.

    164. Shoggoth: A Formal Foundation for Strategic Rewriting

    X. Qin (U. Edinburgh), L. O'Connor (U. Edinburgh), R.J. van Glabbeek (U. Edinburgh), P. Höfner (ANU), O. Kammar (U. Edinburgh) & M. Steuwer (U. Edinburgh -> TU Berlin)

    November 2023

    Rewriting is a versatile and powerful technique used in many domains. Strategic rewriting allows programmers to control the application of rewrite rules by composing individual rewrite rules into complex rewrite strategies. These strategies are semantically complex, as they may be nondeterministic, they may raise errors that trigger backtracking, and they may not terminate.

    Given such semantic complexity, it is necessary to establish a formal understanding of rewrite strategies and to enable reasoning about them in order to answer questions like: How do we know that a rewrite strategy terminates? How do we know that a rewrite strategy does not fail because we compose two incompatible rewrites? How do we know that a desired property holds after applying a rewrite strategy?

    In this paper, we introduce Shoggoth: a formal foundation for understanding, analysing and reasoning about strategic rewriting that is capable of answering these questions. We provide a denotational semantics of System S, a core language for strategic rewriting, and prove its equivalence to our big-step operational semantics, which extends existing work by explicitly accounting for divergence. We further define a location-based weakest precondition calculus to enable formal reasoning about rewriting strategies, and we prove this calculus sound with respect to the denotational semantics. We show how this calculus can be used in practice to reason about properties of rewriting strategies, including termination, that they are well-composed, and that desired postconditions hold. The semantics and calculus are formalised in Isabelle/HOL and all proofs are mechanised.

    Keywords: Strategic rewriting, program transformation, weakest preconditions, semantics, mechanised formalisation.

    165. More on Maximally Permissive Similarity Control of Discrete Event Systems

    Yu Wang, Zhaohui Zhu, Rob van Glabbeek, Jinjin Zhang, Lixing Tan

    July 2024

    Takai proposed a method for constructing a maximally permissive supervisor for the similarity control problem (IEEE Transactions on Automatic Control, 66(7):3197-3204, 2021). This paper points out flaws in his results by providing a counterexample. Inspired by Takai's construction, the notion of a (saturated) (G, R)-automaton is introduced and metatheorems concerning (maximally permissive) supervisors for the similarity control problem are provided in terms of this notion. As an application of these metatheorems, the flaws in Takai's work are corrected.

    Keywords: Discrete event systems, supervisory control, simulation relation, maximally permissive supervisor.

    166. Branching Bisimilarity for Processes with Time-outs

    Gaspard Reghem (ENS Paris-Saclay) & Rob J. van Glabbeek (University of Edinburgh)

    August 2024

    This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.

    Keywords: Concurrency, process algebra, time-outs, CCSP, labelled transition systems, reactive branching bisimulation semantics, modal characterisations, congruence, recursion, complete axiomatisations.

    167. Concrete Branching Bisimilarity for Processes with Time-outs

    Gaspard Reghem (ENS Paris-Saclay) & Rob J. van Glabbeek (University of Edinburgh)

    August 2024

    This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.

    Keywords: Concurrency, process algebra, time-outs, CCSP, labelled transition systems, reactive branching bisimulation semantics, modal characterisations, congruence, recursion, complete axiomatisations.

    Note: Whereas the bisimilarity of 166 elides timeouts, in the sense that it satisfies $a.\mbox{t}.b.0 = a.\mbox{t}.\mbox{t}.b.0$, just like branching bisimilarity elides $\tau$-transitions, the one of this paper instead treats time-outs more like visible actions. We obtained 167 from 166 by systemically suppressing this eliding feature, thereby obtaining simpler definitions and proofs.

    168. Semantics for Linear-time Temporal Logic with Finite Observations

    Rayhana Y. Amjad (U. Edinburgh), Liam O'Connor (ANU) & Rob J. van Glabbeek (U. Edinburgh)

    October 2024

    LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by contrast, gives a full model-based inductive accounting of the semantics of LTL3, in terms of families of definitive prefix sets. We show that our definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby show that our semantics of LTL3 directly correspond to the semantics of conventional LTL. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics. All of our definitions and proofs are mechanised in Isabelle/HOL.

    Keywords: Temporal Logic, runtime monitoring, LTL.

    Only papers i, 7, 8, 10, 16, 20 and 21 are not available electronically through a link from this webpage.
    (Moreover, 7, 10, 16, 20 and 21 are included in 17 and 41, which are available.)

    SFB-reports of the TU Munich (19-23) can be obtained from:

    The original version of my dissertation (17) 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