（通讯员 王文胜）第35届acm/ieee计算机科学逻辑国际会议(acm/ieee symposium on logic in computer science,)，简称lics 2020，于7月08日—7月11日在线举行（主会场设在德国萨尔布吕肯）。该会议是理论计算机科学领域最顶级的国际会议之一，与stoc、focs齐名，在计算机科学领域享有崇高的声誉，成果代表着理论计算机科学的前沿，具有广泛而深远的学术影响力。

lics对成果质量要求极高，论文接收难度大，全球每年仅接收50-60篇论文。自1986年在剑桥大学首次举办以来，共计9篇论文签署国内第一单位在lics发表（含2020年），本年度国内仅有西电1篇论文被录用，题为making streettdeterminization tight，是迄今为止lics接收的第2篇由国内单位独立完成的论文，唯一一篇由国内1家单位独立完成的论文。该论文由计算机科学与技术学院田聪教授、博士生王文胜、段振华教授合作完成。论文完美终结了非确定streett自动机（简称nsa）到rabin自动机（简称dra）的确定化问题，并且得到了nsa到parity自动机（dpa）确定化目前最好的算法和渐近紧界。这是理论计算机科学领域里程碑性的研究成果，是计算机软硬件系统可信性验证时空效率提升的重要理论依据，是sns、μ演算、ctl*等逻辑系统可判定性问题研究的基础，更是解决无限博弈求解问题的关键。

无穷字自动机复杂性问题研究始于上世纪六十年代，1988年safra提出safra tree，发表于focs 1988，成为日后无穷字自动机确定化的核心数据结构。针对streett自动机确定化问题研究始于1992年。28年来，nsa到dra的确定化问题状态复杂度的上下界近似匹配；streett自动机到parity的确定化问题的状态复杂度上下界之间仍有很大的鸿沟。本次发表的论文通过引入新的节点命名机制，提出了新的数据结构h-safra trees，节点的名字仅由索引标签决定，即一旦节点的索引标签确定，名字也唯一确定，避免了节点命名对状态复杂度的影响，从而降低了nsa确定化的复杂度。在此基础上，提出了lir-h-safra trees，通过引入lir记录h-safra tree中节点生成顺序，降低了nsa到dpta的状态复杂度。

lir-h-safra tree图示

论文进一步定义了全streett自动机，以及与其匹配的l-game。通过定义l-game的不同动作，给出了精确的nsa到dra确定化状态复杂度下界，与文中算法复杂度上界完美契合，从而终结了nsa到dra的复杂度问题。同时,该项研究提高了nsa到dpa确定化的状态复杂度的下界，与文中的算法复杂度上界渐近匹配，大幅缩小了上下界之间的鸿沟。

l-game图示

该论文的发表，是国际学术界对学校在理论计算机科学领域研究成果的认可，体现了学校长期对基础研究的支持。据悉，田聪、段振华教授团队长期坚持计算机科学领域基础研究，解决了多个理论计算机科学领域的重要问题。团队坚持理论创新与成果转化落地相结合，坚持创新引领与服务国家需求两手抓，在理论研究的基础上，提出了高效的软硬件系统验证技术，开发了软件可信性保障工具集msv，包括20多个子工具，和fpga设计开发及验证软件xd-v2b，已在探月工程三期等国家重大工程等中得到应用推广。

论文详情请参考视频讲解：https://www.youtube.com/watch?v=xqcvwzkgz3e&feature=youtu.be