第35屆ACM/IEEE計算機科學邏輯研討會（ACM/IEEE Symposium on Logic in Computer Science，http://lics.siglog.org/lics20/），簡稱LICS 2020，將于7月8日至7月11日在線舉行（主會場位于德國薩爾布呂肯）。本次會議是理論計算機科學領域的頂級國際會議之一。它與STOC和FOCS齊名。它在計算機科學領域享有很高的聲譽。其成果代表了理論計算機科學的前沿，具有廣泛而深遠的學術影響。

LICS對結果質(zhì)量要求極高，論文接收難度大。它每年在全球范圍內(nèi)只接受50-60 篇論文。自1986年首次在劍橋大學舉辦以來，共有9篇國內(nèi)單位署名論文在LICS上發(fā)表（含2020年）。今年國內(nèi)只有西電的一篇論文被錄用，題為Making Streett Defineization Tight，是迄今為止最好的一篇。這是LICS接收的第二篇由國內(nèi)單位獨立完成的論文，也是唯一一篇由國內(nèi)單位獨立完成的論文。該論文是與西安電子科技大學計算機科學與技術學院田聰教授、博士生王文勝、段振華教授合作完成。論文最終完美解決了從非確定性Street自動機（NSA）到拉賓自動機（DRA）的確定性問題，得到了從NSA到奇偶自動機（DPA）確定性的最佳算法和漸近緊界。這是理論計算機科學領域具有里程碑意義的研究成果。它是提高計算機軟硬件系統(tǒng)可信驗證時空效率的重要理論基礎。也是SnS、CTL*、微積分等邏輯系統(tǒng)判斷過程的基礎。也是解決無限博弈的重要基礎。問題的關鍵。

對無限字自動機復雜性的研究始于20 世紀60 年代。 1988年，Safra提出了Safra樹，該樹發(fā)表在FOCS 1988上，成為未來確定無限字自動機的核心數(shù)據(jù)結構。 Streett自動機確定性問題的研究始于1992年。28年來，從NSA到DRA，確定性問題的狀態(tài)復雜度上下界大致匹配；從Street自動機到Parity的確定性問題的狀態(tài)復雜度的上限和下限之間仍然存在很大差距。此次發(fā)表的論文通過引入新的節(jié)點命名規(guī)則，提出了一種新的數(shù)據(jù)結構H-Safra樹。節(jié)點的名稱僅由索引標簽確定。即一旦節(jié)點的索引標簽確定了，名稱也就唯一確定了，避免了節(jié)點命名。影響狀態(tài)復雜性，從而降低NSA 決定論的復雜性。在此基礎上，提出了LIR-H-Safra樹。通過引入LIR來記錄H-Safra樹中的節(jié)點生成順序，降低了從NSA到DPTA的狀態(tài)復雜度。

LIR-H-Safra 樹圖標

該論文進一步定義了完整的Streett 自動機及其匹配的L 博弈。通過定義L-game的不同動作，給出了從NSA到DRA的確定性狀態(tài)復雜度的精確下界，與文中給出的算法復雜度（上限）完美匹配，從而結束了從NSA到DRA的復雜度問題。同時，本研究將確定性狀態(tài)復雜度的下界從NSA改進為DPA，漸近匹配文中提出的算法復雜度（上限），并大大縮小了上下界之間的差距。

L 游戲圖標

該論文的發(fā)表是國際學術界對學校在理論計算機科學領域研究成果的認可，是學校長期支持基礎研究的成果。據(jù)悉，田聰和段振華教授團隊長期致力于計算機科學領域的基礎研究，解決了理論計算機科學領域的許多重要問題。團隊堅持理論創(chuàng)新與成果轉化相結合，堅持創(chuàng)新引領與服務國家需求并重。在理論研究的基礎上，提出高效的軟硬件系統(tǒng)驗證技術，開發(fā)了軟件可信性保證工具集MSV，包括20多個子工具和FPGA設計、開發(fā)和驗證軟件XD-V2B，已成功應用于重大領域探月工程三期工程等國家項目。

（來源：西電新聞網(wǎng)）