Axiomatizing Maximal Progress And Discrete Time

Milner's complete proof system for observational congruence is crucially based on the possibility to equate tau divergent expressions to non-divergent ones by means of the axiom recX.(tau.X E) = recX.tau.E. In the presence of a notion of priority, where, e.g., actions of type delta have a lower priority than silent tau actions, this axiom is no longer sound. Such a form of priority is, however, common in timed process algebra, where, due to the interpretation of delta as a time delay, it naturally arises from the maximal progress assumption. We here present our solution, based on introducing an auxiliary operator pri(E) defining a "priority scope" , to the long time open problem of axiomatizing priority using standard observational congruence: we provide a complete axiomatization for a basic process algebra with priority and (unguarded) recursion. We also show that, when the setting is extended by considering static operators of a discrete time calculus, an axiomatization that is complete over (a characterization of) finite-state terms can be developed by re-using techniques devised in the context of a cooperation with Prof. Jos Baeten.