paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Failure Trace Semantics for a Process Algebra with Time-outs

带超时算子的进程代数的失败迹语义
LMCS vol.Volume 17, Issue 22021匹配度 1/10 · 该论文属于纯进程代数与形式语义研究,讨论超时算子的失败迹语义与同余闭包,与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析等方向几乎没有交集。引用 4 inbox
Rob van Glabbeek
crossref: 2026-09-10

AI 速览

一句话:为进程代数引入超时算子并给出其失败迹语义,刻画迹等价与失败等价的同余闭包。

本文在标准进程代数上增加超时(time-out)算子,以提升其绝对表达力,同时仍保持无时间进程代数框架:时间的推进不被量化,也不显式建模时间度量。作者研究该扩展下行为等价的同余性,指出迹等价(trace equivalence)和失败等价(failures equivalence)对超时算子不再是同余关系。为恢复组合推理,论文将它们的同余闭包刻画为失败迹等价(failure trace equivalence),并由此给出适合该算子的失败迹语义。该工作为带超时的并发进程提供语义基础,展示如何在无时间设定中处理超时行为。

问题
如何在保持无时间进程代数框架的同时,为进程代数加入超时算子以提升表达力,并恢复行为等价的同余性。
方法
扩展标准进程代数并定义超时算子,分析迹等价与失败等价在该算子下的同余失效,证明其同余闭包恰好是失败迹等价。
评估
评估方式为形式化理论证明与等价关系分析,给出同余闭包刻画与表达力结论,而非实验评估。
原文摘要(Abstract)

This paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra, in the sense that the progress of time is not quantified. Trace and failures equivalence fail to be congruences for this operator; their congruence closure is characterised as failure trace equivalence.

链接与引用

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

BibTeX
@article{paperbot1316,
  title = {Failure Trace Semantics for a Process Algebra with Time-outs},
  author = {Rob van Glabbeek},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 2},
  year = {2021},
  doi = {10.23638/lmcs-17(2:11)2021}
}