一句话:引入优先级作用域算子 pri(E),给出带优先级与非守卫递归的基本进程代数的完备公理化,解决了用标准观测同余公理化优先级这一长期开放问题。
论文研究进程代数中优先级的公理化问题。Milner 关于观测同余的完备证明系统关键依赖于公理 recX.(τ.X+E)=recX.τ.E,但当存在优先级概念(如 δ 动作优先级低于静默 τ 动作)时该公理不再可靠;而这类优先级在时间进程代数中因最大进度假设而自然出现,其中 δ 被解释为时间延迟。作者提出引入辅助算子 pri(E) 来定义「优先级作用域」,在标准观测同余框架下给出了带优先级与非守卫递归的基本进程代数的完备公理化,从而解决了这一长期悬而未决的问题。进一步地,当用离散时间演算的静态算子扩展该设置后,通过复用与 Jos Baeten 合作中发展的技术,可构造出在(某类)有限状态项上完备的公理化。
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.