模型检测思想和方法的演进，本文主要内容关键词为：模型论文,思想论文,方法论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
[中图分类号]N031 [文献标识码]A [文章编号]1002-8862(2010)10-0094-05
自计算机出现以来，人们就开始寻找一种证明程序正确性的好方法。早期的程序员为验证程序的正确性，在实践中通常使用的方法是运行这一程序。然而，这种运行程序的测试方法虽然可以证明一段不正确的程序是不正确的，但无法证明一段正确的程序是正确的。因此，采用一种在数学上完备的形式验证方法，是构造可靠软件的一个重要途径。模型检测作为逻辑学和计算机科学的一个重要研究领域，正是目前非常流行的一种自动化形式验证方法，它的思想起源可以追溯到20世纪30年代数理逻辑学家对算法的探讨。作为计算机理论科学和数理逻辑中的最高奖图灵奖曾两度颁给对模型检测有重要贡献的三位科学家。一位是将时间逻辑用于计算机科学的皮纽利(A.Pnueli)，另外两位就是提出模型检测的克拉克(E.M.Clarke)和埃默森(E.A.Emerson)。模型检测的基本思想是：先将系统的性质用逻辑公式φ表示，再将系统抽象为一个克里普克(Kripke)结构M，从而将“系统是否具有所期望的性质”这一问题转化为“克里普克结构M是否是公式φ的模型”的问题。
在纯逻辑学界，人们追求的往往是框架层面上的逻辑；而在逻辑学与计算机科学的交界处，模型层面上的逻辑则受到更多的重视。从本质上讲，模型检测问题是一个证明“语言包含”的问题，即：模型M对应的“语言”是否包含在规格说明公式φ所对应的“语言”中。如果成立，则可断言系统M满足规格说明的要求；否则L(M)\L(φ)中的任意执行序列都对应一条违反规约的反例路径。换言之，模型检测是一种检测形式系统中的语形和语义是否密切联系的机制。虽然国外对模型检测的研究已经取得了不少成果，但国内的研究偏重于计算机应用方面，对这一思想和方法做出逻辑学与计算机科学的交叉学科研究还未见报道。本文从希尔伯特方案的失败谈起，由图灵机，丘奇(Church)序列演算，布奇(Büchi)自动机，霍尔(Hoare)逻辑，动态逻辑PDL，线性时间逻辑LTL和计算树逻辑CTL，一直谈到模型检测的正式提出及发展，考察这一重要理论的演进过程，探讨这一发展给我们带来的重要启示。
一 对判定性问题的关注
有人说计算机是数学家一次失败思考的产物，这个数学家大概指的是希尔伯特(D.Hilbert)。希尔伯特方案要解决的是数学的判定性问题。判定性问题是指一个能行过程的设计问题，即是否存在一个能行的过程，在有限的时间内能够告诉我们，某一任意给定的语句是否有效。
20世纪初，罗素悖论的提出撼动了整个数学大厦的根基。为了加固数学大厦的根基，20世纪20年代希尔伯特提出希尔伯特方案，试图证明数学的一致性和可判定性，从而把整个数学建立在一个牢固可靠的基础上。1928年，希尔伯特证明了一阶逻辑系统的一致性。受希尔伯特的影响，为了讨论是否对于每个问题都有解决它的算法，数理逻辑学家们开始提出各种计算模型，其中最著名的模型就是图灵在1936年提出的图灵机(Turing machine)。图灵机很好地将算法这一直观概念精确化，从而确立了算法理论。图灵机在当时已经具备了今天计算机的所有计算能力，以任何常规编程语言编写的计算机程序都可以翻译成一台图灵机，反之任何一台图灵机也都可以翻译成大部分编程语言程序。此外，图灵通过图灵机停机问题的不可判定性推出一阶逻辑的不可判定性，从而明确划分了可判定性和不可判定性的界线，即区分了计算机能做什么和不能做什么，揭示了计算模型的能力极限，完全摧毁了希尔伯特形式化数学的宏伟计划。图灵机因此被看做是现代计算机科学的理论基础。
虽然图灵对一阶逻辑的判定性问题给出了否定回答，但这一否定结果也为相应的肯定结果留下了空间。其实早在1915年洛温海姆(L.Lowenheim)就证明了带等词的单目一阶逻辑(记做
)具有可判定性；1919年斯科伦(T.Skolem)又证明了单目二阶逻辑(记做MSO)具有可判定性[1]。这两个结果曾一度在模型检测思想的发展过程中起到了引导作用。
1957年丘奇在一篇题为“递归算法在人工合成回路中的应用”(Application of Recursive Arithmetics to The Problem of Circuit Synthesis)的论文中定义了序列电路(sequential circuits)，将电路设计问题归结为的判定问题，这便是硬件模型检测思想的萌芽。丘奇在文中还提出一个重要的问题——判定问题，这正是今天所说的模型检测问题①。
丘奇的判定问题本质上是由布奇在1962年解决的。布奇证明了在字结构上的MSO公式的可满足性问题是可判定的，并且提出一个非确定型布奇自动机②A=(∑，S，
，ρ，F)，这正是软件模型检测思想的开始，布奇提出了著名的布奇定理③，即给定一个MSO语句φ，并根据φ构造一个自动机
，能够接受φ所描述的字符串当且仅当L()不为空。这一定理说的就是model(φ)=L()，即MSO与非确定型布奇自动机具有相同的表达能力，从而解决了丘奇的判定问题。
沿着图灵开辟的对判定性问题研究的道路前行，柯克(S.A.Cook)于1969年开启了计算复杂性研究，计算复杂性是评价一个算法优劣的重要指标。人们发现，在布奇定理中构造自动机的算法，其计算复杂度函数是非初等的，并且，在无限字上和MSO的判定问题的计算复杂度函数也是非初等的。其实模型检测思想后来的发展，就是一个不断寻找具有更好表达力和更高计算复杂度算法来解决丘奇判定问题的过程。
二 作为规格说明语言的动态逻辑
为验证程序的正确性，我们首先要考虑如何表达和描述程序。1967年弗洛伊德(R.W.Floyd)提出一种断言法技术来描述程序的意义。这种技术把一对公式放在相应程序段之前和之后，分别称为该程序段的前条件和后条件，如：pre P post，其意思是：如果在程序P执行之前条件pre成立(当时的环境满足pre)，那么当P的执行终止时条件post应该成立。也可以把这样的公式对(pre，post)看做是对一段程序的规格说明，通过逻辑推导就能证明程序的正确性。
霍尔(C.A.R.Hoare)于1969年总结了弗洛伊德的工作，提出基于上述断言法的程序验证系统霍尔逻辑。霍尔逻辑是一阶逻辑的扩充，它由一套推理规则组成，通过这些规则可以把证明一个霍尔公式的问题归结为证明一组普通一阶逻辑公式的问题。例如证明一个霍尔公式｛A｝α｛B｝，就是要证明当程序α开始执行时，如果一阶公式A为真，那么在α执行结束后，一阶公式B将为真。但由于在循环结构中存在着不可用霍尔逻辑描述的程序状态，因此霍尔逻辑在表达力上具有一定缺陷，无法描述程序的终止性，只能用于证明程序的部分正确性。
为克服霍尔逻辑的缺陷，普拉特(V.R.Pratt)在霍尔逻辑中引入程序模态词[π]。通过将霍尔公式｛A｝α｛B｝转换为模态公式A→[α]B，普拉特于1976年提出动态逻辑DL，克服了霍尔逻辑中的不可描述问题。1977年费希尔(M.J.Fischer)和拉德纳(R.E.Ladner)提出了DL的命题版本——命题动态逻辑PDL。④PDL属于多模态逻辑，对于传统的可终止性正规程序来说是表达力完全的。在PDL中有两类语形实体：公式和程序。公式是在原子命题上使用布尔联结词构造而成的，被解释在克里普克结构中的状态点上；程序是在原子程序上使用程序构造子“；”、“*”、“∪”和“？”等构造而成的，被解释为克里普克结构中的二元关系。在动态逻辑中，丘奇的判定问题从序列线路中转移到了程序中。用PDL对程序进行形式验证的过程需要对程序本身有一定的了解，其实这个过程就是对这个程序构造一个正确性规格说明。
三 作为规格说明语言的时间逻辑
普拉特设计的动态逻辑可以用来描述传统的可终止性正规程序，但对于并发(不可终止性)程序来说，这就显得不再适用了。1977年皮纽利在“时间逻辑纲要”(The Temporal Logic of Programs)一文中将带有U和X时间联结词的线性时间逻辑LTL引入计算机科学，用作并发程序规格说明语言，开启了时间逻辑应用于计算机科学的第一道闸门，被授予1996年的图灵奖。描述并发程序的困难在于并发程序的高度非确定性，并发程序的模型
//
//…//
，是由平行程序、、…、构成的，这种构造方式允许在每一个正在执行的序列程序中非确定地插入一个平行程序。与PDL相比，LTL在表达并发系统中的一些概念，如公平性(fairness)，活性(liveness)，无死锁(absence of deadlock)，互斥(mutual exclusion)时是相当理想的。
动态逻辑使用程序模态词描述计算，可以说是采用了一种外部视角，完全通过语形来刻画程序。而时间逻辑则采用一种内部视角，借助某种先在的程序结构(如线性结构或分支结构)，将程序执行计算的过程隐含在带有时间顺序的程序状态序列中，通过迹(而不是状态对)来解释程序，因此可被用于非终止性程序。此外，动态逻辑提供了程序推理中分支时间的方法。有鉴于此，兰波特(L.Lamport)开始研究线性时间逻辑和分支时间逻辑在表达力上的区别，并证明了每一种逻辑都具有表达另一种逻辑无法表达的性质之能力。本-艾利(M.Ben-Ari)，曼纳(Z.Manna)和皮纽利通过在不带U算子的LTL中引入存在和全称路径量词E和A，提出了分支时间逻辑UB⑤，使得可以量化系统将来的不同行为。后来，克拉克和埃默森又在UB中加入U算子，从而得到了计算树逻辑CTL⑥，后来又提出综合了LTL和CTL两者表达能力的分支时间逻辑CTL*⑦。
实际上，采用测试的方法来检测并发程序中的错误是非常困难的，因为这样的错误通常很难再次产生。皮纽利的工作使人们相信时间逻辑是并发程序规格说明的强有力工具，但在那个时代，证明一个程序满足它的规格说明的形式验证方法，是通过手动地为这个程序构造各种公理和规则，从而得到一个特殊的时间逻辑演绎系统，然后再证明程序的规格说明公式是这个演绎系统的定理。然而这种方法通常很繁琐，大量的精力被花费在如何组织证明过程上。模型检测理论的正式提出，使我们摆脱了这种低效的手工形式验证，也开启了时间逻辑应用于计算机科学的第二道闸门。
四 模型检测概念的正式提出及发展
1981年克拉克和埃默森在《运用分支时间的时间逻辑的同时性状态图的设计和综合》(Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic)中，通过搜索程序状态图中的每一个状态，来检测规格说明公式在这个模型上是否成立。这种自动化形式验证技术的采用标志着模型检测概念的正式提出。两位学者也因此被授予2007年的图灵奖。模型检测是计算机科学家给逻辑学家上的一堂非常重要的课，它告诉逻辑学家：适当的推理形式是多么的重要！计算机科学中所要求的“适当推理形式”不仅是形式化和系统化的，而且还必须是算法化和自动化的。
20世纪80年代中后期，模型检测方法按系统属性的表达方式分为两大类：一类是时间逻辑的模型检测，就是刚刚提到的最早的模型检测方法；另一类是自动机的模型检测，亦即将系统抽象成一个自动机，系统要满足的性质也被规约为一个自动机，通过比较这两台自动机所接受的语言来确定系统的行为是否满足规约的要求。而将这两类方法联系在一起的是维达(Vardi)和沃尔普(Wolper)，他们证明了怎样把标号传递系统映射为自动机，从而产生了两者之间的联系，他们的方法是目前模型检测中最流行的一种⑧：将抽象出的系统模型用布奇自动机A来表示，再将需要验证的系统性质用LTL公式φ来表示，然后将LTL公式φ取反后转化为另一台布奇自动机
，最后检查这两台布奇自动机接受语言集合之交是否为空。
不难看出，自动机方法确实为模型检测注入了新的活力。借助自动机方法对LTL公式进行模型检测能否被看做是对丘奇判定问题的满意的解决方案呢？可以这么说，但也不完全。根据著名的坎普(Kamp)定理(1968)，可以证明LTL的表达力等价于。的表达力不及MSO，又根据布奇定理可知LTL的表达力不及布奇自动机。然而一旦我们在标号转换系统中加入公平性，它就可被看做是自动机的变种。我们有理由要求规格说明语言能够刻画基本的程序结构，为此我们需要一种具有布奇自动机或MSO表达能力的程序规格说明语言。20世纪80年代发展各种扩展时间逻辑的主要目标就是为了达到布奇自动机或MSO表达能力。
可能有人会问，为什么不采用经典逻辑作为程序规格说明语言呢？这是因为模型检测者像模态逻辑学家一样更关注模型的局部性质，在各种时间逻辑的框架内看待这些局部可满足性问题更加清晰，而传统的经典逻辑更关注公式的全局性质。既然具有可判定性，为什么不将LTL转换为来得到它的判定过程？这样做当然可以，但是在LTL转换为经典逻辑后的判定过程中往往会涉及到非初等爆炸，这是我们不愿看到的。因此，沃尔普，西斯特拉(A.P.Sistla)和维达提出了避免非初等爆炸的方法，将LTL转换为布奇自动机。
20世纪80年代后涌现出一批具有布奇自动机或MSO表达能力的时间逻辑，其中最早、也最著名的一个成果就是沃尔普、西斯特拉和维达在1983年构造的三个扩展时间逻辑
，它们分别是在LTL中增加以环(looping)、有限(finite)和重复(repeating)为接收条件的自动机作为联结词的扩展的时间逻辑。另外还有通过增加MSO中的单目二阶量词得到的带量词的命题线性时间逻辑QPTL，通过增加最大点和最小点算子得到的带μ演算的命题线性时间逻辑μLTL，以及结合动态逻辑和时间逻辑这两种方法，通过增加带索引的U算子而得到的动态线性时间逻辑DLTL等。除此之外，为满足不同的应用需求，模型检测从理论到应用的各个层面上还采用了许多不同的研究工具，如进程逻辑(PL)，区间时间逻辑(ITL)、交互式时间逻辑(ATL)、混合时间逻辑(HTL)、公制时间逻辑(MTL)、μ演算(MC)、共代数、二叉树图、Petri网等，以及使用它们的各种方法，如表列、归结、博弈和以伪代码表示的各种程序算法等，从而使得这一领域看起来相当纷繁复杂。随着模型检测理论的成熟，工业界也相继出现了多个模型检测软件和具有工业标准的规格说明语言，如基于CTL的IBM Sugar，基于LTL的Intel For-Spec，基于CTL*的IEEE 1850标准PSL等。
回顾这些思想和方法的演进，不难看出它们之间有着令人惊奇的一脉相承的联系。在见证了模型检测由一个简单思想到一个研究领域、由学术界辐射到工业界并创造了商业价值的奇迹之后，笔者想说的是：一方面，模型检测软件和具有工业标准的时间逻辑不过是将基础研究成果变成大众便于使用的工具，但是正是这种技术研发和应用推动了理论和方法的发展演进。尽管技术研发总是要落后于基础研究，但也并不是说所有的理论方法都会变成大众工具，工业界认为有助于解决实际问题的方法，才会把它变为工具。当一个计算模型被刚刚设计出来时，人们还不清楚它的计算复杂度以及在应用它时会遇到的问题，在这样一个不断演进的过程中，一些思想和方法或者被遗忘或者被再次想起，而研发和应用在其中起到了推进器的作用。因此，我们认为，基础研究不能被削弱，但基础研究成果的意义最后还是要工业界说话，要实践来说话。另一方面，国外对模型检测的研究到了20世纪90年代后才趋于成熟，目前我国计算机科学界对模型检测的研究已经蓬勃兴起，而我国逻辑学界对时间逻辑和模型检测的研究还比较薄弱，没有能够为计算机领域中的后继研究提供充分适当的原料。随着模态逻辑被越来越多的人视为研究框架的一般工具，它的发展前景也逐渐显现出来，同时计算机科学也为模态逻辑的发展加大了马力，指引了方向。虽然笔者还不太清楚用于模型检测的时间逻辑将会为模态逻辑将来的发展带来什么，但有一点可以肯定：“今后的模态逻辑学家们会越来越像‘逻辑工程师’，他们会为适应某些特殊的应用而把逻辑工艺化。”⑨模型检测正是时间逻辑被工艺化的一个实例。
注释：
①M.Y.Vardi,From Church and Prior to Psl,2007,Available at http://www.cs.rice.edu/~vardi/papers/index.html.
②J.R.Büchi,"Weak Second-order Arithmetic and Finite Automata",Z.Math Logik Grundlag,Math.6,1960,pp.66-92.
③J.R.Büchi," On a Decision Method in Restricted Second-order Arithmetic",Proc.Internat.Cong.on Logic,Methodology,and Philosophy of Science 1960,Stanford University Press,1962,pp.1-12.
④M.J.Fischer,R.E.Ladner,"Propositional Dynamic Logic of Programs",Journal of Computer and System Sciences,1979,18(2):pp.194-211.
⑤M.Ben-Ari,Z.Manna,A.Pnueli,"The Logic of Nexttime",In Proc.8th ACM Symp.On Principles of Programming Languages,1981,pp.164-176.
⑥E.M.Clarke,E.A.Emerson,"Design and Synthesis of synchronization Skeletons Using Branching Time Temporal Logic",Logic of Programs:Workshop,Yorktoen Heights,LNCS,NY:Springer,1981,131:pp.52-71.
⑦E.A.Emerson,J.Y.Halpern," Sometimes and Not Never Revisited:On Branching Versus Linear Time",In Proc.10th ACM Symp,On Principles of Programming Languages,1983,pp.127-140.
⑧A.P.Sistla,E.M.Clarke," The Complexity of Propositional Linear Temporal Logic",Journal of the ACM,1985,32:pp.733-749.E.A.Emerson,J.Y.Halpern,"Decision Procedures and Expressiveness in the Temporal Logic of Branching Time",Journal of Computer and Systems Science,1985,30:pp.1-24.M.Y.Vardi,P.Wolper,"Anautomata-theoretic Approach to Automatic Program Verification",Proc.1st IEEE Symp.On Logic in Computer Science,1986,pp.332-344.
⑨刘新文、余俊伟：《摹略万物之然，论求群言之比——模态逻辑新观念述评》，《哲学动态》2005年第12期。