Wan Fokkink

I&C Journal 2021 Journal Article

Detecting useless transitions in pushdown automata

• Evangelos Chatzikalymnios
• Wan Fokkink
• Dick Grune
• Brinio Hond
• Peter Rutgers

Pushdown automata may contain transitions that are never used in any accepting run of the automaton. We present an algorithm for detecting such useless transitions. A finite automaton that captures the possible stack content during runs of the pushdown automaton, is first constructed in a forward procedure to determine which transitions are reachable, and then employed in a backward procedure to determine which of these transitions can lead to a final state. An implementation of the algorithm is shown to exhibit a favorable performance.

I&C Journal 2019 Journal Article

Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence

• Wan Fokkink
• Rob van Glabbeek
• Bas Luttik

In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a τ-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of τ-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

I&C Journal 2017 Journal Article

Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity

• Wan Fokkink
• Rob van Glabbeek

Earlier we presented a method to decompose modal formulas for processes with the internal action τ, and congruence formats for branching and η-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. In this follow-up paper the decomposition method is enhanced to deal with modal characterisations that contain a modality 〈 ϵ 〉 〈 a 〉 φ, to derive congruence formats for delay and weak bisimilarity.

I&C Journal 2012 Journal Article

Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity

• Wan Fokkink
• Rob van Glabbeek
• Paulien de Wind

We present a method for decomposing modal formulas for processes with the internal action τ. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for two weak and rooted weak semantics: branching and η-bisimilarity.

TCS Journal 2011 Journal Article

Verification of mobile ad hoc networks: An algebraic approach

• Fatemeh Ghassemi
• Wan Fokkink
• Ali Movaghar

We introduced Computed Network Process Theory to reason about protocols for mobile ad hoc networks (MANETs). Here we explore the applicability of our framework in two regards: model checking and equational reasoning. The operational semantics of our framework is based on constrained labeled transition systems (CLTSs), in which each transition label is parameterized with the set of topologies for which this transition is enabled. We illustrate how through model checking on CLTSs one can analyze mobility scenarios of MANET protocols. Furthermore, we show how by equational theory one can reason about MANETs consisting of a finite but unbounded set of nodes, in which all nodes deploy the same protocol. Model checking and equational reasoning together provide us with an appropriate framework to prove the correctness of MANETs. We demonstrate the applicability of our framework by a case study on a simple routing protocol.

I&C Journal 2008 Journal Article

On finite alphabets and infinite bases

• Taolue Chen
• Wan Fokkink
• Bas Luttik
• Sumit Nain

Van Glabbeek presented the linear time–branching time spectrum of behavioral semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatizations for most of these semantics. Groote proved for some of van Glabbeek’s axiomatizations that they are ω -complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. In this paper, we settle the remaining open questions for all the semantics in the linear time–branching time spectrum, either positively by giving a finite sound and ground-complete axiomatization that is ω -complete, or negatively by proving that such a finite basis for the equational theory does not exist. We prove that in case of a finite alphabet with at least two actions, failure semantics affords a finite basis, while for ready simulation, completed simulation, simulation, possible worlds, ready trace, failure trace and ready semantics, such a finite basis does not exist. Completed simulation semantics also lacks a finite basis in case of an infinite alphabet of actions.

TCS Journal 2006 Journal Article

Bisimilarity is not finitely based over BPA with interrupt

• Luca Aceto
• Wan Fokkink
• Anna Ingolfsdottir
• Sumit Nain

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 (BPA) with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based.

TCS Journal 2006 Journal Article

Compositionality of Hennessy–Milner logic by structural operational semantics

• Wan Fokkink
• Rob van Glabbeek
• Paulien de Wind

This paper presents a method for the decomposition of HML formulas. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulas, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is the extension of an earlier decomposition method for the De Simone format from the Ph. D. thesis of Larsen in 1986, to more general formats.

TCS Journal 2005 Journal Article

CCS with Hennessy's merge has no finite-equational axiomatization

• 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 free fragment of Milner's Calculus of Communicating Systems is not finitely based modulo bisimulation equivalence. Thus, Hennessy's merge cannot replace the left merge and communication merge operators proposed by Bergstra and Klop, at least if a finite axiomatization of parallel composition modulo bisimulation equivalence is desired.

TCS Journal 2005 Journal Article

Guest editors’ foreword

• Luca Aceto
• Wan Fokkink
• Anna Ingolfsdottir
• Zoltán Ésik

I&C Journal 2004 Journal Article

Nested semantics over finite trees are equationally hard

• Luca Aceto
• Wan Fokkink
• Rob van Glabbeek
• Anna Ingólfsdóttir

This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based.

TCS Journal 2000 Journal Article

Language preorder as a precongruence

• Wan Fokkink

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, extended with predicates, to obtain a precongruence format for language preorder.

I&C Journal 1998 Journal Article

A Conservative Look at Operational Semantics with Variable Binding

• Wan Fokkink
• Chris Verhoef

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 substitutions, among other notions such as negative hypotheses and unary predicates on terms. The framework is used to present a conservativity format in operational semantics, which states sufficient criteria to ensure that the extension of a transition system specification with new transition rules does not affect the semantics of the original terms.

TCS Journal 1998 Journal Article

On a question of A. Salomaa the equational theory of regular expressions over a singleton alphabet is not finitely based

• Luca Aceto
• Wan Fokkink
• Anna Ingólfsdóttir

Salomaa (1969, p. 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 answer to this long-standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. The construction of the model mimics the one used by Conway (1971, p. 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions. Our analysis of the model, however, needs to be more refined than the one provided by Conway (1971).

I&C Journal 1997 Journal Article

An Equational Axiomatization for Multi-exit Iteration

• 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. 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 recursion equations of the formX1 = def P1X2+Q1 ⋮Xn = def PnX1+Qn, wherenis a positive integer and thePi and theQi are process terms. The addition of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA*). As a consequence, the proof of completeness of the proposed equational axiomatization for this language, although standard in its general structure, is much more involved than that for BPA*. An expressiveness hierarchy for the family ofk-exit iteration operators proposed by Bergstra, Bethke, and Ponse is also offered.

TCS Journal 1997 Journal Article

Termination modulo equations by abstract commutation with an application to iteration

• Wan Fokkink
• Hans Zantema

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

I&C Journal 1996 Journal Article

Axiomatizing Prefix Iteration with Silent Steps

• 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 operationP*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. , branching congruence, η-congruence, delay congruence, and weak congruence. The completeness proofs forη-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i. e. , terms that may contain process variables. As a by-product, theω-completeness of the axiomatizations is obtained, as well as their completeness for closed terms.

I&C Journal 1996 Journal Article

Ntyft/ntyxt Rules Reduce to Ntree Rules

• Wan Fokkink
• Rob van Glabbeek

Groote and Vaandrager introduced thetyft/tyxt formatfor Transition System Specifications (TSSs), and established that for each TSS in this format that iswell-founded, the bisimulation equivalence it induces is a congruence. In this paper, we construct for each TSS in tyft/tyxt format an equivalent TSS that consists oftree rulesonly. As a corollary we can give an affirmative answer to an open question, namely whether the well-foundedness condition in the congruence theorem for tyft/tyxt can be dropped. These results extend to tyft/tyxt with negative premises and predicates.