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.

On the axiomatisability of priority

2008 ◽  
Vol 18 (1) ◽  
pp. 5-28 ◽  
Author(s):  
LUCA ACETO ◽  
TAOLUE CHEN ◽  
WAN FOKKINK ◽  
ANNA INGOLFSDOTTIR
Keyword(s):  
Process Algebra ◽  
Sufficient Conditions ◽  
Equational Theory ◽  
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. We prove that, in the presence of an infinite set of actions, bisimulation equivalence has no finite, sound, ground-complete equational axiomatisation 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 axiomatisations using equations with action predicates as conditions. In the presence of an infinite set of actions, it is shown that, in general, bisimulation equivalence has no finite, sound, ground-complete axiomatisation consisting of equations with action predicates as conditions 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 axiomatisation of bisimulation equivalence using equations with action predicates as conditions.

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 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 Ready To Preorder: Get Your BCCSP Axiomatization for Free!

2007 ◽  
Vol 14 (3) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Linear Time ◽  
Equational Theory ◽  
Time Spectrum ◽  
Basic Process ◽  
Branching Time ◽  
Discriminating Power

This paper contributes to the study of the equational theory of the semantics in van Glabbeek's linear time - branching time spectrum over the language BCCSP, a basic process algebra for the description of finite synchronization trees. It offers an algorithm for producing a complete (respectively, ground-complete) equational axiomatization of a behavioral congruence lying between ready simulation equivalence and partial traces equivalence from a complete (respectively, ground-complete) inequational axiomatization of its underlying precongruence--that is, of the precongruence whose kernel is the equivalence. The algorithm preserves finiteness of the axiomatization when the set of actions is finite. It follows that each equivalence in the spectrum whose discriminating power lies in between that of ready simulation and partial traces equivalence is finitely axiomatizable over the language BCCSP if so is its defining preorder.

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 Bisimulations for Asynchronous Mobile Processes

1996 ◽  
Vol 3 (8) ◽  
Author(s):  
Martin Hansen ◽  
Hans Hüttel ◽  
Josva Kleist
Keyword(s):  
Equational Theory ◽  
Surprising Result ◽  
Process Calculus ◽  
Process Calculi ◽  
The Past ◽  
Pi Calculus ◽  
Mobile Process ◽  
Bisimulation Equivalence ◽  
Mobile Processes

Within the past few years there has been renewed interest in the<br />study of value-passing process calculi as a consequence of the emergence of the pi-calculus. Here, [MPW89] have determined two variants of the notion of bisimulation, late and early bisimilarity. Most recently [San93] has proposed the new notion of open bisimulation equivalence. <br />In this paper we consider Plain LAL, a mobile process calculus which differs from the pi-calculus in the sense that the communication of data values happens asynchronously. The surprising result is that in the presence of asynchrony, the open, late and early bisimulation equivalences coincide - this in contrast to the pi-calculus where they are distinct. The result allows us to formulate a common equational theory which is sound and complete for finite terms of Plain LAL.

scholarly journals A Complete Equational Axiomatization for MPA with String Iteration

1995 ◽  
Vol 2 (28) ◽  
Author(s):  
Luca Aceto ◽  
Jan Friso Groote
Keyword(s):  
Positive Integer ◽  
Whole Language ◽  
Equational Theory ◽  
Atomic Actions ◽  
Star Operation ◽  
Bisimulation Equivalence ◽  
Countably Infinite

We study equational axiomatizations of bisimulation equivalence for the language obtained by extending Milner's basic CCS with string iteration. String iteration is a variation on the original binary version of the Kleene star operation p*q obtained by restricting the first argument to be a non-empty sequence of atomic actions. We show that, for every positive integer k, bisimulation equivalence over the set of processes in this language with loops of length at most k is finitely axiomatizable. We also offer a countably infinite equational theory that completely axiomatizes bisimulation equivalence over the whole language. We prove that this result cannot be improved upon by showing that no finite equational axiomatization of bisimulation equivalence over basic CCS with string iteration can exist, unless the set of actions is empty.

scholarly journals An Equational Axiomatization for Multi-Exit Iteration

1996 ◽  
Vol 3 (22) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink
Keyword(s):  
Positive Integer ◽  
Process Algebra ◽  
Expressive Language ◽  
General Structure ◽  
Basic Process ◽  
Star Operation ◽  
The Family ◽  
Bisimulation Equivalence

<p>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<br />of systems of recursion equations of the form</p><p>X1 = P1 X2 + Q1<br />...<br />Xn = Pn X1 + Qn</p><p>where n is a positive integer, and the Pi and the Qi are process terms. The addition<br />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<br />consequence, the proof of completeness of the proposed equational axiomatization<br />for this language, although standard in its general structure, is much more involved<br />than that for BPA. An expressiveness hierarchy for the family of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.</p><p> </p>

Sign in / Sign up

Export Citation Format

Share Document