分治归约合成及并行验证语言可分解性

   报告人简介：

   林立勇分别在2011年和2016年获得新加坡南洋理工大学一等荣誉学士学位和博士学位。2016年到2017年间林立勇作为NSERC博士后在加拿大多伦多大学开展研究工作。目前林立勇在新加坡南洋理工大学从事信息物理系统方面有关网络安全方向的博士后研究。林立勇的研究兴趣包括人工智能，形式化方法和监督控制理论。
内容摘要：

   自动计算复杂度理论中的归约有许多理论和实际上的应用，包括自动编程和或许能够帮助我们更深刻地了解复杂度理论中的一些悬而未解的问题。一种比较特殊的归约叫做分治归约， 即将一个大问题归约成多个同样结构的小问题。 分治归约有时能够极大地改进在一些特别情况下已知算法的复杂度。这份报告讨论的是目前对分治归约的一些理解，研究进展和它在一些有序结构的形式化验证问题上的应用。 一个比较具体的应用是语言可分解性的验证问题。语言可分解性是分布式监督控制理论中的一个重要的性质。这份报告将会简单介绍语言可分解性的概念和讨论如何自动合成分治归约来实现在一些特别情况下并行验证语言可分解性和降低验证复杂度。