scholarly journals Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge

2004 ◽  
Vol 11 (1) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Bas Luttik
Keyword(s):  
Process Algebra ◽  
Binary Operation ◽  
Sharp Contrast ◽  
Parallel Composition ◽  
Finitely Based ◽  
Finite Axiomatization ◽  
Auxiliary Operation ◽  
Bisimulation Equivalence

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

scholarly journals CCS with Hennessy's Merge has no Finite Equational Axiomatization

2003 ◽  
Vol 10 (34) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Bas Luttik
Keyword(s):  
Process Algebra ◽  
Parallel Composition ◽  
Finitely Based ◽  
Finite Axiomatization ◽  
Bisimulation Equivalence

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 Communicationg 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 is desired.

scholarly journals Bisimilarity is not Finitely Based over BPA with Interrupt

2005 ◽  
Vol 12 (33) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Sumit Nain
Keyword(s):  
Process Algebra ◽  
Sharp Contrast ◽  
Basic Process ◽  
Finitely Based ◽  
Bisimulation Equivalence

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

scholarly journals A Menagerie of Non-Finitely Based Process Semantics over BPA*: From Ready Simulation Semantics to Completed Traces

1996 ◽  
Vol 3 (23) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Linear Time ◽  
Subject Classification ◽  
Regular Expressions ◽  
Basic Process ◽  
Branching Time ◽  
Finitely Based ◽  
Trace Semantics ◽  
Bisimulation Equivalence ◽  
Trace Equivalence

