paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Axiomatizing Maximal Progress and Discrete Time

公理化最大进度与离散时间
LMCS vol.Volume 17, Issue 12021匹配度 2/10 · 该论文属于并发进程代数与形式语义的公理化理论研究,关注优先级、最大进展与离散时间,并未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向;仅与形式化方法有非常间接的关联。引用 0 inbox
Mario Bravetti
crossref: 2026-09-10

AI 速览

一句话:引入优先级作用域算子 pri(E),给出带优先级与非守卫递归的基本进程代数的完备公理化,解决了用标准观测同余公理化优先级这一长期开放问题。

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

问题
如何用标准观测同余为带优先级的进程代数建立完备公理化;由于优先级(如 δ 低于 τ,源于时间进程代数的最大进度假设)会使 Milner 原有的 τ-发散公理失效,该问题长期未能解决。
方法
引入辅助算子 pri(E) 定义「优先级作用域」,据此为带优先级与非守卫递归的基本进程代数构造公理系统,并将结果扩展到离散时间演算的静态算子,复用与 Jos Baeten 合作中发展的技术处理有限状态项。
评估
以相对于标准观测同余的完备性证明进行评估:先给出基本进程代数(含优先级与非守卫递归)的完备公理化,再证明扩展离散时间静态算子后对有限状态项的完备性。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1350,
  title = {Axiomatizing Maximal Progress and Discrete Time},
  author = {Mario Bravetti},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 1},
  year = {2021},
  doi = {10.23638/lmcs-17(1:1)2021}
}