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