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

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

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

LIR-H-Safra tree圖示

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

L-game圖示

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

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

總結(jié)

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

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