Axiomatizing Maximal Progress and Discrete Time

摘要

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