Rob Van Glabbeek

Symmetric and Asymmetric Asynchronous Interaction (2009)

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

Rob Van Glabbeek, Ursula Goltz, Jens-wolfhard Schicke, Tu Braunschweig

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

Five Determinisation Algorithms (2009)

On Synchronous and Asynchronous Interaction in Distributed Systems (2009)

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

Rob Van Glabbeek, Ursula Goltz, Jens-wolfhard Schicke

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

On Finite Bases for Weak Semantics: Failures versus Impossible Futures ⋆ (2009)

Five Determinisation Algorithms (2009)

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

Characterising testing preorders for finite probabilistic processes (2009)

Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan

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

On Finite Bases for Weak Semantics: Failures versus Impossible Futures ⋆ (2009)

ICE 2008 Symmetric and Asymmetric Asynchronous Interaction (2009)

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

Rob Van Glabbeek, Ursula Goltz, Jens-wolfhard Schicke

On Synchronous and Asynchronous Interaction inDistributed Systems (2009)

Rob Van Glabbeek, Ursula Goltz, Jens-wolfhard Schicke

Symmetric and Asymmetric Asynchronous Interaction (2009)

Rob Van Glabbeek, Ursula Goltz

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

Five Determinisation Algorithms (2009)

Ready to Preorder: The Case of Weak Process Semantics ∗ (2009)

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

Characterising testing preorders for finite probabilistic processes (2009)

Recently, Aceto, Fokkink & Ingólfsdóttir proposed an algorithm to turn any sound and ground-complete axiomatisation of any preorder listed in the linear time – branching time spectrum at...

Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan

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

Contents (2009)

Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan

This paper provides modal- and relational characterisations of may- and must-testing preorders for recursive CSP processes with divergence, featuring probabilistic as well as nondeterministic choice....

Correcting a Space-Efficient Simulation Algorithm (2008)

