A cook’s tour of equational axiomatizations for prefix iteration

Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

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, and yields simple iterative behaviours that can be equationally characterized by means of finite collections of axioms. In this paper, we present axiomatic characterizations for a significant fragment of the notions of equivalence and preorder in van Glabbeek’s linear-time/branching-time spectrum over Milner’s basic CCS extended with prefix iteration. More precisely, we consider ready simulation, simulation, readiness, trace and language semantics, and provide complete (in)equational axiomatizations for each of these notions over BCCS with prefix iteration. All of the axiom systems we present are finite, if so is the set of atomic actions under consideration.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings
EditorsMaurice Nivat
PublisherSpringer - Verlag
Pages20-34
Number of pages15
ISBN (Print)3540643001, 9783540643005
Publication statusPublished - 1 Jan 1998
Event1st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998 - Lisbon, Portugal
Duration: 28 Mar 19984 Apr 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1378
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference1st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998
CountryPortugal
CityLisbon
Period28/03/984/04/98

Fingerprint

Axiomatization
Prefix
Stars
Semantics
Iteration
Star Operation
Preorder
Axiom
Axioms
Branching
Linear Time
Fragment
Simulation
Trace
Equivalence
Binary

Cite this

Aceto, L., Fokkink, W., & Ingólfsdóttir, A. (1998). A cook’s tour of equational axiomatizations for prefix iteration. In M. Nivat (Ed.), Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings (pp. 20-34). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1378). Springer - Verlag.
Aceto, Luca ; Fokkink, Wan ; Ingólfsdóttir, Anna. / A cook’s tour of equational axiomatizations for prefix iteration. Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. editor / Maurice Nivat. Springer - Verlag, 1998. pp. 20-34 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5c2f92489a624fecafb4ad62200d421b,
title = "A cook’s tour of equational axiomatizations for prefix iteration",
abstract = "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, and yields simple iterative behaviours that can be equationally characterized by means of finite collections of axioms. In this paper, we present axiomatic characterizations for a significant fragment of the notions of equivalence and preorder in van Glabbeek’s linear-time/branching-time spectrum over Milner’s basic CCS extended with prefix iteration. More precisely, we consider ready simulation, simulation, readiness, trace and language semantics, and provide complete (in)equational axiomatizations for each of these notions over BCCS with prefix iteration. All of the axiom systems we present are finite, if so is the set of atomic actions under consideration.",
author = "Luca Aceto and Wan Fokkink and Anna Ing{\'o}lfsd{\'o}ttir",
year = "1998",
month = "1",
day = "1",
language = "English",
isbn = "3540643001",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer - Verlag",
pages = "20--34",
editor = "Maurice Nivat",
booktitle = "Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings",

}

Aceto, L, Fokkink, W & Ingólfsdóttir, A 1998, A cook’s tour of equational axiomatizations for prefix iteration. in M Nivat (ed.), Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1378, Springer - Verlag, pp. 20-34, 1st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Lisbon, Portugal, 28/03/98.

A cook’s tour of equational axiomatizations for prefix iteration. / Aceto, Luca; Fokkink, Wan; Ingólfsdóttir, Anna.

Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. ed. / Maurice Nivat. Springer - Verlag, 1998. p. 20-34 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1378).

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - A cook’s tour of equational axiomatizations for prefix iteration

AU - Aceto, Luca

AU - Fokkink, Wan

AU - Ingólfsdóttir, Anna

PY - 1998/1/1

Y1 - 1998/1/1

N2 - 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, and yields simple iterative behaviours that can be equationally characterized by means of finite collections of axioms. In this paper, we present axiomatic characterizations for a significant fragment of the notions of equivalence and preorder in van Glabbeek’s linear-time/branching-time spectrum over Milner’s basic CCS extended with prefix iteration. More precisely, we consider ready simulation, simulation, readiness, trace and language semantics, and provide complete (in)equational axiomatizations for each of these notions over BCCS with prefix iteration. All of the axiom systems we present are finite, if so is the set of atomic actions under consideration.

AB - 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, and yields simple iterative behaviours that can be equationally characterized by means of finite collections of axioms. In this paper, we present axiomatic characterizations for a significant fragment of the notions of equivalence and preorder in van Glabbeek’s linear-time/branching-time spectrum over Milner’s basic CCS extended with prefix iteration. More precisely, we consider ready simulation, simulation, readiness, trace and language semantics, and provide complete (in)equational axiomatizations for each of these notions over BCCS with prefix iteration. All of the axiom systems we present are finite, if so is the set of atomic actions under consideration.

UR - http://www.scopus.com/inward/record.url?scp=84947940291&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947940291&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540643001

SN - 9783540643005

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 20

EP - 34

BT - Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings

A2 - Nivat, Maurice

PB - Springer - Verlag

ER -

Aceto L, Fokkink W, Ingólfsdóttir A. A cook’s tour of equational axiomatizations for prefix iteration. In Nivat M, editor, Foundations of Software Science and Computation Structures - 1st International Conference, FoSSaCS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings. Springer - Verlag. 1998. p. 20-34. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).