paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Behavioural equivalences for timed systems

Timed 系统的行为等价关系
LMCS vol.Volume 15, Issue 12019匹配度 1/10 · 该论文属于纯形式语义/进程代数方向,研究 timed transition systems 的行为等价谱系,与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接交集。虽然形式化验证与用户兴趣有微弱关联,但本文不涉及 LLM 或程序分析工具,因此匹配度很低。引用 2 inbox
Tomasz Brengos, Marco Peressotti
crossref: 2026-09-10

AI 速览

一句话:首次提出统一的 timed 行为模型框架,将各种 timed 行为等价按区分力统一为谱系。

Timed transition systems 显式处理时间流逝,是多种进程演算与自动机的语义模型,但其一般数学刻画和行为理论仍缺失。本文提出首个统一框架来研究 timed 行为模型,涵盖 timed bisimulation、timed language equivalence 及其 weak 和 time-abstract 对应物。作者在抽象层面组织这些等价关系,并证明它们按区分能力构成一个谱系;该结论不依赖于具体系统类型,而适用于 timed transition system 的任何推广。最后将框架实例化到 timed transition systems 及其定量扩展(如 timed probabilistic systems),以展示统一性。

问题
Timed transition systems 显式建模时间流逝,被用于进程演算和自动机语义,但缺乏统一的数学刻画来组织其行为等价。
方法
提出首个统一框架,在任意 timed transition system 推广上定义并比较 timed bisimulation、timed language equivalence 及其 weak 与 time-abstract 变体。
评估
通过理论证明表明这些等价按区分能力形成谱系且不依赖系统类型,并实例化到 timed transition systems 与 timed probabilistic systems。
原文摘要(Abstract)

Timed transition systems are behavioural models that include an explicit treatment of time flow and are used to formalise the semantics of several foundational process calculi and automata. Despite their relevance, a general mathematical characterisation of timed transition systems and their behavioural theory is still missing. We introduce the first uniform framework for timed behavioural models that encompasses known behavioural equivalences such as timed bisimulations, timed language equivalences as well as their weak and time-abstract counterparts. All these notions of equivalences are naturally organised by their discriminating power in a spectrum. We prove that this result does not depend on the type of the systems under scrutiny: it holds for any generalisation of timed transition system. We instantiate our framework to timed transition systems and their quantitative extensions such as timed probabilistic systems.

链接与引用

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

BibTeX
@article{paperbot823,
  title = {Behavioural equivalences for timed systems},
  author = {Tomasz Brengos and Marco Peressotti},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:17)2019}
}