(通訊員 王文勝)第35屆ACM/IEEE計算機科學邏輯國際會議(ACM/IEEE Symposium on Logic in Computer Science,http://lics.siglog.org/lics20/)，簡稱LICS 2020，于7月08日—7月11日在線舉行(主會場設(shè)在德國薩爾布呂肯)。該會議是理論計算機科學領(lǐng)域最頂級的國際會議之一，與STOC、FOCS齊名，在計算機科學領(lǐng)域享有崇高的聲譽，成果代表著理論計算機科學的前沿，具有廣泛而深遠的學術(shù)影響力。

LICS對成果質(zhì)量要求極高，論文接收難度大，全球每年僅接收50-60篇論文。自1986年在劍橋大學首次舉辦以來，共計9篇論文簽署國內(nèi)第一單位在LICS發(fā)表(含2020年)，本年度國內(nèi)僅有西電1篇論文被錄用，題為Making StreettDeterminization Tight，是迄今為止LICS接收的第2篇由國內(nèi)單位獨立完成的論文，唯一一篇由國內(nèi)1家單位獨立完成的論文。該論文由計算機科學與技術(shù)學院田聰教授、博士生王文勝、段振華教授合作完成。論文完美終結(jié)了非確定Streett自動機(簡稱NSA)到Rabin自動機(簡稱DRA)的確定化問題，并且得到了NSA到Parity自動機(DPA)確定化目前最好的算法和漸近緊界。這是理論計算機科學領(lǐng)域里程碑性的研究成果，是計算機軟硬件系統(tǒng)可信性驗證時空效率提升的重要理論依據(jù)，是SnS、μ演算、CTL*等邏輯系統(tǒng)可判定性問題研究的基礎(chǔ)，更是解決無限博弈求解問題的關(guān)鍵。

無窮字自動機復雜性問題研究始于上世紀六十年代，1988年Safra提出Safra tree，發(fā)表于FOCS 1988，成為日后無窮字自動機確定化的核心數(shù)據(jù)結(jié)構(gòu)。針對Streett自動機確定化問題研究始于1992年。28年來，NSA到DRA的確定化問題狀態(tài)復雜度的上下界近似匹配；Streett自動機到Parity的確定化問題的狀態(tài)復雜度上下界之間仍有很大的鴻溝。本次發(fā)表的論文通過引入新的節(jié)點命名機制，提出了新的數(shù)據(jù)結(jié)構(gòu)H-Safra trees，節(jié)點的名字僅由索引標簽決定，即一旦節(jié)點的索引標簽確定，名字也唯一確定，避免了節(jié)點命名對狀態(tài)復雜度的影響，從而降低了NSA確定化的復雜度。在此基礎(chǔ)上，提出了LIR-H-Safra trees，通過引入LIR記錄H-Safra tree中節(jié)點生成順序，降低了NSA到DPTA的狀態(tài)復雜度。

LIR-H-Safra tree圖示

論文進一步定義了全Streett自動機，以及與其匹配的L-game。通過定義L-game的不同動作，給出了精確的NSA到DRA確定化狀態(tài)復雜度下界，與文中算法復雜度上界完美契合，從而終結(jié)了NSA到DRA的復雜度問題。同時,該項研究提高了NSA到DPA確定化的狀態(tài)復雜度的下界，與文中的算法復雜度上界漸近匹配，大幅縮小了上下界之間的鴻溝。

L-game圖示

該論文的發(fā)表，是國際學術(shù)界對學校在理論計算機科學領(lǐng)域研究成果的認可，體現(xiàn)了學校長期對基礎(chǔ)研究的支持。據(jù)悉，田聰、段振華教授團隊長期堅持計算機科學領(lǐng)域基礎(chǔ)研究，解決了多個理論計算機科學領(lǐng)域的重要問題。團隊堅持理論創(chuàng)新與成果轉(zhuǎn)化落地相結(jié)合，堅持創(chuàng)新引領(lǐng)與服務(wù)國家需求兩手抓，在理論研究的基礎(chǔ)上，提出了高效的軟硬件系統(tǒng)驗證技術(shù)，開發(fā)了軟件可信性保障工具集MSV，包括20多個子工具，和FPGA設(shè)計開發(fā)及驗證軟件XD-V2B，已在探月工程三期等國家重大工程等中得到應(yīng)用推廣。

論文詳情請參考視頻講解：https://www.youtube.com/watch?v=xQCVWzKgz3E&feature=youtu.be

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。