Priority and maximal progress are completely axiomatisable

Holger Hermanns, Markus Lohrey

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationCONCUR'98 Concurrency Theory
Subtitle of host publication9th International Conference Nice, France, September 8–11, 1998, Proceedings
EditorsDavide Sangiorgi, Robert de Simone
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages237-252
Number of pages16
ISBN (Electronic)978-3-540-68455-8
ISBN (Print)978-3-540-64896-3
DOIs
Publication statusPublished - 1998
Event9th International Conference on Concurrency Theory, CONCUR 1998 - Nice, France
Duration: 8 Sep 199811 Sep 1998
Conference number: 9

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1466
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Workshop

Workshop9th International Conference on Concurrency Theory, CONCUR 1998
Abbreviated titleCONCUR
CountryFrance
CityNice
Period8/09/9811/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

Fingerprint Dive into the research topics of 'Priority and maximal progress are completely axiomatisable'. Together they form a unique fingerprint.

Cite this