-
Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?
Authors:
Luca Aceto,
Valentina Castiglioni,
Wan Fokkink,
Anna Igolfsdottir,
Bas Luttik
Abstract:
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy's merge is added to that language. These results raise the que…
▽ More
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy's merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. We contribute to answering this question in the simplified setting of the recursion-, relabelling-, and restriction-free fragment of CCS. We formulate three natural assumptions pertaining to the operational semantics of auxiliary operators and their relationship to parallel composition, and prove that an auxiliary binary operator facilitating a finite axiomatisation of bisimilarity in the simplified setting cannot satisfy all three assumptions.
△ Less
Submitted 30 March, 2022; v1 submitted 5 October, 2020;
originally announced October 2020.
-
A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
Authors:
Clemens Grabmayer,
Wan Fokkink
Abstract:
Robin Milner (1984) gave a sound proof system for bisimilarity of regular expressions interpreted as processes: Basic Process Algebra with unary Kleene star iteration, deadlock 0, successful termination 1, and a fixed-point rule. He asked whether this system is complete. Despite intensive research over the last 35 years, the problem is still open.
This paper gives a partial positive answer to Mi…
▽ More
Robin Milner (1984) gave a sound proof system for bisimilarity of regular expressions interpreted as processes: Basic Process Algebra with unary Kleene star iteration, deadlock 0, successful termination 1, and a fixed-point rule. He asked whether this system is complete. Despite intensive research over the last 35 years, the problem is still open.
This paper gives a partial positive answer to Milner's problem. We prove that the adaptation of Milner's system over the subclass of regular expressions that arises by dropping the constant 1, and by changing to binary Kleene star iteration is complete. The crucial tool we use is a graph structure property that guarantees expressibility of a process graph by a regular expression, and is preserved by going over from a process graph to its bisimulation collapse.
△ Less
Submitted 27 April, 2020;
originally announced April 2020.
-
Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence
Authors:
Wan Fokkink,
Rob van Glabbeek,
Bas Luttik
Abstract:
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 stab…
▽ More
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.
△ Less
Submitted 18 August, 2019;
originally announced August 2019.
-
Reliable Restricted Process Theory
Authors:
Fatemeh Ghassemi,
Wan Fokkink
Abstract:
Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator i…
▽ More
Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.
△ Less
Submitted 7 May, 2017;
originally announced May 2017.
-
Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity
Authors:
Wan Fokkink,
Rob van Glabbeek
Abstract:
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…
▽ More
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 $\langleε\rangle\langle a\rangleφ$, to derive congruence formats for delay and weak bisimilarity.
△ Less
Submitted 21 December, 2017; v1 submitted 26 April, 2016;
originally announced April 2016.
-
On the Axiomatizability of Impossible Futures
Authors:
Taolue Chen,
Wan Fokkink,
Rob van Glabbeek
Abstract:
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations…
▽ More
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no finite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is infinite, then the aforementioned ground-complete axiomatizations are shown to be omega-complete. If the alphabet is finite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a finite basis.
△ Less
Submitted 20 September, 2015; v1 submitted 19 May, 2015;
originally announced May 2015.
-
Maximally Permissive Controlled System Synthesis for Modal Logic
Authors:
Allan van Hulst,
Michel Reniers,
Wan Fokkink
Abstract:
We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic.…
▽ More
We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic. while all non-invalidating behavior is retained. This induces maximal permissiveness in the context of supervisory control. Research presented in this paper allows a system model to be constrained according to a broad set of liveness, safety and fairness specifications of desired behavior, and embraces most concepts from Ramadge-Wonham supervisory control, including controllability and marker-state reachability. Synthesis is defined in this paper as a formal construction, which allowed a careful validation of its correctness using the Coq proof assistant.
△ Less
Submitted 14 August, 2014;
originally announced August 2014.
-
Detecting Useless Transitions in Pushdown Automata
Authors:
Wan Fokkink,
Dick Grune,
Brinio Hond,
Peter Rutgers
Abstract:
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 d…
▽ More
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 stat
△ Less
Submitted 8 June, 2013;
originally announced June 2013.
-
Distributed MAP in the SpinJa Model Checker
Authors:
Stefan Vijzelaar,
Kees Verstoep,
Wan Fokkink,
Henri Bal
Abstract:
Spin in Java (SpinJa) is an explicit state model checker for the Promela modelling language also used by the SPIN model checker. Designed to be extensible and reusable, the implementation of SpinJa follows a layered approach in which each new layer extends the functionality of the previous one. While SpinJa has preliminary support for shared-memory model checking, it did not yet support distribute…
▽ More
Spin in Java (SpinJa) is an explicit state model checker for the Promela modelling language also used by the SPIN model checker. Designed to be extensible and reusable, the implementation of SpinJa follows a layered approach in which each new layer extends the functionality of the previous one. While SpinJa has preliminary support for shared-memory model checking, it did not yet support distributed-memory model checking. This tool paper presents a distributed implementation of a maximal accepting predecessors (MAP) search algorithm on top of SpinJa.
△ Less
Submitted 1 November, 2011;
originally announced November 2011.
-
A Modeling Framework for Gossip-based Information Spread
Authors:
Rena Bakhshi,
Daniela Gavidia,
Wan Fokkink,
Maarten van Steen
Abstract:
We present an analytical framework for gossip protocols based on the pairwise information exchange between interacting nodes. This framework allows for studying the impact of protocol parameters on the performance of the protocol. Previously, gossip-based information dissemination protocols have been analyzed under the assumption of perfect, lossless communication channels. We extend our framework…
▽ More
We present an analytical framework for gossip protocols based on the pairwise information exchange between interacting nodes. This framework allows for studying the impact of protocol parameters on the performance of the protocol. Previously, gossip-based information dissemination protocols have been analyzed under the assumption of perfect, lossless communication channels. We extend our framework for the analysis of networks with lossy channels. We show how the presence of message loss, coupled with specific topology configurations,impacts the expected behavior of the protocol. We validate the obtained models against simulations for two protocols.
△ Less
Submitted 30 May, 2011;
originally announced May 2011.
-
Congruence from the Operator's Point of View: Compositionality Requirements on Process Semantics
Authors:
Maciej Gazda,
Wan Fokkink
Abstract:
One of the basic sanity properties of a behavioural semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by the development of rule formats for transition system specifications that define process algebras. In this paper we suggest a novel, orthogonal approach. Namely, we focus on a number of process operators, an…
▽ More
One of the basic sanity properties of a behavioural semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by the development of rule formats for transition system specifications that define process algebras. In this paper we suggest a novel, orthogonal approach. Namely, we focus on a number of process operators, and for each of them attempt to find the widest possible class of congruences. To this end, we impose restrictions on sublanguages of Hennessy-Milner logic, so that a semantics whose modal characterization satisfies a given criterion is guaranteed to be a congruence with respect to the operator in question. We investigate action prefix, alternative composition, two restriction operators, and parallel composition.
△ Less
Submitted 12 August, 2010;
originally announced August 2010.
-
Asynchronous Bounded Expected Delay Networks
Authors:
Rena Bakhshi,
Jörg Endrullis,
Wan Fokkink,
Jun Pang
Abstract:
The commonly used asynchronous bounded delay (ABD) network models assume a fixed bound on message delay. We propose a probabilistic network model, called asynchronous bounded expected delay (ABE) model. Instead of a strict bound, the ABE model requires only a bound on the expected message delay. While the conditions of ABD networks restrict the set of possible executions, in ABE networks all async…
▽ More
The commonly used asynchronous bounded delay (ABD) network models assume a fixed bound on message delay. We propose a probabilistic network model, called asynchronous bounded expected delay (ABE) model. Instead of a strict bound, the ABE model requires only a bound on the expected message delay. While the conditions of ABD networks restrict the set of possible executions, in ABE networks all asynchronous executions are possible, but executions with extremely long delays are less probable. In contrast to ABD networks, ABE networks cannot be synchronised efficiently. At the example of an election algorithm, we show that the minimal assumptions of ABE networks are sufficient for the development of efficient algorithms. For anonymous, unidirectional ABE rings of known size N we devise a probabilistic leader election algorithm having average message and time complexity O(N).
△ Less
Submitted 7 June, 2011; v1 submitted 10 March, 2010;
originally announced March 2010.
-
Modal Logic and the Approximation Induction Principle
Authors:
Maciej Gazda,
Wan Fokkink
Abstract:
We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators.
We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators.
△ Less
Submitted 10 November, 2009;
originally announced November 2009.
-
On Finite Bases for Weak Semantics: Failures versus Impossible Futures
Authors:
Taolue Chen,
Wan Fokkink,
Rob van Glabbeek
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 the axiomatizability of BCCS modulo weak impossible futures semantics.
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 axiomatizability of BCCS modulo weak impossible futures semantics.
△ Less
Submitted 27 October, 2008;
originally announced October 2008.
-
An Analytical Model of Information Dissemination for a Gossip-based Protocol
Authors:
Rena Bakhshi,
Daniela Gavidia,
Wan Fokkink,
Maarten van Steen
Abstract:
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 network, and how fast the item spreads in the network, and how fast the item covers the network. We also determine the optimal size of the exchange buffer, to obtain fast replication. Our results are…
▽ More
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 network, and how fast the item spreads in the network, and how fast the item covers the network. We also determine the optimal size of the exchange buffer, to obtain fast replication. Our results are confirmed by large-scale simulation experiments.
△ Less
Submitted 9 October, 2008;
originally announced October 2008.
-
A Finite Equational Base for CCS with Left Merge and Communication Merge
Authors:
Luca Aceto,
Wan Fokkink,
Anna Ingolfsdottir,
Bas Luttik
Abstract:
Using the left merge and 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, restriction and relabelling. Our equational base is finite if the set of actions is finite.
Using the left merge and 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, restriction and relabelling. Our equational base is finite if the set of actions is finite.
△ Less
Submitted 2 August, 2006; v1 submitted 1 August, 2006;
originally announced August 2006.
-
Split-2 Bisimilarity has a Finite Axiomatization over CCS with<br> Hennessy's Merge
Authors:
Luca Aceto,
Wan Fokkink,
Anna Ingolfsdottir,
Bas Luttik
Abstract:
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 proposed by Hennessy in 1981 to the recursion, relabelling and restriction free fragment of Milner's Calculus of Communicating Systems. Thus the addition of a single binary operation, viz. Hennessy's…
▽ More
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 proposed by Hennessy in 1981 to the recursion, relabelling and restriction free fragment of Milner's Calculus of Communicating Systems. Thus the addition of a single binary operation, viz. Hennessy's merge, is sufficient for the finite equational axiomatization of parallel composition modulo this non-interleaving equivalence. This result is in sharp contrast to a theorem previously obtained by the same authors to the effect that the same language is not finitely based modulo bisimulation equivalence.
△ Less
Submitted 21 June, 2005; v1 submitted 19 January, 2005;
originally announced January 2005.
-
Precongruence Formats for Decorated Trace Semantics
Authors:
B. Bloom,
W. J. Fokkink,
R. J. van Glabbeek
Abstract:
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 specifications using Plotkin's structural approach. For several preorders in the linear time - branching time spectrum a format is given, as general as possible, such that this preorder is a precong…
▽ More
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 specifications using Plotkin's structural approach. For several preorders in the linear time - branching time spectrum a format is given, as general as possible, such that this preorder is a precongruence for all operators specifiable in that format. The formats are derived using the modal characterizations of the corresponding preorders.
△ Less
Submitted 16 April, 2002;
originally announced April 2002.
