Observational Congruence in a Stochastic Timed Calculus with Maximal Progress

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 [31]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by the axiom recX:(ø:X + P ) = recX:ø:P . In this paper we discuss observational congruence in the context of a simple stochastic timed 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. Therefore, 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. 1 Introduction One of the outst..