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

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 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 A Complete Equational Axiomatization for Prefix Iteration with Silent Steps

1995 ◽  
Vol 2 (5) ◽  
Author(s):  
Luca Aceto ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Axiom System ◽  
Subject Classification ◽  
Ams Subject Classification ◽  
Star Operation ◽  
Atomic Action ◽  
Keywords And Phrases ◽  
Bisimulation Equivalence

Fokkink ((1994) Inf. Process. Lett. 52: 333{337) has recently proposed a complete<br />equational axiomatization of strong bisimulation equivalence for MPA_delta^*(A_tau),<br />i.e., the language obtained by extending Milner's basic CCS with prefix iteration.<br />Prefix iteration is a variation on the original binary version of the Kleene star operation<br />p*q obtained by restricting the first argument to be an atomic action. In this<br />paper, we extend Fokkink's results to a setting with the unobservable action by<br />giving a complete equational axiomatization of Milner's observation congruence over<br />MPA_delta^*(A_tau ). <br />The axiomatization is obtained by extending Fokkink's axiom system<br />with two of Milner's standard tau-laws and the following three equations that describe<br />the interplay between the silent nature of tau and prefix iteration:<br />tau . x = tau*x<br />a*(x+tau.y) = a*(x+tau.y + a.y)<br />tau.(a*x) = a*(tau.a*x) .<br />Using a technique due to Groote, we also show that the resulting axiomatization is<br />omega-complete, i.e., complete for equality of open terms.<br />AMS Subject Classification (1991): 68Q40, 68Q42.<br />CR Subject Classification (1991): D.3.1, F.3.2, F.4.2.<br />Keywords and Phrases: Minimal Process Algebra, prefix iteration, equational<br />logic, omega-completeness, observation congruence.

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.

scholarly journals Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation

2006 ◽  
Vol 13 (13) ◽  
Author(s):  
Jirí Srba
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Process Algebra ◽  
Upper And Lower Bounds ◽  
Equivalence Checking ◽  
Basic Process ◽  
Bisimulation Equivalence ◽  
Language Equivalence ◽  
Visibly Pushdown Automata ◽  
Pushdown Automata

We investigate the possibility of (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation, 2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown automata and show that they can be decided in polynomial time.

From the Outside In

2015 ◽  
Author(s):  
Derek Smith
Keyword(s):  
Positive Integer ◽  
Infinite Family ◽  
Open Problems ◽  
The Family

This chapter discusses Slothouber–Graatsma–Conway puzzle, which asks one to assemble six 1 × 2 × 2 pieces and three 1 × 1 × 1 pieces into the shape of a 3 × 3 × 3 cube. The puzzle has been generalized to larger cubes, and there is an infinite family of such puzzles. The chapter's primary argument is that, for any odd positive integer n = 2k + 1, there is exactly one way, up to symmetry, to make an n × n × n cube out of n tiny 1 × 1 × 1 cubes and six of each of a set of rectangular blocks. The chapter describes a way to solve each puzzle in the family and explains why there are no other solutions. It then presents several related open problems.

scholarly journals Risk factors for infant developmental problems

2007 ◽  
Vol 15 (spe) ◽  
pp. 837-842 ◽  
Author(s):  
Margaret Rose Santa Maria-Mengel ◽  
Maria Beatriz Martins Linhares
Keyword(s):  
Family Environment ◽  
Preventive Intervention ◽  
Expressive Language ◽  
Clinical Sample ◽  
Family Health ◽  
Screening Tests ◽  
Developmental Problems ◽  
Family Health Program ◽  
The Family ◽  
Familiar Environment

This descriptive-correlational study aimed to detect risks for child developmental problems in the first four years of age, to identify the protective resources in the familiar environment, and to verify the best predictive variables of the development at risk. The non-clinical sample was composed by 120 children registered in a Family Health Program. The assessment instruments for global development, expressive language and familiar environment were used. The logistic regression analysis indicated that the lower the father's educational level, the higher the risk for developmental problems. Both the history of low nutritional state at six months of age and the psychosocial risk in the family environment increased the chances of having expressive language problems. It is concluded that screening tests of risk for developmental problems and the analysis of the psychosocial factors in the familiar context should be considered as preventive intervention procedure in the Family Health Programs.

Sign in / Sign up

Export Citation Format

Share Document