摘要
近年来,时态逻辑大量应用于程序验证,采取的途径随使用的时态逻辑的形式和方法的不同而异。本文用自动机理论研究几种时态逻辑(LTL,BTL,POTL)的模型和模型生成子,并讨论用时态逻辑进行程序验证的的重要途径。
During recent years, temporal logics have been widely applied in progran verifications. The approachcs they adopt vary with different forms and methods of the temporal logic used. In this paper, we examine the models and model generators of sercral temporal logics by using automata theory. We also discuss the main approchcs for program verifications using temporal logics.
出处
《计算机工程与科学》
CSCD
1992年第4期18-28,共11页
Computer Engineering & Science
关键词
时态逻辑
程序验证
模型
生成子
temporal logic, program verification, model, generator.
