Tech Reports

Tech Report kmi-05-06 Abstract

A Complete Axiomatisation of Observation Congruence for Deterministic Time under Maximal Progress
Techreport ID: kmi-05-06
Date: 2005
Author(s): Barry Norton

This report presents a process calculus CaSE, derived from CCS by extension with transitions, labelled in multiple abstract clocks, that are both deterministic and governed by maximal progress. Two open problems in the literature have prevented a complete axiomatisation of the coarsest congruence within weak bisimulation in such a system. The main result contained here is the proof of soundness and completeness of an axiom system with respect to this congruence.