We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if at least one process is in a given location. This computational model has been considered in the literature before, and example applications are gossiping clock synchronization protocols or planning problems. We address the minimum-time reachability problem (minreach) in DTNs, and show how to efficiently solve it based on a novel zone-graph algorithm. We further show that solving minreach allows us to construct a summary TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff-system required by existing results. Our techniques are also implemented, and experiments show their practicality.

翻译：我们引入了用于参数化验证离散时间网络（DTNs）的新技术。DTN是一类通过位置守卫进行通信的计时自动机（TAs）网络，只有当至少一个进程处于给定位置时，位置守卫才会启用某个转换。该计算模型在以往文献中已有研究，典型应用包括八卦时钟同步协议或规划问题。我们研究了DTN中的最小时间可达性问题（minreach），并展示了如何基于一种新颖的区域图算法高效求解该问题。进一步地，我们证明求解minreach能够构建一个摘要TA，该摘要TA精确捕捉任意规模DTN中单个TA的可能行为。这两个结果相结合，实现了DTN的参数化验证，同时避免了现有结果所需的指数级规模截止系统的构造。我们的技术已付诸实现，实验表明其具有实用性。