时序逻辑的语法语义比较分析.pdf

《时序逻辑的语法语义比较分析.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、2014年9月重庆文理学院学报Sep.，2014第33卷第5期JournalofChongqingUniversityofArtsandSciencesVol.33No.5时序逻辑的语法语义比较分析1，2，31，2，311黄羿，马新强，刘友缘，罗万成（1.重庆文理学院机器视觉与智能信息系统重点实验室，重庆永川402160；2.贵州大学计算机科学与技术学院，贵州贵阳550025；3.贵州科学院，贵州贵阳550001）［摘要］随着信息技术的快速发展，信息和通信技术（ICT）系统被广泛使用，因而其可靠性非常

2、重要.本文采用时序逻辑的形式化方法对ICT系统进行可靠性检测讨论，主要从3种时序逻辑的语法、语义及它们的异同进行比较分析，为ICT的可靠性检测分析提供了理论借鉴.［关键词］语法；语义；时序逻辑；可靠性［中图分类号］TP391［文献标志码］A［文章编号］1673-8004（2014）05-0116-05目前，人们对信息和通信技术（ICT）系统的的正确性，提出了Verilog程序的符号模型检测依赖在快速增长，这些系统正变得越来越复杂.方法.该方法依据形式化操作语义将Verilog程通过Internet和各

3、种嵌入式系统（如智能卡、掌上序建模为有限状态机，将设计规范用命题投影时电脑、移动电话）等大规模的应用，正迅速进入人序逻辑公式描述，并采用命题投影时序逻辑符号们的日常生活.人们对嵌入式系统的依赖使得这模型检测工具对程序进行验证，从而证明片上系［2］些系统的可靠运行变得非常重要.这些系统如果统满足设计规范.在运行过程中出现错误有时会带来金钱上的损通过模型检测技术验证系统的可靠性时，应失，有时甚至会带来灾难.因此，ICT系统的可靠将反应式系统的属性进行形式化描述，考虑到这性在系统设计中是一个关键问题，系统验

4、证技术类系统本身的特点，通常时序逻辑可作为这样的［3］适用于在更可靠的方式下设计ICT系统［1］.一个形式化描述语言.像在自然语言中的情形利用系统验证方式来构建或设计的软件应一样，形式语言也有语义、语法和实例.语义涉及具有某些特性，而要验证的特性可以是一些基本符号和符号表达式的涵义（当给符号以某种解释时）.语法涉及符号表达式的形式结构，不考虑任的属性，属性大多是从系统规范得到的.系统规何对形式语言的解释.形式语言的语义和语法既范描述了系统要做的和不做的，从而构成任何验［4］有联系，又有区分.在这里讨论

5、3种时序逻辑，证活动的基础.一旦系统不满足某个规范的属性分别是线性时序逻辑（LTL）、计算树逻辑则一个缺陷被发现了.一旦系统满足所有的属性（CTL）、时序逻辑与行为逻辑的结合（TLA）.就被认为是正确的.在本文中讨论被称为模型检测的验证技术.在这方面也有相关研究，例如：为1LTL的语法与语义了保证以Verilog硬件描述语言设计的片上系统LTL即线性时序逻辑，用于对计算进行推［收稿日期］2014-05-29［基金项目］重庆市前沿与基础研究项目（CSTC2013JCYJA40053）；重庆市教委科学技术

6、研究项目（KJ131218、KJ111217、KJ1401112）；永川区自然科学基金（重点）项目（YCSTC2013NB8001，YCSTC2013AD2002）.［作者简介］黄羿（1976-），女，重庆人，贵州大学博士研究生，副教授，主要从事逻辑程序、人工智能方面的研究.116j理.虽然没有明说，但隐含了整个系统是按着一σ

7、＝FΦiffj≥0.σ

8、＝Φj个路径向前发展演化的，就像一个只有一个线索σ

9、＝GΦiffj≥0.σ

10、＝Φj的故事一样.σ

11、＝ΦWΨiffj≥0.σ

12、＝Φ1.1LTL的语法

13、或jk定义1令p是原子命题，LTL中的公式由j≥［（0σ

14、＝Ψ）∧（0≤k﹤j，σ

15、＝Φ）］j有限次使用以下规则（1）~（5）形成：σ

16、＝ΦRΨiffj≥0［（σ

17、＝Ψ）∨（0k（1）p是公式.≤k﹤j，σ

18、＝Φ）］（2）如果Φ是公式，则劭Φ是公式.（3）如果Φ和Ψ是公式，则Φ∨Ψ是公式.（4）如果Φ是公式，则ΧΦ是公式.（5）如果Φ和Ψ是公式，则Φ∪Ψ是公式.在定义1中可看出，规则（1）、（2）、（3）与命题逻辑中公式的形成规则相同，但和命题逻辑公图1LTL实例式相比LTL公式引入了时序运算

19、符Χ和∪.1.3实例ΧΦ表示如果Φ在下个时刻成立，则ΧΦ在当前如图1所示的Kripke结构为：时刻成立.Φ∪Ψ表示在将来某个时刻Ψ成立，S＝｛i

20、1≤i≤4｝Φ在该时刻之前成立.I＝｛4｝1.2LTL的语义R＝｛（4，2），（1，2），（2，3），（3，1）｝作者使用Kripke结构这个概念来定义时序Labe（l1）＝｛p｝andLabe（l2）＝｛p｝and公式的含义.Labe（l3）＝｛p，q｝andLabe（l4）＝｛q｝定义2Kripke结构是一