On Finite Bases for Weak Semantics: Failures versus Impossible Futures ⋆ (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...

Characterising testing preorders for finite probabilistic processes (2008)

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

Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan

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

Characterising testing preorders for finite probabilistic processes (2008)

Yuxin Deng, Rob Van Glabbeek

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

Characterising testing preorders for finite probabilistic processes (2008)

Yuxin Deng, Rob Van Glabbeek

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

Divide and Congruence Applied to η-Bisimulation (2008)

Computation Tree Logic with Deadlock Detection (extended abstract) (2008)

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

Characterising testing preorders for finite probabilistic processes (2008)

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

Yuxin Deng, Rob Van Glabbeek

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

A Characterisation of Weak Bisimulation Congruence (2008)

The individual and collective token interpretations of Petri nets (2008)

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

Petri nets with application to active document (2008)

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

David G. Stork, Rob Van Glabbeek

Token-controlled place refinement in hierarchical

SOS 2005 Preliminary Version Divide and Congruence Applied to η-Bisimulation (2008)

A Characterisation of Weak Bisimulation Congruence (2008)

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

Bundle Event Structures and CCSP (2008)

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

Rob Van Glabbeek, Frits Va

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

Computation Tree Logic with Deadlock Detection (2008)

Computation Tree Logic with Deadlock Detection (extended abstract) (2008)

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

Computation Tree Logic with Deadlock Detection (2008)

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

Scheduling Algebra (2007)

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

Scheduling Algebra (2007)

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

Event Structures for Resolvable Con ict (2007)

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

Well-behaved Flow Event Structures for Parallel Composition and Action Renement (2007)

Abstract. We propose a generalisation of Winskel's event structures, matching the expressive power of arbitrary Petri nets. In particular, our event structures capture resolvable con ict,...

Rob Van Glabbeek, Ursula Goltz

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

Petri nets with application to active document (2007)

David G. Stork, Rob Van Glabbeek

Token-controlled place refinement in hierarchical

Compositionality of Hennessy-Milner Logic through Structural Operational Semantics (2007)

Background Testing theory pCSP Simulations Some results Background (2007)

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

Matthew Hennessy, Rob Van Glabbeek, Carroll Morgan, Chenyi Zhang

Goal: Specification and proof methodologies for probabilistic concurrent systems Nondeterminism + Probability – why necessary? ◮ “Nondeterminism ” intrinsic to specification development à la...

Scalar outcomes suffice for finitary probabilistic testing (2007)

Yuxin Deng, Rob Van Glabbeek, Carroll Morgan, Chenyi Zhang

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

Branching Bisimulation with Explicit Divergence (2007)

Rob Van Glabbeek, Matthew Hennessy, Traian Serbanuta, Grigore Rosu, Jose Meseguer

Abstract. We consider the relational characterisation of branching bisimulation with explicit divergence. We prove that it is an equivalence relation and that it coincides with the original...

Editors: (2007)

Scalar outcomes suffice for finitary probabilistic testing (2007)

Yuxin Deng, Rob Van Glabbeek, Carroll Morgan, Chenyi Zhang

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

Liveness, Fairness and Impossible Futures (2006)

Rob Van Glabbeek, Marc Voorhoeve

Abstract. Impossible futures equivalence is the semantic equivalence on labelled transition systems that identifies systems iff they have the same “AGEF ” properties: temporal logic properties...

Liveness, Fairness and Impossible Futures (2006)

Rob Van Glabbeek, Marc Voorhoeve

Abstract. Impossible futures equivalence is the semantic equivalence on labelled transition systems that identifies systems iff they have the same "AGEF " properties: temporal logic...

ii Contents Preface v (2006)

Rob Van Glabbeek, Peter D. Mosses, Mohammadreza Mousavi, Michel A. Reniers

On cool congruence formats for weak bisimulations (extended abstract (2005)

Wind: Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation (2005)

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

Wind: Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation (2005)

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

On cool congruence formats for weak bisimulations (extended abstract (2005)

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

G.D.: Event Structures for Resolvable Conflicts (2004)

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

Nested semantics over finite trees are equationally hard (2004)

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

Luca Aceto, Wan Fokkink, Rob Van Glabbeek, Anna Ingólfsdóttir

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

G.D.: Event Structures for Resolvable Conflicts (2004)

Event Structures for Resolvable Conflict (2004)

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

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

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

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

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

Proof Nets for Unit-free Multiplicative-Additive Linear Logic (2003)

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

Extended Dominic, Dominic Hughes, Rob Van Glabbeek

this paper we propose a new notion of MALL proof net (Section 2) which adheres faithfully to the original MLL # This paper appeared in Proceedings 18th Annual IEEE Symposium on Logic in Computer...

Proof Nets for Unit-free Multiplicative-Additive Linear Logic (2003)

Extended Dominic, Dominic Hughes, Rob Van Glabbeek

this paper we propose a new notion of MALL proof net (Section 2) which adheres faithfully to the original MLL theory: we provide a simple inductive translation of cut-free # A preliminary version of...

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

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

Compositionality of Hennessy-Milner logic through structural operational semantics (2003)

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

Bundle Event Structures and CCSP (2003)

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

Rob Van Glabbeek, Frits Vaandrager

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

Precongruence Formats for Decorated Trace Preorders (2000)

Bard Bloom, Wan Fokkink, Rob Van Glabbeek

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

Precongruence Formats for Decorated Trace Preorders (2000)

Bard Bloom, Wan Fokkink, Rob Van Glabbeek

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

Scheduling Algebra (1999)

Scheduling Algebra (1999)

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

Scheduling algebra (1999)

. Our goal 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...

Refinement of Actions and Equivalence Notions for Concurrent Systems (1998)

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

Rob Van Glabbeek, Ursula Goltz

This paper combines and extends the material of [GG-a/c/d/e], except for the part in [GG-c] on refinement of transitions in Petri nets and the discussion of TCSP-like parallel composition in [GG-e]....

COMPUTING NATURAL LANGUAGE CSLI Lecture Notes (1998)

Atocha Aliseda, Rob Van Glabbeek, Dag Westerstahl, John Perry

Number 81

Ntyft/ntyxt rules reduce to ntree rules (1996)

Axiomatizing Prefix Iteration with Silent Steps (1996)

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

Wan J. Fokkink, Luca Aceto, Luca Aceto, Rob Van Glabbeek, ...

is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...

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

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

Groote and... 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,...

Axiomatizing Prefix Iteration with Silent Steps (1996)

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

Wan J. Fokkink, Luca Aceto, Luca Aceto, Rob Van Glabbeek, Wan Fokkink, ...

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...

Axiomatizing Prefix Iteration with Silent Steps (1996)

Luca Aceto, Rob Van Glabbeek, Wan Fokkink, Anna Ingólfsdóttir

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

Axiomatizing Prefix Iteration with Silent Steps (1995)

Luca Aceto, Rob Van Glabbeek, Wan Fokkink, Anna Ingólfsdóttir

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

Axiomatizing Prefix Iteration with Silent Steps (1995)

Luca Aceto, Rob Van Glabbeek, Wan Fokkink, Anna Ingólfsdóttir

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

Axiomatizing Prefix Iteration with Silent Steps (1995)

Luca Aceto, Rob Van Glabbeek, Wan Fokkink

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

On the Expressiveness of ACP (Extended Abstract) (1994)

Axiomatising ST-Bisimulation Equivalence (1994)

TSSs). An abstract \Sigma-literal is an expression t \Gamma! t 0 with t; t 0 2 T(\Sigma). An abstract action rule over (\Sigma; A) is an expression of the form H; Pr ff with H a set of abstract...

Nadia Busi, Rob Van Glabbeek, Roberto Gorrieri

this paper, we define an ST operational semantics in SOS style [22] for a process algebra equipped with the TCSP parallel composition operator, the ACP sequential composition operator and the...

Axiomatising ST-Bisimulation Equivalence (1994)

Nadia Busi, Rob Van Glabbeek, Roberto Gorrieri

this paper, we define an ST operational semantics in SOS style [22] for a process algebra equipped with the TCSP parallel composition operator, the ACP sequential composition operator and the...

Full Abstraction in Structural Operational Semantics (Extended Abstract) (1993)

The Difference between Splitting in n and n + 1 (1991)

ion in Structural Operational Semantics (extended abstract) Rob van Glabbeek Computer Science Department, Stanford University Stanford, CA 94305, USA rvg@cs.stanford.edu Abstract This paper explores...

Rob Van Glabbeek, Frits Vaandrager

this paper was initiated at the time both authors were employed at CWI, Amsterdam, continued during a visit of the second author to the Technical University of Munich, at the time the first author...

Branching-Time and Abstraction (1989)

Branching-Time and Abstraction (1989)

We consider the relational characterisation of branching bisimulation with explicit divergence. We prove that it is an equivalence relation and that it coincides with the original definition of...