报告名称：语言、LTL和自动机
报 告 人：王小兵 副教授
报告时间：2021年4月25日15：00
报告地点：B5-201
报告人介绍：
计算机学院计算机科学系主任。
中国计算机学会高级会员，中国自动化学会会员。
2000年、2003年与2009年分别于必威BETWAY官网计算机学院获得工学学士、工学硕士与工学博士学位。
2003年起在必威BETWAY官网计算机学院工作至今。
2014年12月至2015年12月在美国University of Texas at Dallas公派访问留学1年。
迄今主持国家自然科学基金面上项目2项，中央高校基本科研业务费资助项目3项，软件工程国家重点实验室开放基金1项。
在国内、国际刊物与学术会议上发表SCI/EI检索学术论文二十余篇。
报告简介：
基于时序逻辑的形式化方法建立在无穷串的自动机基础上，近20年来，在工业界软硬件的分析和验证上取得了很大成功。线性时序逻辑LTL在命题逻辑上引入Next和Until两个时序算子，具有简洁、直观的特点，同时有具有相对较强的表达能力，在验证领域被广泛使用。讲座介绍语言、LTL、自动机以及之间的联系，指出在实际应用中存在的一些问题。
