一句话：为时间网络可达性提出局部时间语义下的抽象与包含检测，奠定偏序方法基础。
时间网络由多个时间自动机通过共同动作同步并行组合而成，其可达性分析面临交错爆炸问题。本文基于 Bengtsson 等人 1998 年提出的局部时间语义，为局部时间 zone 设计新的模拟抽象，并给出高效判定局部时间 zone 间包含关系的算法，以支撑偏序方法。作者进一步证明：在较温和条件下，任意时间网络都不存在有限的局部时间 zone 抽象；为此引入 bounded-spread 网络，其中各进程局部时间的发散程度有界。对于这类网络，论文证明可以同时使用包含检测与偏序方法进行可达性分析，从而为时间网络的偏序约简奠定基础。
A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods when solving the reachability problem for timed networks. It is based on a local-time semantics proposed by [Bengtsson et al. 1998]. A new simulation based abstraction of local-time zones is proposed. The main technical contribution is an efficient algorithm for testing subsumption between local-time zones with respect to this abstraction operator. The abstraction is not finite for all networks. It turns out that, under relatively mild conditions, there is no finite abstraction for local-time zones that works for arbitrary timed networks. To circumvent this problem, we introduce a notion of a bounded-spread network. The spread of a network is a parameter that says how far the local times of individual processes need to diverge. For bounded-spread networks, we show that it is possible to use subsumption and partial-order methods at the same time.
@inproceedings{0001HSW22,
title = {Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods},
author = {R. Govind and Frédéric Herbreteau and Srivathsan and Igor Walukiewicz},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533343}
}