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

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

Download Full-text

A menagerie of non-finitely based process semantics over BPA* – from ready simulation to completed traces

Mathematical Structures in Computer Science ◽

10.1017/s0960129597002491 ◽

1998 ◽

Vol 8 (3) ◽

pp. 193-230 ◽

Cited By ~ 18

Author(s):

LUCA ACETO ◽

WAN FOKKINK ◽

ANNA INGÓLFSDÓTTIR

Keyword(s):

Linear Time ◽

Time Spectrum ◽

Finite Collection ◽

Regular Expressions ◽

Branching Time ◽

Finitely Based ◽

Finite Set ◽

Trace Semantics ◽

Bisimulation Equivalence ◽

Trace Equivalence

Fokkink and Zantema (Fokkink and Zantema 1994) have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary Kleene star operation (BPA*). In light of this positive result on the mathematical tractability of bisimulation equivalence over BPA*, a natural question to ask is whether any other (pre)congruence relation in van Glabbeek's linear time/branching time spectrum is finitely (in)equationally axiomatizable over it. In this paper, we prove that, unlike bisimulation equivalence, none of the preorders and equivalences in van Glabbeek's linear time/branching time spectrum, whose discriminating power lies in between that of ready simulation and that of completed traces, has a finite equational axiomatization. This we achieve by exhibiting a family of (in)equivalences that holds in ready simulation semantics (which is the finest semantics that we consider) and whose instances cannot all be proved by means of any finite set of (in)equations that is sound in completed trace semantics (which is the coarsest semantics that is appropriate for the language BPA*). To this end, for every finite collection of (in)equations that are sound in completed trace semantics, we build a model in which some of the (in)equivalences of the family under consideration fail. The construction of the model mimics the one used by Conway (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 non-finite axiomatizability results apply to the language BPA* over an arbitrary non-empty set of actions. In particular, we show that completed trace equivalence is not finitely based over BPA* even when the set of actions is a singleton. Our proof of this result may be adapted to the standard language of regular expressions to yield a solution to an open problem posed by Salomaa (Salomaa 1969, p. 143).Another semantics that is usually considered in process theory is trace semantics. Trace semantics is, in general, not preserved by sequential composition, and is therefore inappropriate for the language BPA*. We show that, if the set of actions is a singleton, trace equivalence and preorder are preserved by all the operators in the signature of BPA*, and coincide with simulation equivalence and preorder, respectively. In that case, unlike all the other semantics considered in this paper, trace semantics have finite, complete equational axiomatizations over closed terms.

Download Full-text

Bisimilarity is not Finitely Based over BPA with Interrupt

BRICS Report Series ◽

10.7146/brics.v12i33.21900 ◽

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.

Download Full-text

Ready To Preorder: Get Your BCCSP Axiomatization for Free!

BRICS Report Series ◽

10.7146/brics.v14i3.21926 ◽

2007 ◽

Vol 14 (3) ◽

Cited By ~ 2

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.

Download Full-text

Bisimilarity is not Finitely Based over BPA with Interrupt

BRICS Report Series ◽

10.7146/brics.v11i24.21849 ◽

2004 ◽

Vol 11 (24) ◽

Cited By ~ 1

Author(s):

Luca Aceto ◽

Willem Jan Fokkink ◽

Anna Ingólfsdóttir ◽

Sumit Nain

Keyword(s):

Process Algebra ◽

Basic Process ◽

Finitely Based ◽

Bisimulation Equivalence

Download Full-text

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

BRICS Report Series ◽

10.7146/brics.v14i5.21928 ◽

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.

Download Full-text

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

BRICS Report Series ◽

10.7146/brics.v11i1.21826 ◽

2004 ◽

Vol 11 (1) ◽

Cited By ~ 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.

Download Full-text

A Note on an Expressiveness Hierarchy for Multi-exit Iteration

BRICS Report Series ◽

10.7146/brics.v9i40.21755 ◽

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 X_1 = P_1 X_2 + Q_1 X_n = P_n X_1 + Q_n 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.

Download Full-text

Highly Undecidable Questions for Process Algebras

BRICS Report Series ◽

10.7146/brics.v11i8.21833 ◽

2004 ◽

Vol 11 (8) ◽

Author(s):

Petr Jancar ◽

Jirí Srba

Keyword(s):

Petri Nets ◽

Process Algebra ◽

Basic Process ◽

Process Algebras ◽

Parallel Processes ◽

Pushdown Automata ◽

Trace Equivalence

We show Sigma^1_1-completeness of weak bisimilarity for PA (process algebra), and of weak simulation preorder/equivalence for PDA (pushdown automata), PA and PN (Petri nets). We also show Pi^1_1-hardness of weak omega-trace equivalence for the (sub)classes BPA (basic process algebra) and BPP (basic parallel processes).

Download Full-text

Finite Equational Bases in Process Algebra: Results and Open Questions

BRICS Report Series ◽

10.7146/brics.v12i19.21885 ◽

2005 ◽

Vol 12 (19) ◽

Author(s):

Luca Aceto ◽

Willem Jan Fokkink ◽

Anna Ingólfsdóttir ◽

Bas Luttik

Keyword(s):

Process Algebra ◽

State Of The Art ◽

Linear Time ◽

Time Spectrum ◽

Parallel Composition ◽

Basic Process ◽

Process Algebras ◽

Open Questions ◽

The Subject ◽

Sequential Processes

Van Glabbeek (1990) presented the linear time-branching time spectrum of behavioral equivalences for finitely branching, concrete, sequential processes. He studied these semantics in the setting of the basic process algebra BCCSP, and tried to give finite complete and omega-complete axiomatizations for them. (An axiomatization E is omega-complete when an equation can be derived from E if, and only if, all its closed instantiations can be derived from E.) Obtaining such axiomatizations in concurrency theory often turns out to be difficult, even in the setting of simple languages like BCCSP. This has raised a host of open questions that have been the subject of intensive research in recent years. Most of these questions have been settled over BCCSP, either positively by giving a finite complete or omega-complete axiomatization, or negatively by proving that such an axiomatization does not exist. Still some open questions remain. This paper reports on these results, and on the state-of-the-art on axiomatizations for richer process algebras, containing constructs like sequential and parallel composition.

Download Full-text

An Equational Axiomatization for Multi-Exit Iteration

BRICS Report Series ◽

10.7146/brics.v3i22.19985 ◽

1996 ◽

Vol 3 (22) ◽

Cited By ~ 1

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

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 = P1 X2 + Q1 ... Xn = Pn X1 + Qnwhere n is a positive integer, and the Pi and the Qi 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 of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.

Download Full-text