时态逻辑与并发程序

分别阐述了基于Ｍａｎｎａ－Ｐｎｕｅｌｉ框架的命题线性时态逻辑ＰＬＴＬ和基于共享变量方式的并发程序（转换图）模型,并给出该模型与转换系统之间的对应关系;将时态逻辑与公平转移系统ＦＴＳ相结合来描述并发程序及其性质（公平性、安全性及活性）;指出了时态逻辑具备其它形式化方法（ＦＳＭ、Ｐｅｔｒｉ网）所没有的一些优势。     

并发系统性质验证的一种形式化方法

采用Ｍａｎｎａ和Ｐｎｕｅｌｉ提出的命题线性时态罗辑ＰＬＴＬ作为并发系统的形式化规约语言、用ＰＬＴＬ公式描述系统的性质,给出并发系统性质验证的一种模型检验算法。     

一个面向对象的实体—联系—时间模型

讨论了一种应用于时态数据库的数据模型－面向对象的实体－联系－时间（ＥＲＴ）模型，将时态概念作为模型组成部件，重点描述了其模型结构和重要的时态概念，简要介绍了相应的时态关系代数操作及在此基础上约束。     

反应式系统的并发模型（Ⅳ）——时态逻辑模型

基于文（１￣３）,提出反应式系统并发描述的时态逻辑模型,并给出抽象计算模型的时态语义。     

并发系统性质描述的一种形式化方法

给出并系统性质的一种形式化描述方法－时态逻辑方法，其时间模型是离散和和线性的。     

模糊交互时态逻辑及其语义结构

Alur等人建立的交互时态逻辑（ATL ＊）是一种重要的多Agent合作逻辑,它对计算树逻辑（CTL ＊）进行了合作算子拓展,然而它缺乏对不确定时态信息的刻画。通过考察模糊时态事件和模糊时态状态、描述相对时间来改进并发博弈结构,并给出模糊并发博弈结构;把模糊并发博弈结构的若干要件从相对时间域到绝对时间域进行映射,给出已映射模糊并发博弈结构;建立了模糊交互时态逻辑（FATL ＊）,给出其语法,在已映射模糊并发博弈结构下给出其语义;阐述了FATL ＊的表达力比ATL ＊强。     

时态逻辑的比较与分析

对时态逻辑的两种重要形式－线性时态逻辑与分支时态逻辑进行了比较和分析,指出它们各自的特点及适用范围。     

基于时间区间关系的时态模糊描述逻辑研究

针对传统的模糊描述逻辑对随时间变化的不精确知识缺乏表达能力,运用时态逻辑,结合模糊计算,提出了基于时间区间关系的时态模糊描述逻辑—TFDL(IntervalAllen).引入Allen区间关系用于表示时间区间关系,并给出了TFDL(IntervalAllen)的语法和语义.该逻辑形成的系统增强了不精确知识的时态关系的表达能力.     

基于OBDD时序电路设计的验证

依据有序二叉判定图（OBDD）和计算树逻辑（或称分支时态逻辑）CTL（Computational Tree Logic)的基本原理，分析了基于OBDD和CTL的验证数据电路设计的基本原理，并在此基础上，给出了时序电路等价验证的方法。     

地籍管理信息系统中宗地数据的时空组织与查询研究

时态信息是地理信息系统（GIS）中信息的重要一维，时态地理信息系统（TGIS）已成为当前国际GIS研究的热点。在地籍管理工作中，空间对象的历史状态和引起状态变化的相关事件等数据作为重要的存档资料都应当加以保存。在简要介绍了时态地理信息系统和时空数据模型之后，以地籍管理信息系统中的时态数据的管理来讨论适合实际地籍管理的宗地时空数据组织和查询。第一部分分析了宗地变更的基本类型，主要讨论了空间物体形态的变化，一般分为宗地合并、宗地分割和复杂变化。接着在第二部分则描述了宗地变化的时空拓扑关系－空间相关性（spatio-overlap）和时间相接性（time-meet）。第三部分在不改变原有的数据库的存储结构的条件下，运用基态修正法，通过定义时态对象来构造宗地数据时空模型，据此在宗地层区分现状层和历史层来对时态数据进行数据组织。在第四部分，根据宗地数据的时空变化类型和时空拓扑关系，设计了查询算法进行宗地空间数据的时态查询，并提供了查询算法的关键代码。最后，我们以某市旧城改造的实验数据进行了验证，实践表明运用该方法可以有效地对时态数据进行快照查询和任意宗地进行时态跟踪和搜索。     

