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...
Computing with Actions and Communications (2007)
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...
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,...
Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge (2005)
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...
Simplifying Itai-Rodeh Leader Election for Anonymous Rings (2004)
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,...
Verifying a Sliding Window Protocol in CRL (2004)
We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. We show that the sliding window protocol is branching bisimilar to a queue...
Centrum voor Wiskunde en Informatica (2004)
Wan Fokkink, Jaap-henk Hoepman, Jun Pang
We show that, contrary to common belief, Dijkstra's K-state mutual exclusion algorithm on a ring [1, 2] also stabilizes when the number K of states per process is one less than the number N+1 of...
Verifying a Sliding Window Protocol in CRL (2004)
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...
Verifying a Sliding Window Protocol in CRL (2004)
We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n.
Verifying a Sliding Window Protocol in mCRL (2003)
W. J. Fokkink, J. F. Groote, J. Pang, B. Badban, Wan Fokkink
We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n.Thecorrectness consists of showing that the sliding window protocol is...
Nested Semantics over Finite Trees (2003)
Luca Aceto, Wan Fokkink, Rob Van Glabbeek
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...
Compositionality of Hennessy-Milner Logic (2003)
Wan Fokkink, Rob Van Glabbeek, Paulien De Wind
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...
Compositionality of Hennessy-Milner Logic (2003)
Wan Fokkink, Rob Van Glabbeek, Paulien De Wind
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...
Precongruence Formats for Decorated Trace (2003)
Devices]: Modes of Computation--- Parallelism and concurrency; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs---Logics of programs; F.3.2 [Logics and...
On the Axiomatizability of Ready Traces, (2003)
We provide an answer to an open question, posed by van Glabbeek [4], regarding the axiomatizability of ready trace semantics.
A Note on an Expressiveness Hierarchy (2003)
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 (2003)
We present a rule format for structural operational semantics to guarantee that the associated labelled transition system is bounded nondeterministic.
Cones and Foci for Protocol Verification Revisited (2003)
W. J. Fokkink, J. Pang, Wan Fokkink
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)
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...
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....
Refinement and Verification Applied to an In-Flight Data Acquisition Unit (2002)
Wan Fokkink, Natalia Ioustinova, Ernst Kesseler, Yaroslav S. Usenko, Yuri A. Yushtein
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 AIDA...
CRL: A Toolset for Analysing Algebraic Specifications (2001)
Stefan Blom, Wan Fokkink, Jan Friso Groote
Introduction CRL [13] is a language for specifying and verifying distributed systems in an algebraic fashion. It targets the specification of system behaviour in a processalgebraic style and of data...
Structural Operational Semantics (2000)
Structural Operational Semantics (SOS) provides a framework to give an operational semantics to programming and specification languages, which, because of its intuitive appeal and flexibility, has...
W. J. Fokkink, S. P. Luttik, 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...
An omega-complete Equational Specification of Interleaving (2000)
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...
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...
Conservative Extension in Structural Operational Semantics (1999)
Luca Aceto, 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...
Structural Operational Semantics (1999)
Luca Aceto, Wan Fokkink, Chris Verhoef
Contents 1 Introduction 3 2 Preliminaries 6 2.1 Labelled Transition Systems . . . . . . . . . . . . . . . . . . . 7 2.2 Behavioural Equivalences . . . . . . . . . . . . . . . . . . . . 8 2.3...
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, and...
On the Completeness of the Equations for the Kleene Star in Bisimulation (1999)
. 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...
Safety criteria for the vital processor interlocking at Hoorn--Kersenboogerd (1999)
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...
Fast Computation of an Alternating Sum (1999)
Robbert Fokkink, Wan Fokkink, Jan Lune
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)
A Complete Equational Axiomatization for Prefix Iteration (1999)
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 , and...
Verification of Interlockings: from Control Tables to Ladder Logic Diagrams (1999)
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 (1999)
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 Complete Axiomatization for Prefix Iteration in Branching Bisimulation (1999)
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...
Language Preorder as a Precongruence (1999)
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,...
An Elimination Theorem for Regular Behaviours with Integration (1999)
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,...
Axiomatizations for the Perpetual Loop in Process Algebra (1999)
. 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...
Basic Process Algebra with Iteration: Completeness of its Equational Axioms (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...
Unification for Infinite Sets of Equations Between Finite Terms (1999)
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...
Lazy Rewriting on Eager Machinery (1999)
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....
A Cook's Tour of Equational Axiomatizations for Prefix Iteration (1999)
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,...
Rooted Branching Bisimulation as a Congruence (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. It...
A Menagerie of Non-Finitely Based Process Semantics over BPA (1999)
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...
An Effective Axiomatization for Real Time ACP (1999)
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...
. 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 Simple Specification Language Combining Processes, Time and Data (1999)
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...
A Reference Model for Teleconferencing Systems (1999)
C. Bonini, W. J. Fokkink, A. Lesch, Cinzia Bonini, Wan Fokkink, Arek Lesch
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...
A Logic for Signal Inserted Timed Frames (1999)
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...
An Equational Axiomatization for Multi-Exit Iteration (1999)
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...
Basic Process Algebra with Iteration: Completeness of its Equational Axioms (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...
Language Preorder as a Precongruence (1999)
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,...
Rooted Branching Bisimulation as a Congruence (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. It...
On the Completeness of the Equations for the Kleene Star in Bisimulation (1999)
. 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...
Fast Computation of an Alternating Sum (1999)
Robbert Fokkink, Wan Fokkink, Jan Lune
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)
Language Preorder as a Precongruence (1999)
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,...
. 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...
An Equational Axiomatization for Multi-Exit Iteration (1999)
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...
Unification for Infinite Sets of Equations Between Finite Terms (1999)
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...
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...
A Complete Axiomatization for Prefix Iteration in Branching Bisimulation (1999)
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...
Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd (1999)
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...
Basic Process Algebra with Iteration: Completeness of its Equational Axioms (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...
A Complete Equational Axiomatization for Prefix Iteration (1999)
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 , and...
Axiomatizing Prefix Iteration with Silent Steps (1999)
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...
Verification of Interlockings: from Control Tables to Ladder Logic Diagrams (1999)
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...
On the Completeness of the Equations for the Kleene Star in Bisimulation (1999)
. 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...
Within ARM's Reach: Compilation of Left-Linear Rewrite Systems via Minimal Rewrite Systems (1999)
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...
An Elimination Theorem for Regular Behaviours with Integration (1999)
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,...
Ntyft/ntyxt Rules Reduce to Ntree Rules (1999)
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...
On a Question of A. Salomaa (1999)
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...
A Cook's Tour of Equational Axiomatizations for Prefix Iteration (1999)
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,...
Simulation as a Correct Transformation of Rewrite Systems (1999)
. 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...
EURIS, a Specification Method for Distributed Interlockings (extended ) (1999)
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...
An Effective Axiomatization for Real Time ACP (1999)
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...
Axiomatizations for the Perpetual Loop in Process Algebra (1999)
. 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...
An Axiomatization for Regular Processes in Timed Branching Bisimulation (1999)
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,...
A Conservative Look at Operational Semantics with Variable Binding (1999)
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...
. 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...
Within ARM's Reach: Compilation of Left-Linear Rewrite Systems via Minimal Rewrite Systems (1998)
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...
Lazy Rewriting on Eager Machinery (1998)
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...
EURIS, a Specification Method for Distributed Interlockings (Extended Abstract) (1998)
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...
Verification of Interlockings: from Control Tables to Ladder Logic Diagrams (1998)
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...
A Conservative Look at Operational Semantics with Variable Binding (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...
W. Fokkink, C. Verhoef, 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...
An Axiomatization for Regular Processes in Timed Branching Bisimulation (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,...
A Cook's Tour of Equational Axiomatizations for Prefix Iteration (1997)
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,...
Axiomatizations for the Perpetual Loop in Process Algebra (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 are...