Wan Fokkink

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

Ready to Preorder: The Case of Weak Process Semantics ∗ (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...

Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras ⋆ (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...

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Mohammadreza Mousavi

Abstract. This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The...

Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras? (2009)

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Mohammadreza Mousavi

Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras (2009)

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Mohammadreza Mousavi

Abstract This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioral semantics over process algebras from old ones. The proposed...

Contents (2009)

Wan Fokkink, Jan Friso Groote, Michel Reniers

2

Executing multicellular differentiation: quantitative predictive modelling of C.elegans vulval development (2009)

Bonzanni, Nicola, Krepska, Elzbieta, Feenstra, K. Anton, Fokkink, Wan, Kielmann, Thilo, Bal, Henri, ...

Motivation: Understanding the processes involved in multi-cellular pattern formation is a central problem of developmental biology, hopefully leading to many new insights, e.g. in the treatment of...

Executing multicellular differentiation: quantitative predictive modelling of C.elegans vulval development (2009)

Bonzanni, Nicola, Krepska, Elzbieta, Feenstra, K. Anton, Fokkink, Wan, Kielmann, Thilo, Bal, Henri, ...

Formal Analysis Techniques for Gossiping Protocols (2008)

Rena Bakhshi, Wan Fokkink, Francois Bonnet, Boudewijn Haverkort

We give a survey of formal verification techniques that can be used to corroborate existing experimental results for gossiping protocols in a rigorous manner. We present properties of interest for...

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

Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras ⋆ (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...

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Mohammadreza Mousavi

Abstract. This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The...

From �t to �CRL: Combining Performance and Functional Analysis (2008)

Anton Wijs, Wan Fokkink

In this paper we first give short overviews of the modelling languages timed � (�t) and �CRL. Then we present a general translation scheme to translate �t specifications to �CRL...

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

Chen, Taolue, Fokkink, Wan, Van Glabbeek, Rob

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

An Analytical Model of Information Dissemination for a Gossip-based Protocol (2008)

Bakhshi, Rena, Gavidia, Daniela, Fokkink, Wan, Van Steen, Maarten

We develop an analytical model of information dissemination for a gossiping protocol that combines both pull and push approaches. With this model we analyse how fast an item is replicated through a...

Which Two-Sorted Algebras of Booleans and Naturals have a Finite Basis? (2008)

Wan Fokkink, Sujith Vijay

Abstract. We show that the two-sorted algebra of Booleans and naturals with conjunction, addition and inequality is not finitely based. If addition is removed, or negation is included, then the...

Contents Process Algebra with Recursive Operations (2008)

Jan Bergstra, Wan Fokkink

Nordic Journal of Computing A NOTE ON K-STATE SELF-STABILIZATION IN A RING WITH (2008)

Wan Fokkink, Jaap-henk Hoepman, Jun Pang

Abstract. We show that, contrary to common belief, Dijkstra’s K-state mutual exclusion algorithm on a ring also stabilizes when the number K of states per process is one less than the number N + 1...

Abstract A Note on an Expressiveness Hierarchy for Multi-exit Iteration (2008)

Termination Modulo Equations by Abstract Commutation with an Application to Iteration ∗ (2008)

Multi-exit iteration is a generalization of the standard binary Kleene star operation. The addition of this construct to Basic Process Algebra (BPA) yields a more expressive language than that...

Language preorder as a precongruence (2008)

commutation technique, to rewriting modulo equations. This result is applied in the setting of process algebra with iteration. 1

Which Two-Sorted Algebras of Booleans and Naturals have a Finite Basis? (2008)

Groote and Vaandrager introduced the tyft format, which is a congruence format for strong bisimulation equivalence. This article proposes additional syntactic requirements on the tyft format,...

Wan Fokkink, Sujith Vijay

Abstract. We show that the two-sorted algebra of Booleans and naturals with conjunction, addition and inequality is not finitely based. If addition is removed, or negation is included, then the...

Contents Structural Operational Semantics (2008)

Adapting the Uppaal Model of a Distributed Lift System (2008)

Wan Fokkink, Allard Kakebeen, Jun Pang

Abstract. In [6] an existing distributed lift system was analyzed using the process algebraic toolset µCRL, and in [11] the redesign of this system was analyzed using the timed automata based...

and (2008)

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Bas Luttik

finite equational base for CCS with left merge

1 CWI, Specification and Analysis of Embedded Systems Group (2008)

Wan Fokkink, Jun Pang, Inria Futurs, École Polytechnique

We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects....

Variations on itai-rodeh leader election for anonymous rings and their analysis in prism (2008)

Veri cation of Interlockings: from Control Tables to Ladder Logic Diagrams (2008)

Abstract: We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh [Itai and Rodeh 1981]. In contrast...

Wan Fokkink, Paul Hollingshead

Dependency relations between objects in a railway yard are tabulated in control tables. An interlocking, which guarantees validity of these dependencies, can be implemented in ladder logic. We...

Categories and Subject Descriptors: D.3.4 [Programming Languages]: Processors—compilers; (2008)

Adapting the UPPAAL Model of a Distributed Lift System (2008)

The article introduces a novel notion of lazy rewriting. By annotating argument positions as lazy, redundant rewrite steps are avoided, and the termination behavior of a term-rewriting system can be...

Wan Fokkink, Allard Kakebeen, Jun Pang

Abstract. Groote, Pang and Wouters (2001) analyzed an existing distributed lift system using the process algebraic toolset µCRL. Pang, Karstens and Fokkink (2003) analyzed a redesign of this system...

AVoCS’04 Preliminary Version Simplifying Itai-Rodeh Leader Election for Anonymous Rings (2008)

Divide and Congruence Applied to η-Bisimulation (2008)

We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh [14]. In contrast to the Itai-Rodeh algorithm,...

Copyright C, Luca Aceto, Luca Aceto, Willem Jan Fokkink, Willem Jan Fokkink, 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 BRICS...

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir

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

and (2008)

Using the left merge and the communication merge from ACP, we present an equational base (i.e., a ground-complete and ω-complete set of valid equations) for the fragment of CCS without recursion,...

Process algebra needs proof methodology, The Concurrency Column (2008)

Wan Fokkink, Jan Friso Groote, Michel Reniers

Nordic Journal of Computing A NOTE ON K-STATE SELF-STABILIZATION IN A RING WITH (2008)

Wan Fokkink, Jaap-henk Hoepman, Jun Pang

Abstract. We show that, contrary to common belief, Dijkstra’s K-state mutual exclusion algorithm on a ring also stabilizes when the number K of states per process is one less than the number N+ 1...

Nordic Journal of Computing A NOTE ON K-STATE SELF-STABILIZATION IN A RING WITH (2008)

Wan Fokkink, Jaap-henk Hoepman, Jun Pang

Abstract. We show that, contrary to common belief, Dijkstra’s K-state mutual exclusion algorithm on a ring also stabilizes when the number K of states per process is one less than the number N+ 1...

A Complete Equational Axiomatization for BPA with Pre x Iteration (2008)

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

Pre x iteration x is added to Basic Process Algebra with deadlock and empty process. We present a nite equational axiomatization for this process algebra, and we prove that this axiomatization is...

Abstract Prefix iteration (2007)

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

SEN-R0012 May 31, 2000 (2007)

x is added to Basic Process Algebra with deadlock and empty process. We present a finite equational axiomatization for this process algebra, and we prove that this axiomatization is complete with...

W. J. Fokkink, S. P. Luttik, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, ...

We consider the process theory PA that includes an operation for parallel composition, based on the interleaving paradigm. We prove that the standard set of axioms of PA is not !-complete by...

Fast Computation of an Alternating Sum (2007)

Robbert Fokkink, Wan Fokkink

this paper we will see that this is the case indeed. In order to compute S ff (n) efficiently, we looked for patterns in the plus and minus signs of the terms (\Gamma1)

Unification for Infinite Sets of Equations Between Finite Terms (2007)

Decorated Trace Semantics over BPA have no Finite Equational Axiomatization (2007)

A standard result from unification theory says that if a finite set E of equations between finite terms is unifiable, then there exists a most general unifier for E. In this paper, the theorem is...

2, Rob van Glabbeek 4 (2007)

Fokkink and Zantema have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary Kleene star operation (BPA ). In light...

Are Equationally Hard, Luca Aceto, Wan Fokkink, Anna Ingolfsdottir

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

1 (2007)

Wan Fokkink, Bahareh Badban

1

1 (2007)

Stefan Blom, Wan Fokkink, Sumit Nain

Abstract. We provide an answer to an open question, posed by van Glabbeek [4], regarding the axiomatizability of ready trace semantics. We prove that if the alphabet of actions is finite, then there...

and Reasoning about Programs---Logics of programs; F.3.2 [Logics and Meanings of (2007)

Bard Bloom, Wan Fokkink

This paper explores the connection between semantic equivalences and preorders for concrete sequential processes, represented by means of labeled transition systems, and formats of transition system...

From Ready Simulation to Completed Traces (2007)

Wan J. Fokkink, Luca Aceto, Luca Aceto, Wan Fokkink

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

2 (2007)

Wan Fokkink, Natalia Ioustinova, Ernst Kesseler, Yaroslav S. Usenko, Yuri A. Yushtein

Abstract. In order to optimise maintenance and increase safety, the Royal Netherlands Navy initiated the development of a multi-channel on-board data acquisition system for its Lynx helicopters. This...

2 (2007)

Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak Van Langevelde

1, and Jaco van de Pol 1 1

A Note on an Expressiveness Hierarchy for Multi-Exit Iteration (2007)

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir

Multi-exit iteration is a generalization of the standard binary Kleene star operation. The addition of this construct to Basic Process Algebra (BPA) yields a more expressive language than that...

Structural Operational Semantics and Bounded Nondeterminism (2007)

Wan Fokkink, Thuy Duong Vu

We present a rule format for structural operational semantics to guarantee that the associated labelled transition system is bounded nondeterministic.

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

Compositionality of Hennessy-Milner Logic (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...

Through Structural Operational, Wan Fokkink

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

A note on K-state self-stabilization in a ring with K=N (2007)

Wan Fokkink, Wan Fokkink, Jaap-henk Hoepman, Jaap-henk Hoepman, Jun Pang, Jun Pang

CWI is the National Research Institute for Mathematics and Computer Science. It is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a founding member of ERCIM, the...

The Netherlands, (2007)

Computing with Actions and Communications (2007)

Abstract. We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh [20]. In contrast to the Itai-Rodeh...

Fokkink, Wan, Klop, Jan Willem

The paradigm of computer science is nowadays shifting from computation to communication. In this paper we aim to give an impression of the algebra of actions and communications as it has been...

Formal Analysis Techniques for Gossiping Protocols (2007)

Rena Bakhshi, Francois Bonnet, Wan Fokkink, Boudewijn Haverkort

We give a survey of formal verification techniques that can be used to corroborate existing experimental results for gossiping protocols in a rigorous manner. We present properties of interest for...

Ready to preorder: get your BCCSP axiomatization for free (2007)

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir

Abstract. This paper contributes to the study of the equational theory of the semantics in van Glabbeek’s linear time- branching time spectrum over the language BCCSP, a basic process algebra for...

Modelling Distributed Systems (2007)

Fokkink, Wan.

A Finite Equational Base for CCS with Left Merge and Communication Merge (2006)

Aceto, Luca, Fokkink, Wan, Ingolfsdottir, Anna, Luttik, Bas

Using the left merge and communication merge from ACP, we present an equational base (i.e., a ground-complete and $\omega$-complete set of valid equations) for the fragment of CCS without recursion,...

On finite alphabets and infinite bases III: Simulation (2006)

Taolue Chen, Wan Fokkink

Abstract. This paper studies the (in)equational theory of simulation preorder and equivalence over the process algebra BCCSP. We prove that in the presence of a finite alphabet with at least two...

On the axiomatizability of priority (2006)

Luca Aceto, Taolue Chen, Wan Fokkink, Anna Ingolfsdottir

Abstract. This paper studies the equational theory of bisimulation equivalence over the process algebra BCCSP extended with the priority operator of Baeten, Bergstra and Klop. It is proven that, in...

A finite equational base for CCS with left merge and communication merge (2006)

Anna Ingólfsdóttir, Copyright C, Willem Jan Fokkink, Willem Jan Fokkink, Luca Aceto, Luca Aceto, ...

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

On finite alphabets and infinite bases II: Completed and ready simulation (2006)

Taolue Chen, Wan Fokkink, Sumit Nain

Abstract. We prove that the equational theory of the process algebra BCCSP modulo completed simulation equivalence does not have a finite basis. Furthermore, we prove that with a finite alphabet of...

Aceto, Luca, Fokkink, Wan, Ingolfsdottir, Anna, Luttik, Bas

This note shows that split-2 bisimulation equivalence (also known as timed equivalence) affords a finite equational axiomatization over the process algebra obtained by adding an auxiliary operation...

A finite basis for failure semantics (2005)

Wan Fokkink, Sumit Nain

Abstract. We present a finite ω-complete axiomatization for the process algebra BCCSP modulo failure semantics, in case of a finite alphabet. This solves an open question by Groote [12]. 1

Is timed branching bisimilarity an equivalence indeed (2005)

Wan Fokkink, Jun Pang, Anton Wijs

Abstract. We show that timed branching bisimilarity as defined by van der Zwaag [14] and Baeten & Middelburg [2] is not an equivalence relation, in case of a dense time domain. We propose an...

Finite equational bases in process algebra: Results and open questions (2005)

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Bas Luttik

Abstract. Van Glabbeek (1990) presented the linear time/branching time spectrum of behavioral equivalences for finitely branching, concrete, sequential processes. He studied these semantics in the...

CCS with Hennessy’s merge has no finite equational axiomatization (2005)

Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, Bas Luttik

This paper confirms a conjecture of Bergstra and Klop’s from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by Hennessy in 1981 to the recursion...

Anna Ingólfsdóttir, Copyright C, Willem Jan Fokkink, Willem Jan Fokkink, Luca Aceto, Luca Aceto, ...

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

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

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

The quest for equational axiomatizations of parallel composition: Status and open problems (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...

Luca Aceto, Wan Fokkink

This essay recounts the story of the quest for equational axiomatizations of parallel composition operators in process description languages, and of similar results in the classic field of formal...

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Sumit Nain

Abstract. This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop’s Basic Process Algebra with...

Verifying a Sliding Window Protocol in µCRL (2004)

W. J. Fokkink, J. F. Groote, J. Pang, B. Badban, Wan Fokkink, ...

CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented structure and is grouped into four clusters. Listed below...

Verifying a Sliding Window Protocol in µCRL (2004)

Wan Fokkink, Jan Frisco Groote, Jun Pang, Bahareh Badban

. We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is...

Simplifying Itai-Rodeh Leader Election for Anonymous Rings (2004)

W. J. Fokkink, J. Pang, Wan Fokkink, Jun Pang

We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh [20]. In contrast to the Itai-Rodeh algorithm,...

Copyright C, Willem Jan Fokkink, Willem Jan Fokkink, Luca Aceto, Luca Aceto, Luca Aceto, ...

This note shows that split-2 bisimulation equivalence (also known as timed equivalence) affords a finite equational axiomatization over the process algebra obtained by adding an auxiliary operation...

Anna Ingolfsdottir, Copyright C, Willem Jan Fokkink, Willem Jan Fokkink, Luca Aceto, Luca Aceto, ...

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop's Basic Process Algebra with the...

Precongruence formats for decorated trace semantics (2004)

Nested semantics over finite trees are equationally hard (2004)

y

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

Precongruence formats for decorated trace semantics (2004)

Bard Bloom, Wan Fokkink

This paper explores the connection between semantic equivalences and preorders for concrete sequential processes, represented by means of labeled transition systems, and formats of transition system...

On finite alphabets and infinite bases: From ready pairs to possible worlds (2004)

Wan Fokkink, Sumit Nain

Abstract. We prove that if a finite alphabet of actions contains at least two elements, then the equational theory for the process algebra BCCSP modulo any semantics no coarser than readiness...

Simplifying Itai-Rodeh leader election for anonymous rings (2004)

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

We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh [14]. In contrast to the Itai-Rodeh algorithm,...

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

Structural operational semantics and bounded nondeterminism (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...

Wan Fokkink, Thuy Duong Vu

Abstract. We present a rule format for structural operational semantics to guarantee that the associated labelled transition system is bounded nondeterministic. 1

Cones and Foci for Protocol Verification Revisited (2003)

Cones and Foci for Protocol Verification Revisited (2003)

Abstract. We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data...

W. J. Fokkink, J. Pang, Wan Fokkink, Jun Pang

Netherlands Organization for Scientific Research (NWO). CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented...

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

Cones and Foci for Protocol Verification Revisited (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...

Cones and Foci for Protocol Verification Revisited (2003)

We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects....

Model checking a cache coherence protocol for a Java DSM implementation (2003)

Abstract. We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data...

Jun Pang, Wan Fokkink, Rutger Hofman, Ronald Veldema

Jackal is a fine-grained distributed shared memory implementation of the Java programming language. It aims to implement Java’s memory model and allows multithreaded Java programs to run unmodified...

On the axiomatizability of ready traces, ready simulation and failure traces (2003)

Stefan Blom, Wan Fokkink, Sumit Nain

Abstract. We provide an answer to an open question, posed by van Glabbeek [4], regarding the axiomatizability of ready trace semantics. We prove that if the alphabet of actions is finite, then there...

Model checking a cache coherence protocol for a Java DSM implementation (2003)

Jun Pang, Wan Fokkink, Rutger Hofman, Ronald Veldema

Jackal is a fine-grained distributed shared memory implementation of the Java programming language. It aims to implement Java’s memory model and allows multithreaded Java programs to run unmodified...

A Note on an Expressiveness Hierarchy for Multi-exit Iteration (2002)

Willem Jan Fokkink, Willem Jan Fokkink, Luca Aceto, Luca Aceto, Luca Aceto, ...

Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of...

ABSTRACT Cones and Foci for Protocol Verification Revisited (2002)

W. J. Fokkink, J. Pang, Wan Fokkink, Jun Pang

CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented structure and is grouped into four clusters. Listed below...

µCRL: A toolset for analysing algebraic specifications (2001)

Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak Van Langevelde, Bert Lisser

µCRL [13] is a language for specifying and verifying distributed systems in an algebraic fashion. It targets the specification of system behaviour in a process-algebraic style and of data elements...

Structural operational semantics (2001)

Luca Aceto, Wan Fokkink, I Chris Verhoef

Lazy rewriting on eager machinery (2000)

Wan Fokkink, Pum Walters, Jasper Kamperman

The article introduces a novel notion of lazy rewriting. By annotating argument positions as lazy, redundant rewrite steps are avoided, and the termination behaviour of a term rewriting system can be...

ABSTRACT (2000)

W. J. Fokkink, S. P. Luttik, Issn -x, Copyright Stichting, Mathematisch Centrum, Wan Fokkink, ...

and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of

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

Rooted Branching Bisimulation as a Congruence (2000)

An omega-complete Equational Specification of Interleaving (2000)

This article presents a congruence format, in structural operational semantics, for rooted branching bisimulation equivalence. The format imposes additional requirements on Groote's ntyft...

Wan Fokkink, Bas Luttik

We consider the process theory PA that includes an operation for parallel composition, based on the interleaving paradigm. We prove that the standard set of axioms of PA is not !-complete by...

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

Rooted Branching Bisimulation as a Congruence (2000)

Rooted branching bisimulation as a congruence (2000)

This article presents a congruence format, in structural operational semantics, for rooted branching bisimulation equivalence. The format imposes additional requirements on Groote's ntyft...

Conservative extension in structural operational semantics (1999)

This article presents a congruence format, in structural operational semantics, for rooted branching bisimulation equivalence. The format imposes additional requirements on Groote’s ntyft format....

Conservative extension in structural operational semantics (1999)

An extension of a structural definition of an operational semantics is (operationally) conservative if it does not affect the semantics of terms over the original signature. We present a survey of...

Conservative extension in structural operational semantics (1999)

Structural operational semantics (SOS) [44] provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive appeal and...

Conservative Extension in Structural Operational Semantics (1999)

Structural operational semantics (SOS) [44] provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive appeal and...

Lazy Rewriting on Eager Machinery (1999)

Introduction Structural operational semantics (SOS) [44] provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive...

Wan Fokkink, Jasper Kamperman, Pum Walters

Machine [Cousineau et al. 1987], lazy constructors are used to achieve similar effects as our transformations. There, transformation of the program must be carried out manually for the most part....

Conservative Extension in Structural Operational Semantics (1999)

Luca Aceto Wan, Wan Fokkink, Chris Verhoef

Introduction Structural operational semantics (SOS) [44] provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive...

Lazy Rewriting on Eager Machinery (1999)

Wan Fokkink, Jasper Kamperman, Pum Walters

The article introduces a novel notion of lazy rewriting. By annotating argument positions as lazy, redundant rewrite steps are avoided, and the termination behaviour of a term rewriting system can be...

Basic Process Algebra with Iteration: Completeness of its Equational Axioms (1999)

Structural Operational Semantics (1999)

Bergstra, Bethke and Ponse proposed an axiomatization for Basic Process Algebra extended with (binary) iteration. In this paper, we prove that this axiomatization is complete with respect to strong...

1.0, LAnguage for Railway Interlocking Specifications, To appear as a publication of CWI, the (1999)

Contents 1 Introduction 3 2 Preliminaries 6 2.1 Labelled Transition Systems . . . . . . . . . . . . . . . . . . . 7 2.2 Behavioural Equivalences . . . . . . . . . . . . . . . . . . . . 8 2.3...

Wan Fokkink, Jan Friso Groote, Marco Hollenberg

This document has been produced in cooperation

Conservative extension in positive/negative conditional term rewriting with applications to software renovation factories (1999)

Conservative extension in positive/negative conditional term rewriting with applications to software renovation factories (1999)

Abstract. We transpose a conservative extension theorem from structural operational semantics to conditional term rewriting. The result is useful for the development of software renovation factories,...

Verification of Interlockings: from Control Tables to Ladder Logic Diagrams (1998)

Abstract. We transpose a conservative extension theorem from structural operational semantics to conditional term rewriting. The result is useful for the development of software renovation factories,...

Wan Fokkink, Paul Hollingshead

Dependency relations between objects in a railway yard are tabulated in control tables. An interlocking, which guarantees validity of these dependencies, can be implemented in ladder logic. We...

eRENA3.1] Demonstration and Evaluation of Inhabited Television, eRENA Deliverable 3.1 (1998)

A menagerie of non-finitely based process semantics over BPA*—from ready simulation to completed traces (1998)

Abstract. The cones and foci verification method from Groote and Springintveld [9] was extended to timed systems by van der Zwaag [17]. We present an extension of this cones and foci method for timed...

An Axiomatization for Regular Processes in Timed Branching Bisimulation (1998)

Fokkink and Zantema ((1994) Computer Journal 37:259–267) have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary...

Verification of Interlockings: from Control Tables to Ladder Logic Diagrams (1998)

ion The previous section treated BPA ffir with recursion modulo timed strong bisimulation. In this section the alphabet is extended with a special constant ø , to obtain BPA ffiø r with recursion,...

Wan Fokkink, Paul Hollingshead

Dependency relations between objects in a railway yard are tabulated in control tables. An interlocking, which guarantees validity of these dependencies, can be implemented in ladder logic. We...

Within ARM's Reach: Compilation of Left-Linear Rewrite Systems via Minimal Rewrite Systems (1998)

Wan Fokkink, Jasper Kamperman, Pum Walters

machine, automata, specificity ordering, term rewriting 1. INTRODUCTION A standard technique for speeding up the execution of a program in a formal (programming) language is compilation of the...

A Cook's Tour of Equational Axiomatizations for Prefix Iteration (1998)

A Conservative Look at Operational Semantics with Variable Binding (1998)

this paper, we continue this research programme by studying axiomatic characterizations for more abstract semantics over this language than those based on variations of bisimulation. More precisely,...

EURIS, a Specification Method for Distributed Interlockings (Extended Abstract) (1998)

We set up a formal framework to describe transition system specifications in the style of Plotkin. This framework has the power to express many-sortedness, general binding mechanisms and...

Fokko Van Dijk, Wan Fokkink, Gea Kolk, Bas Van Vlijmen

. Safety systems for railways have shifted from electronic relays to more computer-oriented approaches. This article highlights the language EURIS from NS Railinfrabeheer, which champions an...

Conservative Extension in Positive/Negative Conditional Term Rewriting with Applications to Software Renovation Factories (1998)

Wan Fokkink And, Wan Fokkink, Chris Verhoef

. We transpose a conservative extension theorem from structural operational semantics to conditional term rewriting. The result is useful for the development of software renovation factories, and for...

A Conservative Look at Operational Semantics with Variable Binding (1998)

Conservative Extension in Positive/Negative Conditional Term Rewriting with Applications to Software Renovation Factories (1998)

We set up a formal framework to describe transition system specifications in the style of Plotkin. This framework has the power to express many-sortedness, general binding mechanisms and...

eRENA3.1] Demonstration and Evaluation of Inhabited Television, eRENA Deliverable 3.1 (1998)

. We transpose a conservative extension theorem from structural operational semantics to conditional term rewriting. The result is useful for the development of software renovation factories, and for...

EURIS: a specification method for distributed interlockings (extended abstract (1998)

Fokko Van Dijk, Wan Fokkink, Gea Kolk

Abstract. Safety systems for railways have shifted from electronic relays to more computer-oriented approaches. This article highlights the language EURIS from NS Railinfrabeheer, which champions an...

A conservative look at operational semantics with variable binding (1998)

Axiomatizations for the perpetual loop in process algebra (1997)

We set up a formal framework to describe transition system specifications in the style of Plotkin. This framework has the power to express many-sortedness, general binding mechanisms and...

Simulation as a correct transformation of rewrite systems (1997)

Abstract. Milner proposed an axiomatization for the Kleene star in basic process algebra, in the presence of deadlock and empty process, modulo bisimulation equivalence. In this paper, Milner’s...

An equational axiomatization for multi-exit iteration (1997)

Abstract. Kamperman and Walters proposed the notion of a simulation of one rewrite system by another one, whereby each term of the simulating rewrite system is related to a term in the original...

Wan J. Fokkink, Luca Aceto, Luca Aceto, Wan Fokkink, Xn Pnx Qn

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

An SOS Message: Conservative Extension in Higher-Order Positive/Negative Conditional Term Rewriting (1997)

Wan Fokkink, Chris Verhoef, Wan Fokkink, Wan Fokkink, Wan Fokkink, Chris Verhoef, ...

. General theorems in structured operational semantics can be transformed into related results in conditional term rewriting. We apply this approach to obtain a conservative extension theorem for...

Axiomatizations for the Perpetual Loop in Process Algebra (1997)

Simulation as a Correct Transformation of Rewrite Systems (1997)

. Milner proposed an axiomatization for the Kleene star in basic process algebra, in the presence of deadlock and empty process, modulo bisimulation equivalence. In this paper, Milner's axioms...

Simulation as a Correct Transformation of Rewrite Systems (1997)

. Kamperman and Walters proposed the notion of a simulation of one rewrite system by another one, whereby each term of the simulating rewrite system is related to a term in the original rewrite...

An equational axiomatization for multi-exit iteration (1997)

. Kamperman and Walters proposed the notion of a simulation of one rewrite system by another one, whereby each term of the simulating rewrite system is related to a term in the original rewrite...

Luca Aceto, Wan Fokkink, Px Q, Pnx Qn

This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multiexit iteration is a generalization of the...

Ntyft/ntyxt rules reduce to ntree rules (1996)

Safety criteria for the vital processor interlocking at HoornKersenboogerd (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...

On a Question of A. Salomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based (1996)

We formulate several classes of safety criteria for railway yards in terms of observable behaviour. These criteria are meant to protect trains from collisions and from derailments. We identify a...

Axiomatizing Prefix Iteration with Silent Steps (1996)

Salomaa ((1969) Theory of Automata, page 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative...

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

An Equational Axiomatization for Multi-Exit Iteration (1996)

Luca Aceto, Wan Fokkink

This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multiexit iteration is a generalization of the...

A Logic for Signal Inserted Timed Frames (1996)

Jan Bergstra, Wan Fokkink, Kees Middelburg

We propose a first-order predicate logic TFL of timed frames extended with signals. This logic combines a simple syntax with a high expressivity; it can distinguish frames that are not the same as...

On the Completeness of the Equations for the Kleene Star in Bisimulation (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...

Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd (1996)

. A classical result from Redko [20] says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema [13] showed, by means...

A Menagerie of Non-Finitely Based Process Semantics over BPA - From Ready Simulation to Completed Traces (1996)

We formulate several classes of safety criteria for railway yards in terms of observable behaviour. These criteria are meant to protect trains from collisions and from derailments. We identify a...

Fokkink and Zantema ((1994) Computer Journal 37:259--267) have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary...

On a Question of A. Salomaa - The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based (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...

An Axiomatization for the Terminal Cycle (1996)

Salomaa ((1969) Theory of Automata, page 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative...

Correct Transformation of Rewrite Systems for Implementation Purposes (1996)

Milner proposed an axiomatization for the Kleene star in basic process algebra, in the presence of deadlock and empty process, modulo bisimulation equivalence. In this paper, Milner's axioms are...

A Logic for Signal Inserted Timed Frames (1996)

We propose the notion of a correct transformation of one rewrite system into another. If such a transformation is correct, then the normal forms of a term in the original rewrite system can be...

Jan Bergstra, Wan Fokkink, Kees Middelburg

We propose a first-order predicate logic TFL of timed frames extended with signals. This logic combines a simple syntax with a high expressivity; it can distinguish frames that are not the same as...

On the Completeness of the Equations for the Kleene Star in Bisimulation (1996)

. A classical result from Redko [20] says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema [13] showed, by means...

On the Completeness of the Equations for the Kleene Star in Bisimulation (1996)

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

A classical result from Redko [14] says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema [9] showed that there...

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

A complete axiomatization for prefix iteration in branching bisimulation (1996)

On the completeness of the equations for the Kleene star in bisimulation (1996)

This paper studies the interaction of prefix iteration with the silent step in the setting of branching bisimulation. We present a finite equational axiomatization for Basic Process Algebra with...

A Reference Model for Teleconferencing Systems (1995)

Abstract. A classical result from Redko [20] says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema [13] showed,...

Cinzia Bonini, W. J. Fokkink, A. Lesch, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, ...

We present a specification in Z of the framework of a teleconferencing system, which combines text, computer graphics, video, audio and other features in a computer display. Teleconferencing systems...

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

A Complete Axiomatization for Prefix Iteration in Branching Bisimulation (1995)

An Effective Axiomatization for Real Time ACP (1995)

This paper studies the interaction of prefix iteration with the silent step in the setting of branching bisimulation. We present a finite equational axiomatization for Basic Process Algebra with...

Wan Fokkink, Steven Klusener

This paper deals with prefix integration, and integration is parametrized by conditions, which are inequalities between linear expressions of variables. We present an axiomatization for process...

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

A Conservative Look at Term Deduction Systems with Variable Binding (1995)

Safety Criteria for Hoorn-Kersenboogerd Railway Station (1995)

We set up a formal framework to describe term deduction systems, such as transition system specifications in the style of Plotkin, and conditional term rewriting systems. This framework has the power...

A Conservative Look at Term Deduction Systems with Variable Binding (1995)

We formulate several classes of safety criteria for railway yards in terms of observable behaviour. These criteria are meant to protect trains from collisions and from derailments. We identify a...

Axiomatizing Prefix Iteration with Silent Steps (1995)

We set up a formal framework to describe term deduction systems, such as transition system specifications in the style of Plotkin, and conditional term rewriting systems. This framework has the power...

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

A Complete Axiomatization for Prefix Iteration in Branching Bisimulation (1995)

A complete equational axiomatization for prefix iteration (1994)

This paper studies the interaction of prefix iteration ¯ x with the silent step ø in the setting of branching bisimulation. That is, we present a finite equational axiomatization for Basic Process...

Basic process algebra with iteration: Completeness of its equational axioms (1994)

Prefix iteration a∗x is added to Minimal Process Algebra (MPAδ), which is a subalgebra of BPAδ equivalent to Milner’s basic CCS. We present a finite equational axiomatization for MPA ∗ δ,...

Basic Process Algebra with Iteration: Completeness of its Equational Axioms (1994)

Bergstra, Bethke and Ponse proposed an axiomatization for Basic Process Algebra extended with (binary) iteration. In this paper, we prove that this axiomatization is complete with respect to strong...

A Complete Equational Axiomatization for Prefix Iteration (1994)

Bergstra, Bethke and Ponse proposed an axiomatization for Basic Process Algebra extended with (binary) iteration. In this paper, we prove that this axiomatization is complete with respect to strong...

An Elimination Theorem for Regular Behaviours with Integration (1993)

Prefix iteration a x is added to Minimal Process Algebra (MPA ffi ), which is a subalgebra of BPA ffi equivalent to Milner's basic CCS. We present a finite equational axiomatization for MPA ffi...

A Simple Specification Language Combining Processes, Time and Data (1992)

This chapter deals with an extension of the process algebra ACP with rational time and integration. We determine a proper subdomain of the regular processes for which an elimination theorem holds,...

Leader Election in Anonymous Rings: Franklin Goes Probabilistic (1970)

Groote and Ponse have proposed a simple specification language based on CRL (Com- mon Representation Language) in [6]. This language, called ¯CRL, combines processes and data and contains only...

Rena Bakhshi, Wan Fokkink, Jun Pang

We present a probabilistic leader election algorithm for anonymous, bidirectional, asynchronous rings. It is based on an algorithm from Franklin [22], augmented with random identity selection, hop...

Language Preorder as a Precongruence

Process Algebra with Recursive Operations

Groote and Vaandrager introduced the tyft format, which is a congruence format for strong bisimulation equivalence. This article proposes additional syntactic requirements on the tyft format,...

Jan Bergstra, Wan Fokkink, Alban Ponse

ing from just the two atomic actions in I def = fthrow; tailg, FIR b 1 yields I ((throw tail) throw head) = head: First, observe I (throw tail) = . Then, using (4), it easily follows that I ((throw...

Language Preorder as a Precongruence

Language Preorder as a Precongruence

Groote and Vaandrager introduced the tyft format, which is a congruence format for strong bisimulation equivalence. This article proposes additional syntactic requirements on the tyft format,...