(通讯员 王文胜)第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 StreettDeterminization Tight,是迄今为止LICS接收的第2篇由国内单位独立完成的论文,唯一一篇由国内1家单位独立完成的论文。该论文由0638太阳集团官网田聪教授、博士生王文胜、段振华教授合作完成。论文完美终结了非确定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