论文标题
公理的最大进度和离散时间
Axiomatizing Maximal Progress and Discrete Time
论文作者
论文摘要
米尔纳（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 $τ$ divergent expressions to non-divergent ones by means of the axiom $recX. (τ.X + E) = recX. τ. E$. In the presence of a notion of priority, where, e.g., actions of type $δ$ have a lower priority than silent $τ$ 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 $δ$ 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.
