行为时序逻辑与自反线性时序逻辑的关系  

Relationship Between Temporal Logic of Actions and Linear Tense Logic with Reflexive Property

作　　者：白金山[1] 冯天亮[1] 吴应江[1] 丘文峰[1] 王梦[1] 

机构地区：[1]广东医学院信息工程学院,东莞523808

出　　处：《现代计算机（中旬刊）》2014年第1期3-7,共5页Modern Computer

基　　金：广东医学院博士启动基金(No.B2011006)

摘　　要：为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中,对行为时序逻辑公式的语义进行形式化定义,从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系,提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念,定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统,以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。To define the semantics of Temporal Logic of Actions （TLA） formulas so that philosophical logic axiom system can be used for the re- search on TLA. Investigates the relations between TLA and linear tense logic with reflexive property in semantics and syntax. Presents and proves transforming LTL system to TLA system using reflective properties. Proves the TLA system logic rule is proved by LTL axiom system. Defines the notion of item and atomic formula in the temporal logic of action through the idea of set theory and model theory. On this basis, defines the semantic of the temporal logic of action and proves that the axiom system of reflexive linear temporal logic is suitable for the axiom system of the temporal logic of action. Proves the simple rules, basic rules and additional rules of the temporal logic of action.

关 键 词：模型检测 行为时序逻辑 语义 语法 自反性 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]