5月20日上午，印度清奈數理科學研究所R.Ramanujam教授應計算機科學國家重點實驗室邀請到軟件所進行學術交流，并作題為Automata for counting data, and some logic的學術報告，法國洛林信息學與應用研究所的Hans van Ditmarsch教授、北京大學哲學系王彥晶副教授一同參加交流。報告會由楊紹發副研究員主持。

對計算機程序、并發系統以及數據庫系統中的無窮數據進行驗證和推理是形式驗證領域一個很有挑戰性的問題。近年來提出的無窮字母表上的自動機模型為研究具有無窮數據的系統的行為提供了理論模型，但無窮數據也意味著形式模型的判定問題的高復雜度：具有較弱表達能力的模型就有可能導致相關的判定問題具有很高復雜度。

R.Ramanujam教授介紹了他們團隊最近提出的一種對數據串中的數據進行計數的自動機模型，并且證明了其非空性問題是初等可判定的（EXPSPACE完全）。他同時討論了數據串上的一些相關邏輯系統的可滿足性問題的結果。R.Ramanujam教授還簡要介紹了印度在理論計算機科學和形式化方法領域的主要研究機構，并且與大家就如何促進中國與印度在理論計算機科學與形式化方法方面的合作進行了廣泛深入的討論。

R.Ramanujam是印度清奈數理科學研究所邏輯與自動機理論領域教授，研究方向為數理邏輯、哲學邏輯以及它們在計算機科學中分布式系統理論、安全協議驗證、博弈論等的應用。他與Rohit Parikh共同為時態認知邏輯在計算機科學中的應用作過開創性貢獻。R.Ramanujam教授是國際符號邏輯學會（ASL）的理事，《ACM Transactions on Computational Logic》等重要國際期刊的編輯。

R.Ramanujam教授作報告