Page 5 - 《软件学报》2026年第1期
P. 5

2                                                          软件学报  2026  年第  37  卷第  1  期


                 模块配合局部操作来完成所有信息的传递和处理. 该方法指出了一条形式化研究异步系统的途径, 即如今为人所
                 熟知的   Petri 网模型. Petri 网是一种图形化数学工具, 原始       Petri 网的描述非常简单: 一个带权重的有向二分图, 其
                 中的两类节点分别是库所         (place) 和变迁  (transition), 库所和变迁之间的有向弧标示了有限个令牌          (token) 迁移规
                 则. 任何时刻各库所的令牌数称为该时刻下              Petri 网的标识  (marking). 遵循迁移规则的标识变化体现了对应           Petri
                 网上计算的运行过程. 这一简单的模型可以用于刻画和研究各种类型数据的信息处理系统. 由于其形式简洁且建
                 模能力强大, 除了作为描述和分析并发与分布式系统的工具以外                     [2,3] , Petri 网理论还被广泛移植到生物、商务、化
                 学、过程建模、软件设计、人工智能等多个领域中                  [4−10] .
                    同样是出于研究并行程序与计算的目的, Karp             等人  [11] 于  1969  年提出了向量加法系统   (vector addition system,
                 VAS) 这一概念, 并随后被     Hopcroft 与  Pansiot 扩展成为带状态的向量加法系统       (vector addition system with states,
                 VASS) [12] . 尽管  Petri 网和  VASS  分别倾向于对实际问题的建模工作与对并行程序的形式化分析, 二者却是完全等
                 价的. 两者的转换也是直接的: 用         VASS  中的向量来表示     Petri 网中的库所集合, 用向量的加法来表示          Petri 网上的
                 变迁. 这种等价性使得实践中与          Petri 网相关的诸多问题最终都可归约为           VASS  模型上的验证问题. 相对于        Petri
                 网的图形化描述而言, VASS       模型在数学上更加简洁, 这在简化问题分析难度的同时也赋予了                      VASS  重要的理论
                 和应用价值. 为此本文将聚焦于讨论向量加法系统上的验证问题, 特别是其中可达性问题的下界.
                    对给定的模型, 形式化验证是要考察该模型是否满足某个或某些给定的性质. 一方面, 在形式化验证中, 常见
                 的验证问题包括: 系统的正确性、安全性和可靠性等. 另一方面, 前面提到, Petri 网被广泛地应用在多个领域的建
                 模中. 从而对领域中具体对象上的具体问题就可以用                 Petri 网上的相应算法和结论. VASS      是对  Petri 网模型的进一
                 步数学抽象. VASS    模型最主要的验证问题如下.
                    ● 可达性问题    (reachability): 判定给定的初始格局和目标格局之间是否存在可达的路径.
                    ● 有界性问题    (boundedness): 给定初始格局, 判定其可达的格局集合是否是有限的.
                    ● 可覆盖性问题     (coverability): 给定初始格局和目标格局, 判定是否能够从初始格局迁移到某个比目标格局大
                 的格局.
                    以上  3  个验证问题本身蕴含了很多具体、现实的算法问题. 比如通信系统的安全性可以归约到回答从初始格
                 局出发能否到达某个“不安全”格局, 即可达性问题; 再比如计算系统的正确性, 可以归约到该系统能否达到或超越
                 某些目标值, 其本质就是可覆盖性问题.
                    针对上述问题的算法复杂性研究主要涵盖如下两方面内容: 其一是上界研究, 即找到尽可能快的验证算法; 其
                 二是下界研究, 即讨论该问题至少需要多少时间资源. 可达性、有界性和可覆盖性这                           3  个问题间亦存在深刻的内
                 在联系. 事实上, 有界性问题和可覆盖性问题都可以被有效归约到可达性问题. 换言之, 从计算复杂性的角度, 可达
                 性问题是相关验证问题中最困难、最有挑战性的. 就研究历史而言, 早在                      20  世纪  70  年代, 有界性问题与可覆盖性
                 问题就被证明是      EXPSPACE-完备的    [13] , 但关于可达性问题的复杂性刻画却一度停滞了             40  余年, 直到在  2021  年
                 IEEE Symposium on Foundations of Computer Science (FOCS) 会议上, 来自华沙大学的  Czerwiński [14] 和波尔多大学
                 的  Leroux [15] 两个研究团队才各自独立证明了一般        VASS  模型的可达性问题是       Ackermann-完备的. 即便如此, 人
                 们对固定维度下的       VASS  以及关于维度的参数复杂性依然缺乏清晰的认识. 需要强调的是, 由于现实建模使用的
                 VASS  其维度往往是由具体应用所决定的, 是一个固定参数, 因此固定维加法向量模型在应用上有重要价值, 其精
                 确的下界研究是相关形式化建模的理论基础. 相应地, 固定维加法向量模型可达性问题的下界研究也是近年理论
                 计算机科学领域最活跃、最受关注的问题之一. 在国内, 上海交通大学的张文博等人                          [16] 和杨启哲  [17] 曾做过此方面
                 的调研, 但受当时领域内对该问题认识的限制, 在内容上前者主要围绕上界问题展开, 缺乏对下界的讨论, 后者虽
                 有对下界的基本讨论, 但未包含最新的、在固定维模型上的突破性研究.
                    历年来, 相关研究者们发展并建立了许多精妙的证明技术和归约技巧, 积累了丰富的研究成果. 但这些研究工
                 作往往比较分散, 缺乏对相关研究技术和思路的系统梳理和总结. 鉴于此, 本文对                       VASS  可达性问题复杂性下界的
                 关键证明技术进行一个全面的总结, 以期对后续研究有所启发. 特别地, 我们详细分析了若干核心技术之间的内在
                 逻辑, 据此将近    50  年的研究成果联为一体, 并进一步揭示了这些技术的本质优势和局限. 本文旨在从更高的角度
   1   2   3   4   5   6   7   8   9   10