一阶时态逻辑系统及其在程序中的一个应用

随着程序科学研究的不断深入,用于研究的工具也不断改进.从最初使用古典逻辑、普通的模态逻辑,直到现在已经有人使用了时态逻辑.各种新的时态算子的不断涌现,使得对每一种新开拓的时态逻辑系统都必须证明其完全性定理.此外,现今的时态逻辑主要还是“命题形式”的,怎样把它推广到一般的谓词形式的时态逻辑,也有必要进行研究.特别,以往在程序中使用时态逻辑的时候,仅仅是用时态逻辑来描述程序的一些性质,而没能把程序与时态逻辑放到一个公理化的形式系统里加以讨论. 在本文里,我们力图把已知的一类很大的逻辑,统一在一个称为一阶时态逻辑的公理系统里加以研究.在对这个谓词演算的一阶时态逻辑系统进行深入研究之后,我们就可     

纵向注入逻辑

描述一种新的注入逻辑，即纵向注入逻辑，在这种逻辑中，对器件的结构作了特殊的设计以取得高封装密度和低功耗－延时乘积，普通注入逻辑（Ｉ＾２Ｌ）的横向ＰＮＰ注入极被纵向结构所代替。对于在Ｉ＾２Ｌ中影响封装密度和功耗－延时乘积的因素进行了分析，并且给出了这种新结构的设计依据。     

N－100的结构模型

在对Ｎ－１００结构进行分析和表征的基础上，描述了Ｎ－１００的形成过程．通过建立结构模型．以高分辨核磁共振波谱（１Ｈ及定量（１３）ＣＮＭＲ）为定量依据，计算了异氰酸酯百分含量、平均官能度和平均相对分子质量．讨论了影响定量准确性的两个因素．对其中来自ＮＭＲ技术方面的主要因素──纵向弛豫时间做了对比．计算结果与实际测试值的一致性说明了结构模型是可行的．     

面向对象的概念建模

给出一种面向对象概念建模方法，它将图形表示、Ｅ－Ｒ方法、关系演算、时态逻辑溶为一体，支持对象结构、行为和对象演变建模的一体化和封装     

自动化仓库客户服务管理问题的时态逻辑描述

在扩展的时态逻辑框架下对自动化仓库中的客户服务管理问题进行研究，内容包括对此服务管理过程进行描述与分析，并给出了相应的控制策略，以使系统达到期望的动态行为．     

车载导航电子地图中道路数据的空间逻辑描述

道路数据是车载导航电子地图中主要研究的数据，也是智能化交通运输系统（ITS）建立数据框架的基础数据。据此彩地理信息系统（GIS）技术，从逻辑描述方案的角度探讨道路数据的空间逻辑描述、属性描述和速体逻辑关系，以提供恰当的道路逻辑描述方案来建立道路空间数据库，并为道路数据标准化采集提供依据。     

计算机网络通信协议的一种形式化描述技术

针对目前绝大多数形式化描述技术在处理协议的活性等方面存在的不足,提出一种新的基于公平性假设的时态逻辑技术描述协议,并给出ＡＢ协议的形式化描述实例。     

时态形式的“距离”含义

杰弗里·利奇和简·斯瓦特维克所著的《英语交际语法》[1]中非常明确地论述了时间与时态、体态之间的关系,即对态与体态表示由动词描述的动作和过去、现在或者将来时间的关系．由此,英语语法中对动词形式所表现的时态和体态紧密地和时间建立起联系．本文拟从“距离”（distace）这一新的视角,深入探讨动词时与体所描述的时间之外的含义．1动词形式中的时态与体态《英语交际语法》中是这样定义时态和体态的：“时（tense）与体（aspect）表示由动词描述的动作和过去、现在或将来时间（time）的关系．”在定义中,时间就象方程式中的参数,…     

铁路系统的模型检查和参数分析

研究铁路系统的自动验证技术，建立火车和控制器的混合自动机模型，用时态逻辑ＩＣＴＬ描述铁路系统的性质规范，使用模型检查技术自动验证铁路系统，并且对铁路系统的一些参数进行分析。     

基本的一阶时态逻辑的一个完备性定理

仅以基本公理作为逻辑公理的一阶时态逻辑的形式系统,称为基本的一阶时态逻辑的形式系统。基本的一阶时态逻辑有模态逻辑和时态逻辑的一个发展。本文的目的是:为基本的一阶时态逻辑建立一个完备性定理。