Priority and maximal progress are completely axiomatisable

Holger Hermanns; Markus Lohrey

doi:10.1007/BFb0055611

Priority and maximal progress are completely axiomatisable

Holger Hermanns, Markus Lohrey

Faculty of Electrical Engineering, Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

17 Citations (Scopus)

Abstract

During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi.

Original language	English
Title of host publication	CONCUR'98 Concurrency Theory
Subtitle of host publication	9th International Conference Nice, France, September 8–11, 1998, Proceedings
Editors	Davide Sangiorgi, Robert de Simone
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	237-252
Number of pages	16
ISBN (Electronic)	978-3-540-68455-8
ISBN (Print)	978-3-540-64896-3
DOIs	https://doi.org/10.1007/BFb0055611
Publication status	Published - 1998
Event	9th International Conference on Concurrency Theory, CONCUR 1998 - Nice, France Duration: 8 Sept 1998 → 11 Sept 1998 Conference number: 9

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1466
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	9th International Conference on Concurrency Theory, CONCUR 1998
Abbreviated title	CONCUR
Country/Territory	France
City	Nice
Period	8/09/98 → 11/09/98

Keywords

FMT-PA: PROCESS ALGEBRAS
FMT-PM: PROBABILISTIC METHODS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
Proof system
Axiom system
Parallel composition
Process algebra
Continuous time
Markov chain

Access to Document

10.1007/BFb0055611

Cite this

@inproceedings{95d86406637f41448d62d24edf8be31b,

title = "Priority and maximal progress are completely axiomatisable",

abstract = "During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi.",

keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-PM: PROBABILISTIC METHODS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, Proof system, Axiom system, Parallel composition, Process algebra, Continuous time, Markov chain",

author = "Holger Hermanns and Markus Lohrey",

year = "1998",

doi = "10.1007/BFb0055611",

language = "English",

isbn = "978-3-540-64896-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "237--252",

editor = "Davide Sangiorgi and {de Simone}, Robert",

booktitle = "CONCUR'98 Concurrency Theory",

note = "9th International Conference on Concurrency Theory, CONCUR 1998, CONCUR ; Conference date: 08-09-1998 Through 11-09-1998",

}

Hermanns, H & Lohrey, M 1998, Priority and maximal progress are completely axiomatisable. in D Sangiorgi & R de Simone (eds), CONCUR'98 Concurrency Theory: 9th International Conference Nice, France, September 8–11, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1466, Springer, Berlin, Heidelberg, pp. 237-252, 9th International Conference on Concurrency Theory, CONCUR 1998, Nice, France, 8/09/98. https://doi.org/10.1007/BFb0055611

Priority and maximal progress are completely axiomatisable. / Hermanns, Holger; Lohrey, Markus.
CONCUR'98 Concurrency Theory: 9th International Conference Nice, France, September 8–11, 1998, Proceedings. ed. / Davide Sangiorgi; Robert de Simone. Berlin, Heidelberg: Springer, 1998. p. 237-252 (Lecture Notes in Computer Science; Vol. 1466).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Priority and maximal progress are completely axiomatisable

AU - Hermanns, Holger

AU - Lohrey, Markus

N1 - Conference code: 9

PY - 1998

Y1 - 1998

N2 - During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi.

AB - During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi.

KW - FMT-PA: PROCESS ALGEBRAS

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - Proof system

KW - Axiom system

KW - Parallel composition

KW - Process algebra

KW - Continuous time

KW - Markov chain

U2 - 10.1007/BFb0055611

DO - 10.1007/BFb0055611

M3 - Conference contribution

SN - 978-3-540-64896-3

T3 - Lecture Notes in Computer Science

SP - 237

EP - 252

BT - CONCUR'98 Concurrency Theory

A2 - Sangiorgi, Davide

A2 - de Simone, Robert

PB - Springer

CY - Berlin, Heidelberg

T2 - 9th International Conference on Concurrency Theory, CONCUR 1998

Y2 - 8 September 1998 through 11 September 1998

ER -

Priority and maximal progress are completely axiomatisable

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this