An expressive logic for Basic Process Algebra

1993 ◽  
pp. 453-462
Author(s):  
A. Fantechi ◽  
S. Gnesi ◽  
V. Perticaroli
Keyword(s):  
Process Algebra ◽  
Basic Process

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 Basic process algebra with deadlocking states

2001 ◽  
Vol 266 (1-2) ◽  
pp. 605-630 ◽  
Author(s):  
Jiřı́ Srba
Keyword(s):  
Process Algebra ◽  
Basic Process

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 Complexity of Weak Bisimilarity and Regularity for BPA and BPP

2000 ◽  
Vol 7 (16) ◽  
Author(s):  
Jirí Srba
Keyword(s):  
Lower Bound ◽  
Open Problem ◽  
Process Algebra ◽  
Basic Process ◽  
Restricted Class ◽  
Parallel Processes ◽  
Weak Regularity ◽  
Np Hardness

It is an open problem whether weak bisimilarity is decidable<br />for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A<br />PSPACE lower bound for BPA and NP lower bound for BPP have been<br />demonstrated by Stribrna. Mayr achieved recently a result, saying that<br />weak bisimilarity for BPP is Pi^P_2-hard. We improve this lower bound to<br />PSPACE, moreover for the restricted class of normed BPP.<br />Weak regularity (finiteness) of BPA and BPP is not known to be decidable<br />either. In the case of BPP there is a Pi^P_2-hardness result by Mayr,<br />which we improve to PSPACE. No lower bound has previously been established<br />for BPA. We demonstrate DP-hardness, which in particular<br />implies both NP and co-NP-hardness.<br />In each of the bisimulation/regularity problems we consider also the<br />classes of normed processes.

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.

Highly Undecidable Questions for Process Algebras

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

scholarly journals Finite Equational Bases in Process Algebra: Results and Open Questions

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.

Sign in / Sign up

Export Citation Format

Share Document