时态逻辑与并发程序

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

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

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

检验实时系统的有序时段性质

模型检验是一种被广泛应用于对设计或系统正确性进行自动验证的技术。实时系统的性质包括瞬间性质和时段性质，显然后的检验要比前复杂得多。介绍了一类新的时段性质——有序时段性质，并检验了时间正则表达式的有序时段性质，最后分析了算法的复杂度，和相关工作进行了比较，并探讨了今后的工作方向。     

时态逻辑的比较与分析

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

Reduction and Simplification of Explicit LTL Model Checking via an Abstraction Method

An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period.This reduces the cost during the abstraction period relative to models requiring many useless states.A dining-philosophers example comparing this abstraction method with conventional methods indicates that a large proportion of the state space has been reduced by this abstraction method.Finally,the abstract method is shown to be correct and an analysis is given to show how such a large proportion of states can be reduced.     

程序条件化用于软件模型检测中的状态空间缩减

针对软件模型检测中的状态爆炸问题，提出将程序条件化技术用于软件状态空间缩减的方案．以程序性质的线性时序逻辑公式可能出现的蕴涵式的前件作为条件化的约束条件，通过分析程序符号化执行语义，借助自动定理证明器，对语句的可达性条件进行逻辑推理，删除那些与性质的可满足性无关的语句，以达到程序精简的目的．理论分析和实验结果表明，条件化可以有效缩减程序状态空间，而且缩减后的程序模型保留了原程序中与所需验证的性质有关的所有信息，满足软件模型检测对状态缩减的安全性要求．     

多智能体协同的认知规范模型检测算法

 在Wooldridge提出的利用不变式特征的方法来模型检测时态认知逻辑的基础上,研究多智能体协同逻辑ATEL(Alternating Temporal Epistemic Logic)中认知算子的模型检测算法,包括多层的认知算子,分布式认知算子和公共知识算子等等。研究结果表明,加入认知算子后的ATEL的在增加系统描述能力的同时并没有明显增加其计算复杂性。     

扩展Tempura语言统一模型检测算法

针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序...     

基于CTL的并发系统CSP模型验证

主要通过指称语义和回答集程序(Answer Set Programming,简称ASP)完成迹模型的生成,并构建了一套基于计算树逻辑(computing tree logic,简称CTL)的CSP模型验证方法.实验表明,该方法对于分支类型的性质具有较好的描述能力,且保证了验证的正确性.     

时序Rough逻辑及其在数据分析中的应用

提出一种时序Rough逻辑,定义了时序算子及其作用于Rough逻辑公式上的意义．描述了这种逻辑的语法和语义．论述了时序Rough逻辑中的语义模型是一个无限状态序列,其中每一状态都描述了当前时刻和场景点上信息系统的信息．从当前状态到下一状态的变换是遵循时序Rough逻辑演算的,它必须保持知识不变,也就是属性和讨论的对象不变,而属性关于对象的特征值,即属性值随着时间和场景变化而可以变化．因此。在信息系统上作决策、数据约简和信息粒化等都将产生影响,由此可见时序Rough逻辑将是动态地处理信息系统的理论工具,也将是合理地解决和处理不一致信息表的较好方法．     

基于时序逻辑语言XYZ/E的实时系统应用研究

针对实时系统在计算机系统应用中的重要性,采用形式化方法是保证实时系统软件开发正确性的一种重要途径,而时序逻辑这种形式化方法是研究实时系统的一个重要的理论基础。本文给出了时序逻辑语言XYZ/E的相关介绍,并利用XYZ/E的子语言XYZ/RBE与XYZ图描述了煤气炉实时控制问题。     

模型检测研究进展

阐述模型检测的基本思想和工作方式,介绍二叉决策图、符号模型检测、偏序规约等几种在模型检测中抑制状态爆炸的优化技术,并分析模型检测在应用上的优势,最后展望模型检测今后的研究热点.     

基于子结构逻辑的不确定性语义时态查询技术研究

为解决不确定性语义时态查询及其计算资源配置的优化问题,使用子结构逻辑对时态演算机制进行了完善并构建了查询中间件原型. 基于构造性逻辑语义,构建了中间件演算流程,将时态属性映射为类型语义,使针对时间属性的运算从句法演算中剥离,在保证表达能力的前提下,仅进行语义计算,加速并优化了查询演算流程.实验结果表明:该方法与中间件原型可行、高效,具有共性,为时态信息处理提供理论与技术支撑.     

模 糊 择 优 逻 辑 的 数 值 扩 充

提出一种新的模糊逻辑数值模糊择优逻辑, 给出了数值模糊择优逻辑的语法和语义, 并研究了其性质. 该逻辑结合多值逻辑和择优推理的语义特点, 得到的推理关系具有模糊性、 次协调性和非单调性, 且知识的模糊性能以数值的形式显式地表现, 适用于对智能系统中的不精确、 不一致和不完备知识进行表示和推理.     

基于模型检测的实时模型诊断方法

提出一种基于模型检测的实时模型诊断方法. 利用 模型检测算法对大状态空间系统验证的高效性, 使诊断系统能够更快地进行模型诊断, 并对这种方法进行了系统实现, 结果表明, 此方法可行、 有效.     

一种解决次协调数据库中无限关系的方法

次协调数据库的数据模型是用来处理数据库中两类不确定信息,即不完全信息和不一致信息(矛盾信息).次协调关系模型上的代数运算是普通关系上的代数运算的扩展,但由于次协调关系的特殊性,在其上的代数运算会产生无限关系,因此,以次协调关系为基础的DBMS必须能够表示和操纵无限关系.首先介绍了无限关系以及几种常见的解决方法,然后提出了一种新的元组扩展的方法以避免无限关系的出现,从而为次协调数据库的应用打下坚实的基础.     

面向投影时序逻辑的Web服务模型检测

为了满足Web服务的可靠性.利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模.用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定M和非P的合取的不可满足性,亦利用M和非P的正则形可构造合取式的正则图,判定合取的不可满足性,从而达到模型检测的目的.通过运行实例表明,所提模型检测器可验证Web服务系统性质,保证Web服务的可靠性.     

CAPM模型应用于房地产股票市场的有效性检验

CAPM模型普遍应用于中国房地产行业资本成本估算,投资风险评价和房地产泡沫等研究中。但是目前并没有文献对该模型在中国市场使用是否有效进行检验。本文选择了沪深A股房地产市场的33只股票,对CAPM模型在中国房地产股票市场的有效性进行检验。通过理论和实证研究,得出CAPM模型应用于房地产市场是无效的结论,即在中国房地产股票市场上不能直接应用CAPM模型,而应当根据中国房地产市场的实际条件做出相应的改进。     

基于FSA的模型检测算法研究

自动机就是描述系统行为的模型,通过它可以检测出系统实际工作时发生的状态,经过反复测试,诊断,以达到理想的模型。在基于自动机的模型检测中,前提是需要把非确定性FSA转化为确定性FSA,本文给出了非确定性自动机转换为确定性自动机的算法,最后分析该算法。     

基于时序的不同事物同属性的关联规则挖掘

基于时序的关联规则挖掘算法的研究一直都是人们关注的课题,提出了一种基于时序逻辑的不同事物同属性的关联规则挖掘。传统的关联规则主要是揭示了多个事物的同一属性在相同的时间点上的相互关联性,这样的关联规则的项与项之间没有体现时间上的差别,也就无法对时间序列的发展趋势进行预测。实验表明这种方法对于不同事物同属性预测具有现实意义。