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