2016年1月5日晚七点，科学前沿进展名家系列讲座I第30讲在中国科学院大学玉泉路校区礼堂举行。本次讲座的主讲人是中国科学院软件研究所的林惠民院士。他向同学们介绍了软件方面的模型检验的知识。
首先林惠民院士向大家解释了这场讲座题目“模型检验与博弈”中“博弈”的确切含义。通俗地讲，就是我们日常生活中说到的游戏（game）。然后他谈到了模型检验与模型检验中的并发系统这些概念，并用一些生活中的例子进行了一番阐述。其实，就如同现今已经很常见的网购，就涉及到了很多这方面的内容。在提到模型检验的重要性时，林惠民院士举出了中国甬温线动车事故的例子，使同学们认识到了模型检验方面的疏忽引起的后果。
接下来，林惠民院士引入了状态机这一概念，并详细介绍了状态机中的一种——图灵机。其实，图灵机是由有穷状态机和无穷长纸带组成，是一种用于计算的机械，但其更为抽象和复杂。在此期间，林惠民院士举出了“加1”函数的图灵机这一例子。
最后，林惠民院士的重点放在了介绍奇偶博弈上。因为μ-运算模型检验问题与奇偶博弈问题之间的等价性，奇偶博弈这样一个数学上的问题可以用来研究模型检验中的一些内容。林惠民院士详细介绍了奇偶博弈这个“游戏“的游戏规则以及游戏中可能出现的一些情况，并且给出了这个游戏的制胜策略——即游戏中奇偶双方要想取胜的方法。在此基础上，林惠民院士又引入了奇偶博弈中的“或闭偶区”和“与闭奇区”的概念，使同学们对这一问题的认识更加全面。
讲座在林惠民院士详细回答了同学们的提问后圆满结束。（文/段宏键 图/张帜 ）
主讲人简介：
林惠民，中国科学院软件研究所研究员。1947年11月13日生于福建福州。1982年毕业于福州大学计算机科学系。1986年获中国科学院软件研究所博士学位。1999年当选为中国科学院院士。长期从事并法理论、形式语义、形式化方法、模型检测研究。
延伸阅读：
“科学前沿进展名家系列讲座”创办于2014年9月，是中国科学院大学为本科生开设的必修课程，同时欢迎研究生和教职工参加，由中国科学院大学本科部主办，讲座召集人为高鸿钧院士。该课程按照数学、物理、化学、生物、材料、计算机六个专业，邀请相关科学领域的院士等知名专家开展专题讲座。通过讲述科学故事、介绍相关学科方向的科学前沿进展，让学生在本科阶段了解不同学科的科研方向和主要进展，拓宽学生的学术视野，为他们最终选择学科专业和专业方向提供更丰富的判断依据。
林惠民院士讲座
学生提问
