第35届ACM/IEEE计算机科学逻辑研讨会（ACM/IEEE Symposium on Logic in Computer Science，http://lics.siglog.org/lics20/），简称LICS 2020，将于7月8日至7月11日在线举行（主会场位于德国萨尔布吕肯）。本次会议是理论计算机科学领域的顶级国际会议之一。它与STOC和FOCS齐名。它在计算机科学领域享有很高的声誉。其成果代表了理论计算机科学的前沿，具有广泛而深远的学术影响。

LICS对结果质量要求极高，论文接收难度大。它每年在全球范围内只接受50-60 篇论文。自1986年首次在剑桥大学举办以来，共有9篇国内单位署名论文在LICS上发表（含2020年）。今年国内只有西电的一篇论文被录用，题为Making Streett Defineization Tight，是迄今为止最好的一篇。这是LICS接收的第二篇由国内单位独立完成的论文，也是唯一一篇由国内单位独立完成的论文。该论文是与西安电子科技大学计算机科学与技术学院田聪教授、博士生王文胜、段振华教授合作完成。论文最终完美解决了从非确定性Street自动机（NSA）到拉宾自动机（DRA）的确定性问题，得到了从NSA到奇偶自动机（DPA）确定性的最佳算法和渐近紧界。这是理论计算机科学领域具有里程碑意义的研究成果。它是提高计算机软硬件系统可信验证时空效率的重要理论基础。也是SnS、CTL*、微积分等逻辑系统判断过程的基础。也是解决无限博弈的重要基础。问题的关键。

对无限字自动机复杂性的研究始于20 世纪60 年代。 1988年，Safra提出了Safra树，该树发表在FOCS 1988上，成为未来确定无限字自动机的核心数据结构。 Streett自动机确定性问题的研究始于1992年。28年来，从NSA到DRA，确定性问题的状态复杂度上下界大致匹配；从Street自动机到Parity的确定性问题的状态复杂度的上限和下限之间仍然存在很大差距。此次发表的论文通过引入新的节点命名规则，提出了一种新的数据结构H-Safra树。节点的名称仅由索引标签确定。即一旦节点的索引标签确定了，名称也就唯一确定了，避免了节点命名。影响状态复杂性，从而降低NSA 决定论的复杂性。在此基础上，提出了LIR-H-Safra树。通过引入LIR来记录H-Safra树中的节点生成顺序，降低了从NSA到DPTA的状态复杂度。

LIR-H-Safra 树图标

该论文进一步定义了完整的Streett 自动机及其匹配的L 博弈。通过定义L-game的不同动作，给出了从NSA到DRA的确定性状态复杂度的精确下界，与文中给出的算法复杂度（上限）完美匹配，从而结束了从NSA到DRA的复杂度问题。同时，本研究将确定性状态复杂度的下界从NSA改进为DPA，渐近匹配文中提出的算法复杂度（上限），并大大缩小了上下界之间的差距。

L 游戏图标

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

（来源：西电新闻网）