一句话:首次提出统一的 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 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.