<p>Fokkink and Zantema ((1994) Computer Journal 37:259-267) have shown that<br />bisimulation equivalence has a finite equational axiomatization over the language<br />of Basic Process Algebra with the binary Kleene star operation (BPA*). In light<br />of this positive result on the mathematical tractability of bisimulation equivalence<br />over BPA*, a natural question to ask is whether any other (pre)congruence relation<br />in van Glabbeek's linear time/branching time spectrum is finitely (in)equationally<br />axiomatizable over it. In this paper, we prove that, unlike bisimulation equivalence,<br />none of the preorders and equivalences in van Glabbeek's linear time/branching time<br />spectrum, whose discriminating power lies in between that of ready simulation and<br />that of completed traces, has a finite equational axiomatization. This we achieve by<br />exhibiting a family of (in)equivalences that holds in ready simulation semantics, the<br />finest semantics that we consider, whose instances cannot all be proven by means of<br />any finite set of (in)equations that is sound in completed trace semantics, which is<br />the coarsest semantics that is appropriate for the language BPA*. To this end, for<br />every finite collection of (in)equations that are sound in completed trace semantics, we<br />build a model in which some of the (in)equivalences of the family under consideration<br />fail. The construction of the model mimics the one used by Conway ((1971) Regular<br />Algebra and Finite Machines, page 105) in his proof of a result, originally due to<br />Redko, to the effect that infinitely many equations are needed to axiomatize equality<br />of regular expressions.</p><p>Our non-finite axiomatizability results apply to the language BPA* over an arbitrary<br />non-empty set of actions. In particular, we show that completed trace equivalence<br />is not finitely based over BPA* even when the set of actions is a singleton.<br />Our proof of this result may be easily adapted to the standard language of regular expressions to yield a solution to an open problem posed by Salomaa ((1969) Theory<br />of Automata, page 143).<br />Another semantics that is usually considered in process theory is trace semantics.<br />Trace semantics is, in general, not preserved by sequential composition, and is<br />therefore inappropriate for the language BPA*. We show that, if the set of actions<br />is a singleton, trace equivalence and preorder are preserved by all the operators in<br />the signature of BPA, and coincide with simulation equivalence and preorder, respectively.<br />In that case, unlike all the other semantics considered in this paper, trace<br />semantics have nite, complete equational axiomatizations over closed terms.</p><p> </p><p>AMS Subject Classification (1991): 08A70, 03C05, 68Q10, 68Q40, 68Q45,<br />68Q55, 68Q68, 68Q70.<br />CR Subject Classification (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1.<br />Keywords and Phrases: Concurrency, process algebra, Basic Process Algebra<br />(BPA*), Kleene star, bisimulation, ready simulation, simulation, completed trace semantics,<br />ready trace semantics, failure trace semantics, readiness semantics, failures<br />semantics, trace semantics, equational logic, complete axiomatizations.</p><p> </p>

scholarly journals Bisimilarity is not Finitely Based over BPA with Interrupt

2004 ◽  
Vol 11 (24) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir ◽  
Sumit Nain
Keyword(s):  
Process Algebra ◽  
Basic Process ◽  
Finitely Based ◽  
Bisimulation Equivalence

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 interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based.

Step bisimulation is pomset equivalence on a parallel language without explicit internal choice

1993 ◽  
Vol 3 (1) ◽  
pp. 25-62 ◽  
Author(s):  
Douglas R. Troeger
Keyword(s):  
Equivalence Classes ◽  
Binary Choice ◽  
Parallel Composition ◽  
Focus Attention ◽  
Semantic Level ◽  
Parallel Language ◽  
Bisimulation Equivalence ◽  
Local Nondeterminism ◽  
Trace Equivalence ◽  
Single Set

We focus attention on a language ℒ generated by a set of elementary actions under operations of sequential composition, external binary choice, iteration, and non-nested disjoint parallel composition: that is, on an especially simple parallel language without explicit internal, or ‘local’, nondeterminism. ℒ is nondeterministic, despite the restriction to external choice, since a given action may occur in both subterms F and G of the parallel composition F ║ G. We exhibit a single set of equations that axiomatizes both step bisimulation and pomset equivalence on ℒ Given that step bisimulation and pomset equivalence are incomparable on the language ℒ+ obtained from ℒ by relaxing just the constraint on choice, the coincidence of these equivalences on ℒ suggests that the elimination of explicit internal choice can result in simplifications at the semantic level. We reinforce this impression by showing for ℒ that step bisimulation (i) coincides with pomset bisimulation equivalence, (ii) is real-time consistent, and (iii) has step trees as concrete representatives of its equivalence classes. Moreover, we show that none of these results holds for the language ℒ+ Finally, step trace equivalence is proved not to coincide with step bisimulation equivalence on ℒ.

scholarly journals On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt

2007 ◽  
Vol 14 (5) ◽  
Author(s):  
Luca Aceto ◽  
Silvio Capobianco ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Basic Process ◽  
Single Action ◽  
Finite Axiomatization ◽  
Finite Base ◽  
Special Case ◽  
Trace Equivalence

We study Basic Process Algebra with interrupt modulo complete trace equivalence. We show that, unlike in the setting of the more demanding bisimilarity, a ground complete finite axiomatization exists. We explicitly give such an axiomatization, and extend it to a finite complete one in the special case when a single action is present.

scholarly journals Semantic Foundations for Deterministic Dataflow and Stream Processing

2020 ◽  
pp. 394-427 ◽  
Author(s):  
Konstantinos Mamouras
Keyword(s):  
Binary Operation ◽  
Stream Processing ◽  
Query Languages ◽  
Programming Models ◽  
Parallel Composition ◽  
Monotone Functions ◽  
Semantic Framework ◽  
Abstract Machines ◽  
Full Class ◽  
Infinite State

AbstractWe propose a denotational semantic framework for deterministic dataflow and stream processing that encompasses a variety of existing streaming models. Our proposal is based on the idea that data streams, stream transformations, and stream-processing programs should be classified using types. The type of a data stream is captured formally by a monoid, an algebraic structure with a distinguished binary operation and a unit. The elements of a monoid model the finite fragments of a stream, the binary operation represents the concatenation of stream fragments, and the unit is the empty fragment. Stream transformations are modeled using monotone functions on streams, which we call stream transductions. These functions can be implemented using abstract machines with a potentially infinite state space, which we call stream transducers. This abstract typed framework of stream transductions and transducers can be used to (1) verify the correctness of streaming computations, that is, that an implementation adheres to the desired behavior, (2) prove the soundness of optimizing transformations, e.g. for parallelization and distribution, and (3) inform the design of programming models and query languages for stream processing. In particular, we show that several useful combinators can be supported by the full class of stream transductions and transducers: serial composition, parallel composition, and feedback composition.

scholarly journals A Note on an Expressiveness Hierarchy for Multi-exit Iteration

2002 ◽  
Vol 9 (40) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir
Keyword(s):  
Positive Integer ◽  
Process Algebra ◽  
Expressive Language ◽  
Basic Process ◽  
Star Operation ◽  
The Family ◽  
Bisimulation Equivalence

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 form<br />X_1 = P_1 X_2 + Q_1 <br /><br /> X_n = P_n X_1 + Q_n <br /><br /> where n is a positive integer, and the P_i and the Q_i are process terms. The addition of multi-exit iteration to Basic Process Algebra (BPA) yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star. This note offers an expressiveness hierarchy, modulo bisimulation equivalence, for the family of multi-exit iteration operators proposed by Bergstra, Bethke and Ponse.

scholarly journals On the Axiomatizability of Priority

2006 ◽  
Vol 13 (1) ◽  
Author(s):  
Luca Aceto ◽  
Taolue Chen ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Sufficient Conditions ◽  
Equational Theory ◽  
Complete Axiomatization ◽  
Bisimulation Equivalence ◽  
Arbitrary Collection ◽  
Infinite Set ◽  
Priority Structure

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 the presence of an infinite set of actions, bisimulation equivalence has no finite, sound, ground-complete equational axiomatization over that language. This negative result applies even if the syntax is extended with an arbitrary collection of auxiliary operators, and motivates the study of axiomatizations using conditional equations. In the presence of an infinite set of actions, it is shown that, in general, bisimulation equivalence has no finite, sound, ground-complete axiomatization consisting of conditional equations over the language studied in this paper. Finally, sufficient conditions on the priority structure over actions are identified that lead to a finite, ground-complete axiomatization of bisimulation equivalence using conditional equations.

Sign in / Sign up

Export Citation Format

Share Document