由西安电子科技大学计算机科学与技术学院田聪教授、博士生王文胜、段振华教授合作完成的论文在第35届ACM/IEEE计算机科学逻辑国际会议上发表。

　　第35届ACM/IEEE计算机科学逻辑国际会议（ACM/IEEE Symposium on Logic in Computer Science,http：//lics.siglog.org/lics20/），简称LICS 2020，将于7月08日—7月11日在线举行（主会场设在德国萨尔布吕肯）。该会议是理论计算机科学领域最顶级的国际会议之一，与STOC、FOCS齐名，在计算机科学领域享有崇高的声誉，成果代表着理论计算机科学的前沿，具有广泛而深远的学术影响力。

　　LICS对成果质量要求极高，论文接收难度大，全球每年仅接收50-60篇论文。自1986年在剑桥大学首次举办以来，共计9篇论文签署国内第一单位在LICS发表（含2020年），本年度国内仅有西电1篇论文被录用，题为Making Streett Determinization 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图示

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

L-game图示

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