  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.
