实时系统验证：时间Petri网秒表状态空间计算的精确算法与实验对比

本文探讨了在实时系统形式化验证的背景下，如何精确地计算时间Petri网的状态空间，特别是在考虑秒表机制时。作者Morgan Magning、Didier Lem和Olivier Roux针对这类问题提出了一种算法，该算法旨在高效且准确地构建状态空间模型，通过使用边界矩阵（DBM）技术。DBM在处理时间Petri网，特别是那些包含简单时钟（如时间自动机）的网络时，提供了一种有效的方法，它们将连续的时间/秒表变化编码为一组线性不等式构成的凸多面体。 文章的主要贡献在于提出了一种策略，即在可能的情况下使用DBM来计算状态空间，这是一种相对低的时间和内存消耗方法。然而，当需要更全面的精确性时，会自动过渡到一般多面体计算。作者给出了一个必要条件，用于确定何时从DBM切换到一般多面体。这对于理解何时采取哪种方法来验证系统的行为至关重要，尤其是在多任务环境中，比如抢占式的系统建模，其中秒表变量的暂停和恢复特性需要得到精确处理。 值得注意的是，由于考虑了密集时间的语义，传统上时间Petri网的状态空间是无限的，因此验证过程通常需要对其进行抽象，保留关键属性。实验部分对比了作者的方法与完全DBM近似和精确计算的效果，重点展示了仅使用一般多面体的优势。 这篇文章在实时系统验证领域提供了重要的理论基础和技术手段，对于理解和优化状态空间分析，特别是在秒表计时复杂性下，具有显著的实际意义。关键词包括实时系统、时间Petri网、多面体以及DBM的应用，这表明了研究者们在探索更有效的方法来处理这类高度复杂的系统模型。