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 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...
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....
Precongruence Formats for Decorated Trace Semantics (2002)
Bloom, B., Fokkink, W. J., Van Glabbeek, R. J.
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...
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...
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...
Algebra of Timed Frames (1999)
J. A. Bergstra, W. J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Within ARM's Reach: Compilation of Left-Linear Rewrite Systems via Minimal Rewrite Systems (1998)
A new compilation technique for left-linear term rewriting systems is presented, where rewrite rules are transformed into so-called minimal rewrite rules. These minimal rules have such a simple form...
Algebra of Timed Frames (1997)
J. A. Bergstra, W. J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
An Axiomatization for the Terminal Cycle (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...
Correct Transformation of Rewrite Systems for Implementation Purposes (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...
Termination modulo equations by abstract commutation with an application to iteration (1996)
We generalize a termination theorem in term rewriting, based on an abstract commutation technique, to rewriting modulo equations. This result is applied in the setting of process algebra with...
A logic for signal inserted timed frames (1996)
Bergstra, J.A., Fokkink, W.J., Middelburg, K.
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...
Algebra of Timed Frames (1995)
J. A. Bergstra, W. J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Algebra of Timed Frames (1995)
J. A. Bergstra, W. J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Algebra of Timed Frames (1995)
J. A. Bergstra, W. J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Algebra of Timed Frames (1995)
Bergstra, J.A., Fokkink, W.J., Middelburg, C.A.
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
A Conservative Look at Term Deduction Systems with Variable Binding (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...
On the Completeness of the Equations for the Kleene Star in Bisimulation (1995)
A classical result from Redko says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema showed that there does exist...
Safety Criteria for Hoorn-Kersenboogerd Railway Station (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...
A Complete Axiomatization for Prefix Iteration in Branching Bisimulation (1995)
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...
A complete equational axiomatization for BPA-δε with prefix iteration (1995)
Prex 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...
The Tyft/tyxt Format Reduces to Tree Rules (1994)
W. J. Fokkink, Willem Jan Fokkink
. Groote and Vaandrager [5] introduced the tyft/tyxt format for transition system specifications (TSSs), and established that for each TSS in this format that is well-founded, the strong bisimulation...
Basic Process Algebra With Iteration: Completeness of Its Equational Axioms (1994)
W. J. Fokkink, H. Zantema, Willem Jan Fokkink, Hans Zantema
Bergstra, Bethke & Ponse [BBP93] proposed an axiomatisation for Basic Process Algebra extended with (binary) iteration. In this paper, we prove that this axiomatisation is complete with respect to...
Basic process algebra with iteration: completeness of its equational axioms (1993)
Bergstra, Bethke & Ponse [BBP93] proposed an axiomatisation for Basic Process Algebra extended with iteration. In this paper, we prove that this axiomatisation is complete with respect to...
Algebra of Timed Frames (1970)
J. A. Bergstra, W. J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...