官方公众号

手机端

我室田聪教授团队科研成果在顶会LICS 2020发表

发布时间:2020-07-08 10:41:21 审核人: 点击:

第35届ACM/IEEE计算机科学逻辑国际会议(ACM/IEEE Symposium on Logic in Computer Science,http://lics.siglog.org/lics20/),简称LICS2020,将于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的状态复杂度。

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

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

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

上一篇:我室李云松教授团队参与我国首次火星探测任务
下一篇:我室李云松团队在CVPR2020两项比赛中获佳绩