Axiomatizing Prefix Iteration with Silent Steps

Luca Aceto; Willem Jan Fokkink; Rob J. van Glabbeek; Anna Ingólfsdóttir

doi:10.7146/brics.v2i56.19957

Axiomatizing Prefix Iteration with Silent Steps

BRICS Report Series ◽

10.7146/brics.v2i56.19957 ◽

1995 ◽

Vol 2 (56) ◽

Cited By ~ 2

Author(s):

Luca Aceto ◽

Willem Jan Fokkink ◽

Rob J. van Glabbeek ◽

Anna Ingólfsdóttir

Keyword(s):

Process Algebra ◽

Direct Proof ◽

Completeness Theorem ◽

Subject Classification ◽

Star Operation ◽

Weak Bisimulation ◽

Keywords And Phrases ◽

Completeness Result ◽

Considerable Simplification ◽

Branching Bisimulation

Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. branching congruence, eta-congruence, delay congruence and weak congruence. The completeness proofs for eta-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e. terms that may contain process variables. As a by-product, the omega-completeness of the axiomatizations is obtained as well as their completeness for closed terms. AMS Subject Classification (1991): 68Q10, 68Q40, 68Q55. CR Subject Classification (1991): D.3.1, F.1.2, F.3.2. Keywords and Phrases: Concurrency, process algebra, basic CCS, prefix iteration, branching bisimulation, eta-bisimulation, delay bisimulation, weak bisimulation, equational logic, complete axiomatizations.

Download Full-text

A Complete Equational Axiomatization for Prefix Iteration with Silent Steps

BRICS Report Series ◽

10.7146/brics.v2i5.19507 ◽

1995 ◽

Vol 2 (5) ◽

Cited By ~ 2

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

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

A completeness theorem for Zermelo-Fraenkel set theory

Journal of Symbolic Logic ◽

10.1017/s0022481200051379 ◽

1976 ◽

Vol 41 (2) ◽

pp. 323-327 ◽

Cited By ~ 1

Author(s):

William C. Powell

Keyword(s):

Set Theory ◽

Ad Hoc ◽

Completeness Theorem ◽

Explicit Formulation ◽

Completeness Result ◽

Close Relationship ◽

Unary Relation ◽

Law Of Excluded Middle ◽

Excluded Middle

We provide a semantics for Zermelo-Fraenkel set theory. The semantics was essentially given by W. Ackermann [1], and the proof of completeness follows from a lemma of Levy [4]. Furthermore, a close relationship between Ackermann's set theory and Zermelo-Fraenkel set theory has been established by Levy [4] and Reinhardt [6]. Thus, any interest in this paper must consist solely in the explicit formulation of the completeness result and the consequential evidence of the fundamental character of Ackermann's principle and the ad hoc character of the full law of excluded middle and the strong transitivity of Ackermann's unary relation

Download Full-text

Algebraic completeness results for R-mingle and its extensions

Journal of Symbolic Logic ◽

10.1017/s0022481200092161 ◽

1970 ◽

Vol 35 (1) ◽

pp. 1-13 ◽

Cited By ~ 22

Author(s):

J. Michael Dunn

Keyword(s):

Algebraic Logic ◽

Completeness Theorem ◽

Strong Completeness ◽

Finite Characteristic ◽

Sentential Calculus ◽

Completeness Result

Schiller Joe Scroggs in [9] established remarkable facts concerning “normal” extensions of the modal sentential calculus S5, the most notable of these facts being that all such proper extensions have finite characteristic matrices. The major import of the present paper is that like facts hold for the relevant sentential calculus R-Mingle (RM). Robert K. Meyer in [6] has obtained an important completeness result for RM, which will play a central role in our results. However, in §2 we shall obtain a new proof of Meyer's result as a by-product of the algebraic logic that we develop in §1. Also in §2 we shall obtain the promised results for extensions of RM. In §3 we shall provide a strong completeness theorem for RM by generalizing the semantics of Meyer.

Download Full-text

A proof of completeness for continuous first-order logic

Journal of Symbolic Logic ◽

10.2178/jsl/1264433914 ◽

2010 ◽

Vol 75 (1) ◽

pp. 168-190 ◽

Cited By ~ 14

Author(s):

Itaï Ben Yaacov ◽

Arthur Paul Pedersen

Keyword(s):

Model Theory ◽

Completeness Theorem ◽

Order Logic ◽

First Order Logic ◽

Complete Theory ◽

Strong Completeness ◽

First Order ◽

Completeness Result ◽

Metric Structures ◽

Natural Classes

