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.
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.
- Report nr. 3, Mathematical Institute, University of Leiden,
The Netherlands.
-
Available as scanned pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#0
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
- CWI report CS-R8624 (i.e. Report CS-R8624, Centre for
Mathematics and Computer Science, Amsterdam 1986).
Available as Scanned PDF.
-
Theoretical Computer Science 177(2), 1997, pp. 329-349.
Free download from Elsevier at the above link.
-
Scanned PDF. This is a small modification of the CWI
report whose content equals that of the TCS publication.
Additionally it has a marginal note taking back the
statement that in general abstraction and recursion commute.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#1
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
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
- CWI report CS-R8701. Available as
Scanned PDF.
- Extended abstract in:
Automata, Languages and Programming,
Proceedings 14th International Colloquium, ICALP 87,
Karlsruhe, Germany, July 1987 (Th. Ottman, ed.), LNCS 267,
Springer-Verlag, 1987, pp. 84-94. Available as
Scanned PDF.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#3
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
- CWI report CS-R8716. Available as
Scanned PDF.
- In: Proceedings Seventh Conference on Foundations of Software
Technology and Theoretical Computer Science, Pune, India,
December 1987 (K.V. Nori, ed.), LNCS 287, Springer-Verlag,
1987, pp. 153-172. Available as
Scanned PDF.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#4
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
- CWI report CS-R8721. Available as
Scanned PDF.
- Fundamenta Informaticae XII, 1989, pp. 221-242. Available as
Scanned PDF.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#5
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:
- the occurrence net equivalence of Nielsen, Plotkin and Winskel;
- bisimulation equivalence, which leads to a model which
is isomorphic to the graph model of Baeten, Bergstra & Klop;
- the concurrent bisimulation equivalence, which is also
described by Nielsen & Thiagarajan, and Goltz;
- 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.
- Unfinished
- Extended abstract in: Proceedings PARLE conference,
Eindhoven, The Netherlands 1987, Vol. II (Parallel Languages)
(J.W. de Bakker, A.J. Nijman & P.C. Treleaven, eds.),
LNCS 259, Springer-Verlag, 1987, pp. 224-242.
-
Available as scanned pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#6
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.
- Syllabus processemantieken, deel 2. Handwritten manuscript, in Dutch.
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.
- CWI report CS-R8821
- Appeared as Chapter II of my Ph.D. Thesis.
- Extended abstract in: Algebraic Methods: Theory, Tools and
Applications (M. Wirsing & J.A. Bergstra, eds.), LNCS 394,
Springer-Verlag, 1989, pp. 465-506.
Available as Scanned PDF.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#7
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.
- Arbeitspapiere der GMD 320, Sankt Augustin, Germany 1988.
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.
- In 8, pp. 18-19.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#graph
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.
- CWI report CS-R8838
Available as Scanned PDF.
-
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#9
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.
- Arbeitspapiere der GMD 366, Sankt Augustin, Germany 1989.
- Appeared in Chapter VI of my Ph.D. Thesis.
- Extended abstract in: Proceedings Mathematical Foundations
of Computer Science 1989 (MFCS), Poræbka-Kozubnik, Poland,
August/September 1989 (A. Kreczmar & G. Mirkowska, eds.),
LNCS 379, Springer-Verlag, 1989, pp. 237-248.
Available as Scanned PDF.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#10
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.
- CWI report CS-R8911
Available as Scanned PDF.
- Appeared in Chapter III of my Ph.D. Thesis.
- In: Information Processing 89, Proceedings of the IFIP 11th
World Computer Congress, San Francisco, USA 1989 (G.X.
Ritter, ed.), Elsevier Science Publishers B.V. (North
Holland), 1989, pp. 613-618.
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.
- CWI report CS-R8922.
Available as Scanned PDF.
- Appeared as Section 6 of Chapter III of my
Ph.D. Thesis.
- In: J.W de Bakker, 25 jaar semantiek, liber amicorum,
Centre for Mathematics and Computer Science, Amsterdam
1989, pp. 247-252.
Available as Scanned PDF.
- and in: Proceedings AMAST Conference,
Iowa City, USA 1989, pp. 197-201.
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.
- In: J.W de Bakker, 25 jaar semantiek, liber amicorum,
Centre for Mathematics and Computer Science, Amsterdam
1989, pp. 243-246.
Available as Scanned PDF.
R.J. van Glabbeek (CWI) & U. Goltz (GMD)
July 1989
In this note we argue:
- that there are several semantic equivalences based on
partial orders which are not preserved by action refinement
(namely when taking the choice structure of systems into account);
- that nevertheless a "branching time" partial order
equivalence can be found that is preserved under refinement;
- but that, in order to achieve preservation under refinement
it is not necessary to employ partial order semantics:
there exists equivalences that abstract from the causal
structure of concurrent systems and are still preserved
under refinement.
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.
- CWI note CS-N8901.
Available as Scanned PDF.
- Appeared as Chapter V of my Ph.D. Thesis.
- Bulletin of the EATCS 38, 1989, pp. 154-163.
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.
- CWI report CS-R9002.
-
Available as scanned pdf.
- Appeared as Chapter VII of my Ph.D. Thesis.
- In: Programming Concepts and Methods, Proceedings of a IFIP
Working Group 2.2/2.3 Working Conference, Sea of Galilee,
Israel, 2-5 April 1990 (M. Broy & C.B. Jones, eds.),
Elsevier Science Publishers B.V. (North-Holland), 1990, pp.
27-52.
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.
- Arbeitspapiere der GMD 428, Sankt Augustin, Germany 1990.
- Appeared as Chapter IV of my Ph.D. Thesis.
- In: Stepwise Refinement of Distributed Systems: Models,
Formalism, Correctness, Proceedings REX Workshop, Mook, The
Netherlands, May/June 1989 (J.W. de Bakker, W.-P. de Roever
& G. Rozenberg, eds.), LNCS 430, Springer-Verlag, 1990,
pp. 267-300.
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.
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.
- CWI report CS-R9020.
Available as Scanned PDF (5.5MB).
- In: Proceedings 5th Annual IEEE Symposium on Logic in
Computer Science, LICS 90, Philadelphia, USA, IEEE
Computer Society Press, Los Alamitos 1990, pp. 130-141.
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.
- CWI report CS-R9029 and TUM report I9025 (i.e. Report
TUM-I9025, Technical University of Munich, Munich, Germany
1990) (= SFB-Bericht Nr. 342/13/90 A).
Available as Scanned PDF (11MB).
- Appeared as Chapter I of my Ph.D. Thesis.
- Extended abstract in: Proceedings CONCUR '90, Theories of
Concurrency: Unification and Extension, Amsterdam, The
Netherlands, August 1990 (J.C.M. Baeten & J.W. Klop, eds.),
LNCS 458, Springer-Verlag, 1990, pp. 278-297.
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.
- TUM report I9024 (= SFB-Bericht Nr. 342/12/90 A).
- An earlier version appeared as Chapter VI of my Ph.D. Thesis.
- In: Semantics of Systems of Concurrent Processes,
Proceedings LITP Spring School on Theoretical Computer
Science, La Roche-Posay, France, April 1990 (I.
Guessarian, ed.), LNCS 469, Springer-Verlag, 1990, pp.
309-333.
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.
- TUM report I9044 (= SFB-Bericht Nr. 342/23/90 A).
- Abstract in: Proceedings 3rd
Workshop on Concurrency and Compositionality, Goslar, March
5-8, 1991 (E. Best & G. Rozenberg, eds.), GMD-Studien
Nr. 191, Sankt Augustin, Germany 1991, pp. 113-116.
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.
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.
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.
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.
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.
- Report No. STAN-CS-93-1470, Department of computer Science,
Stanford University, CA 94305, USA.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/complete.dvi.gz (also as
tex,
ps
and pdf).
- In: Proceedings Mathematical Foundations of Computer
Science 1993 (MFCS), Gdansk, Poland, August/September 1993
(A.M. Borzyszkowski & S. Soko
lowski,
editors.), LNCS 711, Springer-Verlag, 1993, pp. 473-484.
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.
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.
- Report No. STAN-CS-93-1486
- Available at http://rvg.web.cse.unsw.edu.au/pub/branching.tex.gz,
http://rvg.web.cse.unsw.edu.au/pub/branching.dvi.gz,
http://Boole.stanford.edu/pub/branching.ps.gz,
http://Boole.stanford.edu/pub/branching.pdf.gz and
http://Theory.stanford.edu/~rvg/branching.
- In: The Concurrency Column (M. Nielsen, ed.),
Bulletin of the EATCS 53, June 1994, pp. 190-198.
- In: Current Trends in Theoretical Computer Science;
Entering the 21st Century (G. Paun, G. Rozenberg &
A. Salomaa, eds.), World Scientific, 2001, pp. 469-479.
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.
- Available at
http://Boole.stanford.edu/pub/sos.ps.gz. Also as
pdf.
- In: Proceedings of the Third International Conference on
Algebraic Methodology and Software Technology (AMAST'93),
Twente, The Netherlands, June 1993, (M. Nivat, C. Rattray,
T. Rus & G. Scollo, eds.), Workshops in Computing,
Springer-Verlag, 1993, pp. 75-82.
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
- Technical Report UBLCS-93-26, Laboratory for Computer
Science, University of Bologna
- Available at
ftp://ftp.cs.unibo.it/pub/TR/UBLCS/1993/93-26.ps.gz and
http://rvg.web.cse.unsw.edu.au/pub/axiomst.dvi.gz (also as
tex,
ps
and pdf).
- In: Proceedings IFIP Working Conference on Programming
Concepts, Methods and Calculi, San Miniato, Italy, June 1994
(E.-R. Olderog, ed.), Elsevier Science Publishers B.V.
(North-Holland), 1994, pp. 169-188.
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.
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.
- Available as
pdf,
dvi,
ps and
tex source.
- In: ACP94, Workshop on Algebra of Communicating Processes,
Utrecht, The Netherlands, May 1994, (A. Ponse, C. Verhoef &
S.F.M. van Vlijmen, eds.), Workshops in
Computing, Springer-Verlag, 1994, pp. 188-217.
- Draft full version available on request.
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.
- Report
STAN-CS-TN-95-16
- Available at
http://rvg.web.cse.unsw.edu.au/pub/negative.dvi.gz (also as
tex,
ps,
pdf and
gif).
- Extended abstract in: Automata, Languages and Programming,
Proceedings 23th International Colloquium, ICALP '96,
Paderborn, Germany, July 1996 (F. Meyer auf der Heide &
B. Monien, eds.), LNCS 1099, Springer, 1996, pp. 502-513.
- Extended abstract available as
dvi,
tex,
ps
and pdf.
- A mild revision with added emphasis on 3-valued
interpretations appeared as 53.
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.
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.
- Report CS-R9553, CWI, Amsterdam.
Available as Scanned PDF.
- Updated version, January 1997, available at
http://boole.stanford.edu/pub/split.pdf.
-
Information and Computation 136(2), 1997, pp. 109-142.
- Abstract in: Proceedings 3rd
Workshop on Concurrency and Compositionality, Goslar, March
5-8, 1991 (E. Best & G. Rozenberg, eds.), GMD-Studien
Nr. 191, Sankt Augustin, Germany 1991, pp. 117-121.
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.
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.
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.
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.
- In: Semantics of Concurrent Systems - Foundations and Applications
(M. Droste, E.-R. Olderog, B. Steffen & G. Winskel, eds.),
Dagstuhl-Seminar-Report 144, Internationales Begegnungs- und
Forschungszentrum für Informatik Schloss Dagstuhl,
Postfach 15 11 50, D-66041 Saarbrücken, Germany 1996, pp. 14-15.
- Available here.
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:
- The current axiomatizations generalize to full CCS, whereas
the prefix iteration approach does not allow an elimination
theorem for an asynchronous parallel composition operator.
- 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.
- Report
STAN-CS-TN-97-57, Department of Computer Science,
Stanford University, CA 94305, USA 1997.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/flat.dvi.gz (also as
tex,
pdf,
A4.ps and
US.ps).
- Archived at http://arxiv.org/abs/cs/9810008.
- In: Proceedings CONCUR '97, Warsaw, Poland, July 1997
(A. Mazurkiewicz & J. Winkowski, eds.), LNCS 1243,
Springer, 1997, pp. 228-242.
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.
- In: Information Systems as Reactive Systems (H.-D. Ehrich,
U. Goltz & J. Meseguer, eds.), Dagstuhl-Seminar-Report 200,
Internationales Begegnungs- und Forschungszentrum für Informatik
Schloss Dagstuhl, Postfach 15 11 50, D-66041 Saarbrücken, Germany
1998, page 12.
- Available here.
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.
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.
- Original version:
Arbeitsberichte des Instituts für Wirtschaftsinformatik
12, Universität Koblenz-Landau, Germany 1998.
- Java applet,
bringing SA terms into normal form.
- Updated
version:
Report
STAN-CS-TN-98-87, Department of Computer Science,
Stanford University, CA 94305, USA 1998.
Available as postscript and PDF.
- Also available at
http://Boole.stanford.edu/pub/sa.ps.gz and at
http://Boole.stanford.edu/pub/sa.pdf.gz.
The postscript file may not be readable with old
versions of ghostview; however, it should print fine.
- Slightly condensed version of the latter in:
Proceedings of the Seventh International Conference on
Algebraic Methodology and Software Technology (AMAST '98),
Amazonia, Brazil, January 1999 (A.M. Haeberer, ed.),
LNCS 1548, Springer, 1999, pp. 278-292.
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.
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.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/concur99.dvi.gz (also as
tex,
ps
and pdf).
- In Proceedings CONCUR '99, 10th International
Conference on Concurrency Theory, Eindhoven, The
Netherlands, August 1999 (J.C.M. Baeten & S. Mauw, eds.),
LNCS 1664, Springer, 1999, pp. 21-27.
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.
R.J. van Glabbeek (Stanford)
December 6, 1999
Keywords: Counting, ordinal numbers, cardinal numbers,
inclusive versus exclusive counting, millennium, calendar.
C. Palamidessi (Pennsylvania State U.), J. Parrow
(Royal Institute of Technology, Sweden) & R.J. van Glabbeek (Stanford)
January 2000
Keywords: Concurrency, expressiveness.
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.
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.
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.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/bisimulation.dvi.gz
(also as
tex,
ps and
pdf; the source is
tex.pic).
- Originally written for the forgotten Encyclopedia of Distributed
Computing (J.E. Urban & P. Dasgupta, eds.), Kluwer.
- "Further reading" added November 2010. Available as
ps,
pdf,
dvi and
tex file.
- In the
Encyclopedia of Parallel Computing (D. Padua, ed.), Part 2,
Springer, 2011, pp. 136-139.
R.J. van Glabbeek (Stanford)
February 23, 2001
Keywords: Decidability, formal language, algorithms, halting,
enumerability, recognizability
R.J. van Glabbeek (Stanford)
February 23, 2001
Keyword: undefinable languages.
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.
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.
- Available at
http://boole.stanford.edu/pub/token.pdf.gz (also
as
postscript, for previewing only).
- In: Proceedings 23rd International
Conference on Application and Theory of Petri Nets,
Adelaide, Australia, June 2002 (J. Esparza & C. Lakos, eds.),
LNCS,
2360, Springer, 2002, pp. 394-413.
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.
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.
- Available at
http://boole.stanford.edu/pub/query.ps.gz (also as
tex source
and as pdf).
- In:
Proceedings International Conference on Business Process Management,
BPM 2003, Eindhoven, The Netherlands, June 2003
(W.M.P. van der Aalst, A.H.M. ter Hofstede & M. Weske, eds.),
LNCS 2678,
Springer, 2003, pp 184-199.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#49
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.
- A preliminary version of some of the
material in this paper was presented in a talk at
the workshop Linear Logic 2002, Copenhagen.
- In: Proceedings 18th Annual IEEE Symposium on Logic in
Computer Science, LICS 2003, Ottawa, Canada, June 2003, IEEE
Computer Society Press, Los Alamitos 2003, pp. 1-10.
- Available at
http://Boole.stanford.edu/pub/mallnets-lics-with-proofs.ps.gz
(also as
tex
and pdf).
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#50
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.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/hml.dvi.gz (also as
tex,
ps
and pdf).
- In: Proceedings 14th International Symposium on Fundamentals
of Computation Theory, FCT 2003, Malmö, Sweden, August 2003
(A. Lingas & B.J. Nilsson, eds.),
LNCS 2751,
Springer, 2003, pp. 412-422.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#51
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
- all denotable event structures are bundle event structures,
- upon adding an infinitary parallel composition all
bundle event structures are denotable,
- without it every finite bundle event structure can be denoted,
- as well as every countable prime event structure with
binary conflict.
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.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/bundle.dvi.gz (also as
tex,
ps
and pdf).
- In: Proceedings 14th International Conference on Concurrency Theory,
CONCUR 2003, Marseilles, France, September 2003 (R. Amadio & D. Lugiez, eds.),
LNCS 2761,
Springer, 2003, pp. 57-71.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#52
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.
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.
- In: Slide Reprints from the Workshop on Process Algebra:
Open Problems and Future Directions, PA '03, Bologna,
Italy, July 2003 (L. Aceto, Z. Ésik, W.J. Fokkink &
A. Ingólfsdóttir, eds.),
BRICS notes NS-03-3,
Department of Computer Science, University of Aarhus,
Denmark, pp. 59-63.
- Available at http://www.cs.auc.dk/~luca/BICI/SLIDES-PA03/vanglabbeek.pdf.
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.
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.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/resolv.dvi.gz (also as
tex,
ps
and pdf).
- In: Proceedings 29th International Symposium on Mathematical Foundations
of Computer Science (MFCS 2004), Prague, Czech Republic, August 2004
(J. Fiala, V. Koubek & J. Kratochvíl, eds.),
LNCS 3153, Springer, 2004, pp. 550-561.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#55
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.
-
Electronic Notes in Theoretical Computer Science 128(2),
April 2005: Proceedings of the 11th International Workshop
on Expressiveness in Concurrency, EXPRESS 2004
(J.C.M. Baeten & F. Corradini, eds.), pp. 5-34.
- My original submission to ENTCS, November 2004, same
content as above, as pdf file.
- Final version, April 2005, available at
http://Boole.stanford.edu/pub/express-ea.pdf (also as
tex,
dvi,
and ps).
In footnote 5 this version corrects an error found in the
versions above.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#56
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.
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.
- Available at
http://rvg.web.cse.unsw.edu.au/pub/cool-ea.dvi.gz (also as
tex,
ps
and pdf).
© Springer-Verlag Berlin Heidelberg 2005
- In: Proceedings International Colloquium on Theoretical
Aspects of Computing, ICTAC05, Hanoi, Vietnam, October 2005
(D.V. Hung & M. Wirsing, eds.),
LNCS 3722,
Springer, 2005, pp. 318-333.
- Submission (same as above but with appendix
for referees, containing the proofs), as
pdf,
ps,
dvi and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#58
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.
- Available at
http://Boole.stanford.edu/pub/individual.ps.gz (also as
tex,
dvi
and pdf).
© Springer-Verlag Berlin Heidelberg 2005
- In: Proceedings 16th International Conference on
Concurrency Theory, CONCUR 2005, San Francisco, USA, August 2005
(M. Abadi & L. de Alfaro, eds.),
LNCS 3653,
Springer, 2005, pp. 323-337.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#59
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.
- Available as
dvi,
ps,
pdf and
tex file.
- In: Short Contributions from the Workshop on
Algebraic Process Calculi: The First Twenty Five Years and
Beyond, PA '05, Bertinoro, Italy, August 2005
(Luca Aceto and Andrew D. Gordon, editors),
BRICS Note NS-05-3,
Department of Computer Science, University of Aarhus,
Denmark 2005, pp. 112-113.
-
Electronic Notes in Theoretical Computer Science 162,
2006, pp. 173-175.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#60
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.
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.
- Preliminary version in: Participants Proceedings Structural
Operational Semantics 2005, Lisbon, Portugal, June 2005. Available as
dvi,
ps,
pdf and
tex file.
- Final version, October 2005, available as
dvi,
ps,
pdf and
tex file.
-
Electronic Notes in Theoretical Computer Science 156(1),
May 2006: Proceedings of the Second Workshop on Structural
Operational Semantics, SOS 2005, Lisbon, Portugal
(P. Mosses and I. Ulidowski, eds.), pp. 97-113.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#62
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.
- Available at
http://Boole.stanford.edu/pub/express.pdf (also as
tex,
dvi,
and ps).
- Theoretical Computer Science 368(1-2), 2006, pp. 169-194.
- Elsevier did a failed attempt to publish this paper
in
Theoretical Computer Science 356(3), 2006, pp. 265-290.
The figures in that publication are mangled.
Elsevier corrected this mistake in Erratum to "On the
expressiveness of higher dimensional automata",
Theoretical Computer Science 368(1-2), 2006,
pp. 168-194. Pages 169-194 of this erratum contain the
paper itself, with unmangled figures.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#63
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.
- In: Preliminary Proceedings of the Workshop on Geometry and
Topology in Concurrency, GETCO '05, San Francisco, USA,
August 2005 (Patrick Cousot, Lisbeth Fajstrup, Eric
Goubault, Maurice Herlihy, Kim G. Larsen & Martin Rauen, eds.)
BRICS Note NS-05-5,
Department of Computer Science, University of Aarhus,
Denmark 2005, page 1.
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.
- Preliminary report presented at the Fourth International
Symposium on Formal Methods for Components and Objects,
FMCO 2005, Amsterdam, The Netherlands, 3 November 2005.
Available as
dvi,
ps,
pdf and
tex file.
- Final report (hardly different from the above), April 2006,
in Revised Lectures Fourth International Symposium on
Formal Methods for Components and Objects, FMCO '05,
Amsterdam, The Netherlands, November 2005 (F.S. de Boer,
M.M. Bonsangue, S. Graf & W.-P. de Roever, eds.), LNCS
4111, Springer, 2006, pp. 195-218. Available as
dvi,
ps,
pdf and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#64
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.
- Available at
http://Boole.stanford.edu/pub/jwk.ps.gz (also as
tex,
dvi
and pdf).
© Springer-Verlag Berlin Heidelberg 2005
- In: Processes, Terms and Cycles: Steps on the Road to Infinity:
Essays Dedicated to Jan Willem Klop on the Occasion of His
60th Birthday (Aart Middeldorp, Vincent van Oostrom, Femke
van Raamsdonk & Roel de Vrijer, eds.), LNCS 3838,
Springer, 2005, pp. 26-39.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#65
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.
- Available as
ps,
pdf and
tex file.
- In: Proceedings 17th International Conference on
Concurrency Theory, CONCUR 2006, Bonn, Germany, August 2006
(C. Baier & H. Hermanns, eds.)
LNCS 4137,
Springer, 2006, pp. 126-141.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#66
R.J. van Glabbeek (NICTA), B. Luttik (TU Eindhoven)
& N. Trčka (TU Eindhoven)
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.
R.J. van Glabbeek (NICTA) & P.D. Mosses (Swansea U.), editors
August 2006
R.J. van Glabbeek (NICTA) & P.D. Mosses (Swansea U.), editors
November 2006
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.
-
Preliminary report in the original Gordon D. Plotkin
Festschrift (1 copy only) offered to Gordon Plotkin on his
60th birthday.
- Available as
pdf,
ps,
dvi and
tex file.
- In: Computation, Meaning, and Logic: Articles dedicated to
Gordon Plotkin (L. Cardelli, M. Fiore and G. Winskel, eds.),
Electronic Notes in Theoretical Computer Science 172, 2007,
pp. 359-397.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#69
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.
- Available as
pdf and
tex file.
- In: Proceedings 16th European Symposium on Programming,
ESOP 2007, Braga, Portugal, 24 March – 1 April, 2007
(R. De Nicola, ed.),
LNCS 4421,
Springer, 2007, pp. 363-378.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#70
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.
- Available as
dvi,
ps,
pdf and
tex file.
- In: Proceedings 22nd Annual IEEE Symposium on Logic in
Computer Science, LICS 2007, Wroclaw, Poland, July 2007, IEEE
Computer Society Press, Los Alamitos 2007, pp. 313-322.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#71
R.J. van Glabbeek (NICTA) & M. Hennessy (U. Sussex), editors
June 2007
R.J. van Glabbeek (NICTA) & M. Hennessy (U. Sussex), editors
September 2007
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.
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.
- CS-Report 08-06, Eindhoven University of Technology, 2008; available as
ps,
pdf and
tex file.
- Extended abstract in: Proceedings 20th International Conference on
Computer Aided Verification (CAV 2008), Princeton, USA, July 2008
(A. Gupta & S. Malik, eds.),
LNCS 5123,
Springer, 2008, pp. 517-529.
- Extended abstract available as
ps,
pdf and
tex file.
© Springer-Verlag Berlin Heidelberg 2008
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#74
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.
- CS-Report 08-14, Eindhoven University of Technology, 2008; available as
pdf,
ps and
tex file.
- Extended abstract in: Proceedings Thirteenth International Conference on
Implementation and Application of Automata (CIAA 2008),
San Francisco, California, USA, July 2008 (O.H. Ibarra & B. Ravikumar, eds.),
LNCS 5148,
Springer, 2008, pp. 161-170.
- Extended abstract available as
ps,
pdf and
tex file.
© Springer-Verlag Berlin Heidelberg 2008
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#75
R.J. van Glabbeek (NICTA) & P.D. Mosses (Swansea U.), editors
June 2008
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.
- Technical Report 2008-03, Technical University of Braunschweig.
- Available as
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/0901.0043.
- Extended abstract in: Pre-proceedings of the
1st
Interaction and Concurrency Experience,
ICE '08: Synchronous and Asynchronous Interactions in Distributed Systems,
Reykjavik, Iceland, July 2008 (F. Bonchi, D. Grohmann, P. Spoletini,
A. Troina & E. Tuosto, eds.), available at
http://ice08.dimi.uniud.it/doku.php?id=ice08:programme.
- Extended abstract in: Proceedings of the
First Interaction and Concurrency Experiences Workshop (ICE 2008),
Reykjavik, Iceland, July 2008 (F. Bonchi, D. Grohmann, P. Spoletini,
A. Troina & E. Tuosto, eds.),
Electronic Notes in Theoretical Computer Science
229(3), 2009, pp. 77-95.
- Extended abstract available as
ps,
pdf and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#77
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.
- Technical Report 2008-04, Technical University of Braunschweig.
- Available as
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/0901.0048.
- Extended abstract in: Proceedings 33rd International Symposium on
Mathematical Foundations of Computer Science (MFCS 2008),
Toruń, Poland, August 2008 (E. Ochmański & J. Tyszkiewicz, eds.),
LNCS 5162,
Springer, 2008, pp. 16-35.
- Extended abstract available as
ps,
pdf and
tex file.
© Springer-Verlag Berlin Heidelberg 2008
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#78
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.
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
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.
- Available as
dvi,
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/0810.4904.
- Extended abstract in Proceedings 35th Conference on
Current Trends in Theory and Practice of Computer Science,
Špindlerův Mlýn, Czech Republic, January 2009
(M. Nielsen, A. Kucera, P. Bro Miltersen, C. Palamidessi,
P. Tuma & F. Valencia, eds.),
LNCS 5404,
Springer, pp. 167-180.
- Extended abstract available as
dvi,
ps,
pdf and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#81
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
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.
- Available as
dvi,
ps,
pdf and
tex file.
- In: Proceedings 20th International Conference on Concurrency
Theory, CONCUR 2009, Bologna, Italy, September 2009
(M. Bravetti & G. Zavattaro, eds.),
LNCS 5710, Springer, pp. 274-288.
- Draft full version available as
pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#83
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.
- May-testing equivalence is fully abstract for safety properties.
- Must testing is fully abstract for liveness properties
(w.r.t. abstraction, renaming and interleaving) [DH84].
- The may-testing preorder as stated is less useful;
its inverse is fully abstract for safety properties.
- 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.
- I present a finer semantics that is fully abstract for safety
and conditional liveness properties w.r.t. abstraction and interleaving.
- 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.
- Due to the use of interleaving operators, must-testing and
related semantics make distinctions
that are wholly unobservable when using merely parallel composition.
- 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.
- Copies of slides. Invited talk for IFIP WG 1.8 at CONCUR 2009 in Bologna.
Available as
pdf.
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.
- Available as
dvi,
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/1007.5488.
- In: Reflections on the Work of C.A.R. Hoare
(C.B. Jones, A.W. Roscoe & K.R. Wood, eds.), History of
Computing, Springer, 2010, pp. 333-369.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#84
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.
- Available as
dvi,
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/1007.5491.
- In: Proceedings TCS 2010, IFIP AICT 323, September 2010
(C.S. Calude & V. Sassone, eds.), Springer, pp. 32-52.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#85
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.
- Available as
dvi,
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/1007.5188.
- Extended abstract in: Proceedings 17th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR),
Yogyakarta, Indonesia, October 2010 (C.G. Fermüller &
A. Voronkov, eds.), LNCS 6397, Springer, 2010, pp. 278-293.
- Extended abstract available as
dvi,
ps,
pdf and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#86
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.
- Available as
dvi,
ps,
pdf and
tex file.
- In: Proceedings Ninth Workshop on Quantitative Aspects of
Programming Languages, QAPL 2011, Saarbrücken, Germany,
April 2011 (M. Massink & G. Norman, eds.),
Electronic
Proceedings in Theoretical Computer Science 57, Open Publishing
Association, 2011, pp. 61-73,
doi: 10.4204/EPTCS.57.5
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#87
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.
- Available as
pdf,
ps,
dvi and
tex file.
- Theoretical Computer Science 412(28), pp. 3283-3302, 2011,
doi:
10.1016/j.tcs.2011.02.036
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#88
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:
- We introduce the Petri net class of structural conflict nets (SCN).
- On SCNs, processes modulo Best/Devillers swapping give a satisfying semantics.
- This semantics adheres to the collective token interpretation and respects causality.
Note: This paper ends with an open question that is
answered in 90.
Keywords: Concurrency, Petri nets, PT-systems, causal semantics, processes.
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.
- Informatik Bericht Nr. 2011-06, Institut für
Programmierung und Reaktive Systeme, TU Braunschweig, Germany 2011.
- Available as
pdf,
ps and
tex file.
- Archived at http://arxiv.org/abs/2103.00729.
- Extended abstract in: Proceedings 22th International Conference on Concurrency
Theory, CONCUR 2011, Aachen, Germany, September 2011
(J.-P. Katoen & B. König, eds.), LNCS 6901, Springer, 2011, pp. 43-59.
- Extended abstract available as
pdf and
ps.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#90
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.
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.
- Available as
dvi,
ps,
pdf and
tex file.
- Information and Computation 214, 2012, pp. 59-85,
doi:10.1016/j.ic.2011.10.011
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#92
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.
- Available as
pdf,
ps and
tex file.
- In: Programming Languages and Systems, Proceedings 21st
European Symposium on Programming (ESOP'12); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2012), Tallinn, Estonia, March/April 2012
(Helmut Seidl, ed.), LNCS 7211, Springer, 2012, pp. 295-315.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#93
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.
- Available as
pdf.
- In: Proceedings 18th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12);
held as part of the European Joint Conferences on Theory and Practice of
Software (ETAPS 2012), Tallinn, Estonia, March/April 2012
(C. Flanagan & B. König, eds.), LNCS 7214, Springer, 2012, pp. 173-187.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#94
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.
-
Technical Report 2011-10, Technical University of Braunschweig.
- Available as
ps,
pdf and
tex file.
- Archived at http://arxiv.org/abs/1207.3597.
- Extended abstract in: Proceedings 15th
International Conference on Foundations of Software Science
and Computation Structures (FoSSaCS 2012); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2012), Tallinn, Estonia, March/April 2012
(L. Birkedal, ed.), LNCS 7213, Springer, 2012, pp. 331-345,
doi:10.1007/978-3-642-28729-9_22.
- Extended abstract available as
ps,
pdf and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#95
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.
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.
- Available as
ps,
pdf and
source files.
- In: Proceedings 15th ACM International Conference on
Modeling, Analysis and Simulation of Wireless and Mobile Systems,
(MSWiM '12), Paphos, Cyprus, October 2012 (A.Y. Zomaya, B. Landfeldt & R. Prakash, eds),
ACM, 2012, pp. 203-212, doi:10.1145/2387238.2387274.
- Free download from the ACM:
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#97
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.
- Available as
ps,
pdf and
source files.
- In: Proceedings Combined 19th International Workshop on Expressiveness in Concurrency
and 9th Workshop on Structured Operational Semantics (EXPRESS/SOS 2012),
Newcastle upon Tyne, UK, September 3, 2012 (B. Luttik & M.A. Reniers, eds.),
Electronic Proceedings in
Theoretical Computer Science 89, Open Publishing Association, pp. 81-98,
doi:10.4204/EPTCS.89.7.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#98
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.
- Available as
pdf,
ps and
tex file.
- Theoretical Computer Science 538, pp. 16-36, 2014,
doi:
10.1016/j.tcs.2013.07.016
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#99
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.
- Available as
pdf,
ps and
tex file.
- Archived at https://arxiv.org/abs/1512.08891.
- In: Proceedings 16th ACM International Conference on
Modeling, Analysis and Simulation of Wireless and Mobile Systems
(MSWiM '13), Barcelona, Spain, November 2013, pp. 91-100, ACM, 2013,
doi:10.1145/2507924.2507943.
- Free download from the ACM:
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#100
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.
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].
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.
- Available as
dvi,
pdf and
ps.
- The Isabelle/HOL source files, and a full proof document, are available in the Archive of Formal Proofs, at
http://afp.sourceforge.net/entries/AWN.shtml.
- Archived at http://arxiv.org/abs/1407.3519.
- In: Proceedings 5th International Conference on Interactive Theorem Proving,
ITP 2014; held as Part of the Vienna Summer of Logic, VSL 2014,
Vienna, Austria, July 2014 (G. Klein & R. Gamboa, eds.),
LNCS 8558, Springer, 2014, pp. 144-159,
doi: 10.1007/978-3-319-08970-6_10
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#103
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
- Available as
pdf.
- The Isabelle/HOL source files, and a full proof document, are available in the Archive of Formal Proofs, at
http://afp.sourceforge.net/entries/AODV.shtml.
- Archived at http://arxiv.org/abs/1505.05646.
- In: Proceedings 12th International Symposium on Automated Technology
for Verification and Analysis, ATVA 2014, Sydney, Australia, November 2014
(F. Cassez and J.-F. Raskin, eds.), LNCS 8837, Springer, 2014, pp. 47-63,
doi: 10.1007/978-3-319-11936-6_5
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#104
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.
- Acta Informatica 52(1), 2015, pp. 3-4,
doi: 10.1007/s00236-014-0213-y
- Available as
pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#105
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.
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!
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.
- Acta Informatica 52(4-5), 2015, pp. 303-304,
doi: 10.1007/s00236-015-0240-3
- Available as
pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#108
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.
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
- In: Proceedings Combined 22th International Workshop on Expressiveness in Concurrency
and 12th Workshop on Structured Operational Semantics (EXPRESS/SOS 2015),
Madrid, Spain, 31st August 2015 (S. Crafa and D.E. Gebler, eds.),
Electronic
Proceedings in Theoretical Computer Science 190, Open Publishing
Association, pp. 46-60.
doi:10.4204/EPTCS.190.4.
- Available as
pdf and
source files.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#110
- The Isabelle/HOL source files, and a full proof document,
are available in the Archive of Formal Proofs,
at
http://afp.sourceforge.net/entries/Encodability_Process_Calculi.shtml
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.
- In: Proceedings Correct System Design - Symposium in Honor of
Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday
(R. Meyer, A. Platzer & H. Wehrheim, eds.),
Oldenburg, Germany, September 8-9, 2015, LNCS 9360,
Springer, pp. 99–130,
doi:10.1007/978-3-319-23506-6_9.
- Available as
pdf,
postscript and
source files.
- Archived at http://arxiv.org/abs/1509.05842.
- Slides.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#111
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.
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.
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.
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.
- Technical Report 9145, NICTA.
- Available as
pdf,
ps and
dvi.
- Archived at http://arxiv.org/abs/1606.03663.
- Extended abstract in: P. Thiemann, ed.:
Programming Languages and Systems, Proceedings 25th
European Symposium on Programming (ESOP 2016); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2016), Eindhoven, The Netherlands, April 2016,
LNCS 9632, Springer, pp. 95-122,
doi:10.1007/978-3-662-49498-1_5
- Extended abstract available as
pdf,
ps,
dvi and
tex source.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#115
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.
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.
- Available as
pdf and
tex source.
- In: Proceedings 31st Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2016, New York City, USA, July 2016,
ACM, 2016, pp. 778-787,
doi:10.1145/2933575.2933590
Free access through the above link.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#116
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.
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.
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.
- Available as
dvi,
ps,
pdf and
tex source.
- In: Liber Amicorum for Jan A. Bergstra (I. Bethke and B. Bredeweg
and A. Ponse, eds.), Informatics Institute, University of Amsterdam,
2016, pp. 58-59.
- Archived at http://arxiv.org/abs/1702.07838.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#119
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.
- Available as
dvi,
ps,
pdf and
tex source.
- In: Concurrency, Security, and Puzzles — Essays Dedicated to Andrew William Roscoe on the
Occasion of His 60th Birthday (Th. Gibson-Robinson and Ph.J. Hopcroft and R. Lazic, eds.),
LNCS 10160, Springer, 2017, pp. 272-293,
doi:10.1007/978-3-319-51046-0_14.
- Archived at http://arxiv.org/abs/1702.07844.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#120
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.
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.
- Available as
pdf and
tex source.
- In: Proceedings 26th EACSL Annual Conference on Computer Science Logic,
CSL 2017, Stockholm, Sweden, August 2017 (V. Goranko & M. Dam, eds.)
Leibniz International Proceedings in Informatics (LIPIcs) 82, Schloss
Dagstuhl–Leibniz-Zentrum für Informatik, 2017, pp. 25:1-25:20,
doi:10.4230/LIPIcs.CSL.2017.25.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#122
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.
- Available as
dvi,
ps,
pdf and
tex source.
- Archived at http://arxiv.org/abs/1704.03160.
- (Draft, released August 2016, available as
dvi,
ps,
pdf and
tex source.)
- In: Proceedings 32nd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2017, Reykjavik, Iceland, June 2017, IEEE
Computer Society Press, Los Alamitos 2017,
doi:10.1109/LICS.2017.8005142.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#123
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.
- Available as
pdf and
tex source.
- In: Proceedings 28th International Conference on Concurrency
Theory, CONCUR 2017, Berlin, Germany, September 2017
(R. Meyer & U. Nestmann, eds.), Leibniz International
Proceedings in Informatics (LIPIcs) 85, Schloss
Dagstuhl–Leibniz-Zentrum für Informatik, 2017, pp. 15:1-15:16,
doi:10.4230/LIPIcs.CONCUR.2017.15.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#124
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.
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.
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.
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
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.
- Available as
pdf and
tex file.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#129
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.
- May'18: Available as
dvi,
ps,
pdf and
tex source.
- Archived at http://arxiv.org/abs/1805.10415.
- Extended abstract in: Proceedings 21st
International Conference on Foundations of Software Science
and Computation Structures (FoSSaCS 2018); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2018), Thessaloniki, Greece, April 2018
(C. Baier & U. Dal Lago, eds.), LNCS 10803,
Springer, 2018, pp. 183-202, doi:10.1007/978-3-319-89366-2_10.
- February'18: Extended abstract available as
dvi,
ps,
pdf and
tex source.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#130
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.
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.
- In: Proceedings 14th International Conference on Integrated Formal Methods (IFM 2018),
Maynooth, Ireland, September 2018 (C.A. Furia and K. Winter, eds.), LNCS 11023,
pp. 398--418, doi:
10.1007/978-3-319-98938-9_23.
- Available as
pdf and
source files.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#132
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.
- In: Proceedings 29th International Conference on Concurrency Theory (CONCUR 2018),
Beijing, China (S. Schewe & L. Zhang, eds.),
Leibniz International Proceedings in Informatics (LIPIcs) 118:3,
doi:10.4230/LIPIcs.CONCUR.2018.3.
- Available as
pdf.
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.
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.
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.
- Original version available as
pdf and
sources;
archived at http://arxiv.org/abs/1909.00286v1.
- Revision 25-8-2021, with many small improvements based on
feedback by Weiyou Wang, available as
pdf and
sources.
- Archived at http://arxiv.org/abs/1909.00286.
- Extended abstract in: Proceedings 22st
International Conference on Foundations of Software Science
and Computation Structures (FoSSaCS 2019); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2019), Prague, Czech Republic, April 2019
(M. Bojańczyk, A. Simpson, eds.), LNCS 11425,
Springer, pp. 505-522, doi:10.1007/978-3-030-17127-8_29.
- Extended abstract available as
pdf and
sources.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#135
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.
- Available as
pdf and
sources.
- Archived at http://arxiv.org/abs/1907.13329.
- In L. Caires, ed.: Programming Languages and Systems, Proceedings 28th
European Symposium on Programming (ESOP 2019); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2019), Prague, Czech Republic, April 2019,
LNCS 11423, Springer, pp. 668-693,
doi:10.1007/978-3-030-17184-1_24
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#136
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.
- Available as
pdf,
dvi,
ps and
sources.
- Archived at http://arxiv.org/abs/1907.13348.
- In: Models, Languages, and Tools for Concurrent and Distributed Programming,
Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday
(M. Boreale, F. Corradini, M. Loreti & R. Pugliese, eds.), LNCS 11665,
Springer, 2019, pp. 45-70, doi:10.1007/978-3-030-21485-2_5.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#137
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.
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.
- Original version available as dvi,
ps,
pdf and
sources.
- In: Proceedings Combined 26th International Workshop on Expressiveness in Concurrency
and 16th Workshop on Structural Operational Semantics (EXPRESS/SOS 2019),
Amsterdam, The Netherlands, 26th August 2019 (J.A. Pérez & J. Rot, eds.),
Electronic Proceedings in
Theoretical Computer Science 300, Open Publishing Association,
doi:10.4204/EPTCS.300.5.
- Minor revision (15-9-2021), correcting an omission in Proposition 1,
available as pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#139
W.J. Fokkink (VU) & R.J. van Glabbeek (Data61, CSIRO), editors
August 2019
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.
- Available as pdf,
ps and
sources.
- In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to
Security and Privacy — Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday,
(M.S. Alvim, K. Chatzikokolakis, C. Olarte & F. Valencia, eds.), LNCS 11760, Springer, 2019,
pp. 182-205, doi:10.1007/978-3-030-31175-9_11.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#141
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.
- Available as pdf.
- In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to
Security and Privacy — Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday,
(M.S. Alvim, K. Chatzikokolakis, C. Olarte & F. Valencia, eds.), LNCS 11760, Springer, 2019,
pp. 139-162, doi:10.1007/978-3-030-31175-9_9.
- Full version available as pdf.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#142
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.
- Available as pdf.
- Archived at http://arxiv.org/abs/1912.04513.
- A minor revision, incorporating referee feedback and adding
an appendix with the formal syntax and semantics of ANTA:
Distributed Computing 36, 2023, pp. 137–157,
doi:10.1007/s00446-023-00446-0 (open access).
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#143
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.
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.
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.
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.
- Available as pdf.
- Archived at http://arxiv.org/abs/2007.08152.
- In: Proceedings 32nd ACM Symposium on Parallelism in Algorithms and Architectures, SPAA '20,
Virtual Event, USA, July 2020, pp. 579–581,
doi:10.1145/3350755.3400264.
Free access through the above link.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#147
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.
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.
W.J. Fokkink (VU) & R.J. van Glabbeek (Data61, CSIRO), editors
February/March 2021
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.
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.
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.
- Original version available as
pdf.
- Minor revision incorporating ESOP refereeing available as
pdf and
source files.
- Archived at https://arxiv.org/abs/2203.11519.
- Extended abstract in I. Sergey, ed.: Programming Languages and Systems,
Proceedings 31st European Symposium on Programming (ESOP 2022); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2022), Munich, Germany, April 2022,
LNCS 13240, Springer, pp. 548–574,
doi:10.1007/978-3-030-99336-8_20
The conference version equals the full version, but without the two appendices
with proofs of the main theorem.
- Extended abstract available as
pdf and
source files.
- Minor revision incorporating TOCL refereeing available as
pdf and
source files.
- ACM Transactions on
Computational Logic 25(1):1, November 2023,
doi: 10.1145/3611013
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#153
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.
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.
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.
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.
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.
- Available as pdf and
source files.
- In Proceedings 32nd International Conference on Concurrency Theory (CONCUR 2021),
Online, August 2021 (S. Haddad & D. Varacca, eds.)
Leibniz International Proceedings in Informatics (LIPIcs) 203,
Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2021,
doi:10.4230/LIPIcs.CONCUR.2021.1.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#158
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.
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.
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.
- Original version available as
pdf and
source files.
- December'22: Minor revision incorporating FoSSaCS refereeing available as
pdf and
source files.
- Archived at https://arxiv.org/abs/2212.08829.
- Extended abstract in: Proceedings 26th
International Conference on Foundations of Software Science
and Computation Structures (FoSSaCS 2023); held as part of
the European Joint Conferences on Theory and Practice of
Software (ETAPS 2023), Paris, France, April 2023
(O. Kupferman & P. Sobocinski, eds.), LNCS 13992, Springer, pp. 498-519,
doi:10.1007/978-3-031-30829-1_24.
- Extended abstract available as
pdf, and
source files.
- Slides
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#161
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.
- In: Proceedings Combined 30th International Workshop on Expressiveness in Concurrency
and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS 2023),
Antwerp, Belgium, 18th September 2023 (C.A. Mezzina and G. Caltais, eds.),
Electronic Proceedings in
Theoretical Computer Science 387, Open Publishing Association, pp. 42–58,
doi:10.4204/EPTCS.387.6.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#162
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.
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.
- Available as
pdf and
source files.
- In: Proceedings of the ACM on Programming Languages 8, POPL, Article 3, pp 61-89
(January 2024), doi:10.1145/3633211.
- Proof mechanisation:
Artifact for Shoggoth - A Formal Foundation for Strategic Rewriting,
doi:10.5281/zenodo.10125602.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#164
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.
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.
- Archived at http://arxiv.org/abs/2408.10117.
- Available as
pdf and
source files.
- Extended abstract in Proceedings 35th International Conference on
Concurrency Theory (CONCUR 2024), Calgary, Canada (Rupak Majumdar and Alexandra Silva, eds.)
Leibniz International Proceedings in Informatics (LIPIcs) 311,
Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2024,
doi:10.4230/LIPIcs.CONCUR.2024.36.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#166
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.
- Available as
pdf and
source files.
- This abstract: http://theory.stanford.edu/~rvg/abstracts.html#167
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:
Prof. Dr. A. Bode
SFB 342
Institüt für Informatik
Technische Universität München
Arcisstraße 21
D-8000 München 2,
Germany
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