(通訊員 王文勝)第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家單位獨立完成的論文。該論文由計算機科學與技術學院田聰教授、博士生王文勝、段振華教授合作完成。論文完美終結了非確定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

總結

以上是生活随笔為你收集整理的计算机科学中的研究成果,田聪教授团队科研成果在计算机科学顶会LICS 2020发表...的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。