AbstractContinuous first-order logic has found interest among model theorists who wish to extend the classical analysis of “algebraic” structures (such as fields, group, and graphs) to various natural classes of complete metric structures (such as probability algebras, Hilbert spaces, and Banach spaces). With research in continuous first-order logic preoccupied with studying the model theory of this framework, we find a natural question calls for attention. Is there an interesting set of axioms yielding a completeness result?The primary purpose of this article is to show that a certain, interesting set of axioms does indeed yield a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies anapproximatedform of strong completeness, whereby Σ⊧φ(if and) only if Σ⊢φ∸2−nfor alln < ω. This approximated form of strong completeness asserts that if Σ⊧φ, then proofs from Σ, being finite, can provide arbitrarily better approximations of the truth ofφ.Additionally, we consider a different kind of question traditionally arising in model theory—that of decidability. When is the set of all consequences of a theory (in a countable, recursive language) recursive? Say that a complete theoryTisdecidableif for every sentenceφ, the valueφTis a recursive real, and moreover, uniformly computable fromφ. IfTis incomplete, we say it is decidable if for every sentenceφthe real numberφTois uniformly recursive fromφ, whereφTois the maximal value ofφconsistent withT. As in classical first-order logic, it follows from the completeness theorem of continuous first-order logic that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable.

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

On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers

BRICS Report Series ◽

10.7146/brics.v6i22.20079 ◽

1999 ◽

Vol 6 (22) ◽

Cited By ~ 1

Author(s):

Luca Aceto ◽

Zoltán Ésik ◽

Anna Ingólfsdóttir

Keyword(s):

Process Algebra ◽

Equational Theory ◽

Finite Basis ◽

Alternative Proof ◽

Equational Logic ◽

Basic Process ◽

Natural Numbers ◽

Binary Operations ◽

Keywords And Phrases ◽

Trace Equivalence

This paper shows that the collection of identities in two variables which hold in the algebra N of the natural numbers with constant zero, and binary operations of sum and maximum does not have a finite equational axiomatization. This gives an alternative proof of the non-existence of a finite basis for N - a result previously obtained by the authors. As an application of the main theorem, it is shown that the language of Basic Process Algebra (over a singleton set of actions), with or without the empty process, has no finite omega-complete equational axiomatization modulo trace equivalence. AMS Subject Classification (1991): 08A70, 08B05, 03C05, 68Q70. ACM Computing Classification System (1998): F.4.1. Keywords and Phrases: Equational logic, varieties, complete axiomatizations, process algebra, trace equivalence.

Download Full-text

On the Finitary Bisimulation

BRICS Report Series ◽

10.7146/brics.v2i59.19960 ◽

1995 ◽

Vol 2 (59) ◽

Cited By ~ 1

Author(s):

Luca Aceto ◽

Anna Ingólfsdóttir

Keyword(s):

Denotational Semantics ◽

Subject Classification ◽

Process Algebras ◽

Transition Systems ◽

Behavioural Observation ◽

Labelled Transition Systems ◽

Full Abstraction ◽

Ams Subject Classification ◽

Keywords And Phrases

The finitely observable, or finitary, part of bisimulation is a key tool in establishing full abstraction results for denotational semantics for process algebras with respect to bisimulation-based preorders. A bisimulation-like characterization of this relation for arbitrary transition systems is given, relying on Abramsky's characterization in terms of the finitary domain logic. More informative behavioural, observation-independent characterizations of the finitary bisimulation are also offered for several interesting classes of transition systems. These include transition systems with countable action sets, those that have bounded convergent sort and the sort-finite ones. The result for sort-finite transition systems sharpens a previous behavioural characterization of the finitary bisimulation for this class of structures given by Abramsky. AMS Subject Classification (1991): 68Q10 (Modes of computation), 68Q55 (Semantics), 03B70 (Logic of Programming), 68Q90 (Transition nets). Keywords and Phrases: Concurrency, labelled transition systems with divergence, bisimulation preorder, finitary relations, domain logic for transition systems.

Download Full-text

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

BRICS Report Series ◽

10.7146/brics.v3i23.20003 ◽

1996 ◽

Vol 3 (23) ◽

Cited By ~ 1

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

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

On a Question of Arto Salomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based

BRICS Report Series ◽

10.7146/brics.v3i36.20018 ◽

1996 ◽

Vol 3 (36) ◽

Author(s):

Luca Aceto ◽

Willem Jan Fokkink ◽

Anna Ingólfsdóttir

Keyword(s):

Equational Theory ◽

Negative Answer ◽

Subject Classification ◽

Finite Collection ◽

Regular Expressions ◽

Regular Algebra ◽

Keywords And Phrases ◽

Regular Equation ◽

Theoretic Argument ◽

The One

Salomaa ((1969) Theory of Automata, page 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative answer to this long standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. 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 analysis of the model, however, needs to be more refined than the one provided by Conway ibidem.AMS Subject Classification (1991): 08A70, 03C05, 68Q45, 68Q68, 68Q70. CR Subject Classification (1991): D.3.1, F.1.1, F.4.1. Keywords and Phrases: Regular expressions, equational logic, complete axiomatizations.

Download Full-text