A survey on temporal logics for specifying and verifying real-time systems  

作　　者：Savas KONUR 

机构地区：[1]Department of Computer Science, the University of Liverpool, Liverpool L69 3BX, UK

出　　处：《Frontiers of Computer Science》2013年第3期370-403,共34页中国计算机科学前沿（英文版）

摘　　要：Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.

关 键 词：propositional temporal logics first-order linear temporal logics branching temporal logics interval temporal logics real-time temporal logics probabilistic temporal logics DECIDABILITY model checking EXPRESSIVENESS 

分 类 号：TP332[自动化与计算机技术—计算机系统结构] TP316.2[自动化与计算机技术—计算机科学与技术]