报告名称：语言、LTL和自动机

报 告 人：王小兵 副教授

报告时间：2021年4月25日15：00

报告地点：B5-201

报告人介绍：

计算机学院计算机科学系主任。

中国计算机学会高级会员，中国自动化学会会员。

2000年、2003年与2009年分别于西安电子科技大学计算机学院获得工学学士、工学硕士与工学博士学位。

2003年起在西安电子科技大学计算机学院工作至今。

2014年12月至2015年12月在美国University of Texas at Dallas公派访问留学1年。

迄今主持国家自然科学基金面上项目2项，中央高校基本科研业务费资助项目3项，软件工程国家重点实验室开放基金1项。

在国内、国际刊物与学术会议上发表SCI/EI检索学术论文二十余篇。

报告简介：

基于时序逻辑的形式化方法建立在无穷串的自动机基础上，近20年来，在工业界软硬件的分析和验证上取得了很大成功。线性时序逻辑LTL在命题逻辑上引入Next和Until两个时序算子，具有简洁、直观的特点，同时有具有相对较强的表达能力，在验证领域被广泛使用。讲座介绍语言、LTL、自动机以及之间的联系，指出在实际应用中存在的一些问题。