黄 羿，马新强，刘友缘，罗万成

(1.重庆文理学院机器视觉与智能信息系统重点实验室，重庆 永川 402160;

2.贵州大学计算机科学与技术学院，贵州 贵阳 550025;3.贵州科学院，贵州 贵阳 550001)

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

黄 羿1，2，3，马新强1，2，3，刘友缘1，罗万成1

(1.重庆文理学院机器视觉与智能信息系统重点实验室，重庆 永川 402160;

2.贵州大学计算机科学与技术学院，贵州 贵阳 550025;3.贵州科学院，贵州 贵阳 550001)

随着信息技术的快速发展，信息和通信技术(ICT)系统被广泛使用，因而其可靠性非常重要.本文采用时序逻辑的形式化方法对ICT系统进行可靠性检测讨论，主要从3种时序逻辑的语法、语义及它们的异同进行比较分析，为ICT的可靠性检测分析提供了理论借鉴.

语法;语义;时序逻辑;可靠性

目前，人们对信息和通信技术(ICT)系统的依赖在快速增长，这些系统正变得越来越复杂.通过Internet和各种嵌入式系统(如智能卡、掌上电脑、移动电话)等大规模的应用，正迅速进入人们的日常生活.人们对嵌入式系统的依赖使得这些系统的可靠运行变得非常重要.这些系统如果在运行过程中出现错误有时会带来金钱上的损失，有时甚至会带来灾难.因此，ICT系统的可靠性在系统设计中是一个关键问题，系统验证技术适用于在更可靠的方式下设计ICT系统［1］.

利用系统验证方式来构建或设计的软件应具有某些特性，而要验证的特性可以是一些基本的属性，属性大多是从系统规范得到的.系统规范描述了系统要做……