时间飞镖：一种用于验证闭时间自动机的数据结构

用于模型检验时间系统的符号数据结构一直是重要研究课题，差分约束矩阵（DBM）仍然是多个成熟验证工具中首选的数据结构。相比之下，离散化提供了一种简单的替代方案，所有操作在时钟数量上具有线性时间复杂度，并且对于一大类闭系统有效。不幸的是，细粒度离散化本身会导致状态空间爆炸。我们引入了一种称为时间飞镖的新数据结构，用于时间自动机状态空间的符号表示。与完全离散化相比，单个时间飞镖可以表示任意大的状态集，而时间飞镖上的操作时间复杂度仍与时钟数量成线性关系。我们证明了所提出的可达性算法的正确性，并进行了多次实验以比较时间飞镖与完全离散化的性能。主要结论是，在所有实验中，时间飞镖方法均优于完全离散化，并且在具有较大常数的模型上扩展性显著更好。