【本站讯】近日，上海交通大学傅育熙教授做客黄岛论坛，作题为“可达性问题、算法与复杂性”的线下学术报告。

傅育熙就计算机可达性问题进行简要阐述，说明可达性问题可以理解成一个系统从其中一个状态经过一定次数的变迁后是否可以改变成另一个目标状态。报告从可达性问题的基本概念、研究历史、可判定性以及算法复杂性等几个方面进行介绍，并指出可达性问题在系统的安全性验证、程序分析等方面都有很好的应用。

傅育熙介绍可达性问题的分析模型——带状态的向量加法系统VASS（Vector Addition Systems with States）。VASS能够对系统的状态变化进行描述，通过使用一组多维的向量来表示系统状态，在相同维度的迁移规则上进行向量的加减法操作来控制系统状态的变化。傅育熙解释道，VASS和不带状态的向量加法系统VAS（Vector Addition Systems）模型被证明是等价的。他通过一个简单的图形化例子，分别对VASS中的规则、参数、状态进行详细的阐述。

傅育熙在讲述VASS的可达性问题的可判定性验证时指出，n维VASS可以用n+3维VAS来表达，因此两者的可达性问题等价，所以可选择其中一种进行可达性问题的研究。根据VASS可达性问题的研究历史来看，VASS上的可覆盖性问题（coverability）已经被证明是ExpSpace-hardness问题，而判定VASS可达性问题的算法难度从2-VASSes的PSpace-complete到特定维度VASS的Tower-hardness甚至是Ackermann-hardness。其次，针对VASS可达性的判定算法复杂性验证问题，傅育熙教授介绍了其证明思想：由于计算机系统中的参数都是非负的，因此，将初始状态和终止状态都向上抬升以保证初始状态和终止状态之间的路径在第一象限内，同时，还需要保持抬升后的路径和原路径一致。

傅育熙在介绍VASS可达性问题判定算法的复杂性时指出，算法的复杂性分析需要对算法的下界和上界进行证明。在证明VASS可达性问题的EXPSPACE算法下界时，他给出归约的思想，通过将该算法归约到一个已经可以计算其复杂性的问题上来确定其复杂性的下界。而对于上界问题，给出了KLMST分解算法，该算法会维护一个标记证据图序列（marked witness graph sequence）集，对其中不满足完美条件的标记证据图作分解。如果分解结束时集合不为空，则原可达性问题是可达的；否则不可达。总的来说，此方法可以归纳为分解-降维-分解-降维的持续化过程。

最后，傅育熙给同学们提出了一些宝贵的建议。第一是对线性代数的掌握，只有掌握了线性代数才能让我们的研究向更多维度的空间中拓展；第二是对几何直觉的培养，几何直觉往往决定着工科生对图形的理解和分析能力；第三是对数形结合的理解，将数与形结合起来进行分析、研究、解决问题，是研究中必须具备的科研能力。

报告结束后，傅育熙就有关学术问题与现场师生进行了热烈讨论，并就可判定性、算法复杂度分析等方面的提问又作了详细解答。

傅育熙，1992年获英国曼彻斯特大学计算机博士学位，1994年起在上海交通大学计算机系任职，现为上海交通大学特聘教授，国家杰出青年基金获得者、上海市优秀学科带头人。曾任上海交通大学软件学院院长、上海高校软件理论研究中心主任、上海市计算机学会理事长、国务院学位委员会第六届学科评议组成员、教育部计算机类专业教学指导委员会副主任。研究领域为理论计算机科学，研究内容涉及程序理论、并发理论、等价性验证、可达性理论、交互理论。担任Mathematical Structures in Computer Science编委，讲授的“计算复杂性理论”课程获评“2019年度高校计算机专业优秀教师奖励计划”。