封闭与开放时间网络的安全性质验证：决定性与不可判定性

本文主要探讨了时间网络参数化系统的安全性质验证问题，特别是在理论计算机科学的背景下。时间网络（TN）是一种参数化系统，由一个有限状态控制器和一组可变数量的定时进程构成，每个定时进程在有限实值时钟上运行。这些时钟的存在使得TN的行为特性超越了传统的有限状态自动机模型。 在之前的研究中，[3]表明，在每个定时进程仅配有一个实值时钟的情况下，检查控制器状态的可达性问题是可判定的。然而，当每个定时进程至少有两个时钟时，这一判定性结果不再成立，这一发现揭示了复杂性界限的变化。 本文将焦点转向了两种特定的时间网络子类：封闭时间和开放时间网络。封闭时间网络的特点是所有时钟约束是非严格的，这意味着时钟之间的比较关系不涉及严格等于。相反，开放时间网络则具有严格的时钟约束，相当于移除了相等测试的语法。文章的核心贡献在于证明了封闭时间网络的安全性质验证问题是可判定的，而开放时间网络的验证问题则变得不可判定。 此外，文章还探讨了在引入“定时模糊”概念的强语义定时网络中，即使在鲁棒语义下，无论是封闭还是开放的时间网络，其安全性质验证问题都保持为不可判定。这进一步强调了时间网络参数化系统在复杂性和语义上的挑战。 本文不仅扩展了对时间网络模型检测的理解，还揭示了随着系统复杂性的增加，验证问题的决定性特征如何发生变化，并且在处理模糊性和参数化时钟约束时遇到了理论上的限制。这对于理论研究者和实际应用中的系统设计者来说，提供了关于如何有效处理这类复杂系统的重要洞见。