5月20日上午，印度清奈数理科学研究所R.Ramanujam教授等应计算机科学国家重点实验室邀请到澳门赌场软件研究所进行学术交流，并作题为Automata for counting data, and some logic的学术报告。报告会由杨绍发副研究员主持。

对计算机程序、并发系统以及数据库系统中的无穷数据进行验证和推理是形式验证领域一个很有挑战性的问题。近年来提出的无穷字母表上的自动机模型为研究具有无穷数据的系统的行为提供了理论模型，但无穷数据也意味着形式模型的判定问题的高复杂度：具有较弱表达能力的模型就有可能导致相关的判定问题具有很高复杂度。

R.Ramanujam教授介绍了他们团队最近提出的一种对数据串中的数据进行计数的自动机模型，并且证明了其非空性问题是初等可判定的（EXPSPACE完全）。他同时讨论了数据串上的一些相关逻辑系统的可满足性问题的结果。R.Ramanujam教授还简要介绍了印度在理论计算机科学和形式化方法领域的主要研究机构，并且与大家就如何促进中国与印度在理论计算机科学与形式化方法方面的合作进行了广泛深入的讨论。

R.Ramanujam是印度清奈数理科学研究所逻辑与自动机理论领域教授，研究方向为数理逻辑、哲学逻辑以及它们在计算机科学中分布式系统理论、安全协议验证、博弈论等的应用。他与Rohit Parikh共同为时态认知逻辑在计算机科学中的应用做出过开创性贡献。R.Ramanujam教授是国际符号逻辑学会（ASL）的理事，ACM Transactions on Computational Logic等重要国际期刊的编辑。

R.Ramanujam教授作报告