基于可能性测度的计算树逻辑

首先,提出了可能的Kripke结构的定义,建立了可能的Kripke结构的可能性测度空间,并分析了可能的Kripke结构的一系列性质,即任一路径转移的可能性可由其初始状态的可能性分布与各转移的可能性取下确界而得到;依据可能的Kripke结构所定义的可能性测度具有其合理性等等。其次,给出了可能性计算树逻辑(PoCTL)的概念,讨论了两个PoCTL状态公式以及PoCTL与经典计算树逻辑(CTL)公式的等价性。最后,证明了PoCTL公式有与CTL*公式中"一致性"相对应的公式。     

基于可能性测度的工程管理决策的研究

考虑可能性Kripke结构的一种扩展形式——带有成本的可能性Kripke结构,并且研究在此之上的期望测度和多属性决策问题。带有成本的可能性Kripke结构是在可能性Kripke结构的转移关系上(或者是状态上)给定了成本——这个自然数可以看成是成本,当然也可以看成是收益。在此只考虑转移关系上的成本。为了便于理解,文中给出实例,即应用带有成本的可能性Kripke结构的相关理论来解决工程管理决策的某些问题。     

基于Kripke结构的程序正确性证明

为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。     

单道批处理系统的建模与验证

单道批处理系统的模型是其性能评价、仿真、作业调度及控制的研究基础。建立了单道批处理系统的一个数学模型—批处理自动机,并给出了相应的转换算法,将所建数学模型转换成Kripke结构;完成了基于Kripke结构的单道批处理系统模型检测,验证了单道批处理系统的合理性即兼顾公平性与效率。     

基于模糊逻辑的几类Kripke结构之间的关系

根据初始状态、状态之间的转换关系和命题赋值函数是否为分明的,模糊Kripke结构可分为8类。提出将模糊计算树逻辑作为判断模糊Kripke结构之间是否是等价的依据;详细讨论了8种模糊Kripke结构之间的关系。这些结论为设计应用中模型的合理选取提供了理论依据,也为解决模糊计算树逻辑的模型检测问题提供了一种新的方法。     

基于抽象和组合方法的网络协议验证

由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

具有公平性约束的CTL部分状态空间模型检测

检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术，部分Kripke 结构是描述部分状态空间的形式框架。文章主要讨论一类具有公平性约束条件的CTL（计算树逻辑）模型检测问题。定义了部分公平Kripke结构和公平序，分别来表征部分公平状态空间和它们之间的序关系。并给出相应的3值CTL语意和相关定理来说明部分状态空间模型检测技术同样适用于具有公平性约束条件的CTL模型检测问题。     

基于余归纳的最小Kripke结构的求解

状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K）,在互模拟等价意义下K中最小Kripke结构（记为K₀）的存在唯一性.K₀描述了K中所有Kripke结构的行为而且没有冗余的状态;（2） 对于任意的M∈K（M可能包含无穷多个状态）,在互模拟等价意义下的相对于（M且基于K₀）的最小Kripke结构（记为K_M）的存在唯一性.由此提出一种求解K_M的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的K_M代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.     

A new model for model checking: cycle-weighted Kripke structure

This paper proposes a new model, named cycle-weighted Kripke structure (CWKS), based on the traditional Kripke structure. It adds two integer weights to some transitions of the Kripke structure, restricting when these transitions can occur. These weights mainly specify the occurrences of some cycles in a Kripke structure, giving a range of how many times these cycles may be executed repeatedly. This new model can efficiently describe some quantitative discrete-time characters of reactive and concurrent systems, so it is significant for some model checking problems. We also define a subset of CWKS, named conditional CWKS, which satisfies a constraint referring to the weighted transitions in the structure. The paper modifies the explicit computation tree logic (CTL) model checking algorithm to accommodate the conditional CWKS. It can also be regarded as the foundation of some more complex models obtained by extending from the Kripke structure, which will be studied in the future.     

基于控制流信息的克里普克结构生成方法

恶意程序检测是信息安全技术研究的重要内容,基于程序行为特征的检测可以弥补二进制特征码检测方法的很多不足。使用模型检验技术可以对程序的操作行为做属性验证,它需要对目标程序进行建模,得到一个符合克里普克结构的迁移系统。通过对模型检验技术和克里普克结构的研究分析,提出了一种以完整控制流信息为基础、采用贪婪归一策略的克里普克迁移系统生成方法。测试分析表明,利用该方法生成的迁移系统可以完整地描述控制流信息,也可以精确地刻画系统状态的改变。     

Possibilistic mean-variance models and efficient frontiers for portfolio selection problem

In this paper, it is assumed that the rates of return on assets can be expressed by possibility distributions rather than probability distributions. We propose two kinds of portfolio selection models based on lower and upper possibilistic means and possibilistic variances, respectively, and introduce the notions of lower and upper possibilistic efficient portfolios. We also present an algorithm which can derive the explicit expression of the possibilistic efficient frontier for the possibilistic mean-variance portfolio selection problem dealing with lower bounds on asset holdings.     

Knowledge structure approach to verification of authentication protocols

~~Knowledge structure approach to verification of authentication protocols1. Hintikka, J., Knowledge and Belief, Ithaca, NY. Cornell University Press, 1962. 2. Fagin, R., Halpern, J., Moses, Y. et al.,Reasoning About Knowledge, Cambridge, MA. MIT Press, 1995. 3. Halpern, I., Zuck, L., A little knowledge goes a long way. Simple knowledge based derivations and correctness proofs for a family of protocols. Journal of the ACM, 1992, 39(3): 449-478. 4. Stulp, F., Verbrugge, …     

Possibilistic support vector machines

We propose new support vector machines (SVMs) that incorporate the geometric distribution of an input data set by associating each data point with a possibilistic membership, which measures the relative strength of the self class membership. By using a possibilistic distance measure based on the possibilistic membership, we reformulate conventional SVMs in three ways. The proposed methods are shown to have better classification performance than conventional SVMs in various tests.     

模态转移系统的三值逻辑模型检验

分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题.提出了把模态转移系统转换成Kripke结构的算法以及三值逻辑公式转换成2个二值逻辑的算法,经过转换后可用现有的模型检验技术进行模型检验.用该算法转换后,状态数、转移数和原子命题数目与原模型呈线性关系,没有增加模型检验的复杂度.     

A fuzzy portfolio selection method based on possibilistic mean and variance

This paper deals with the portfolio selection problem when the returns of assets obey LR-type possibility distributions and there exist the limits on holdings. A new possibilistic mean–variance model to portfolio selection is proposed based on the definitions of the possibilistic return and possibilistic risk, which can better integrate an uncertain decision environment with vagueness and ambiguity. This possibilistic mean–variance model can be regarded as extensions of conventional probabilistic mean–variance methodology and previous possibilistic approaches since it contains less parameter and has a more extensive application. A numerical example of a possibilistic fuzzy portfolio selection problem is given to illustrate our proposed effective means and approaches. This project was supported by NCET (No.06-0749) and The National Natural Science Foundation of China (No.70571024).     

A portfolio selection model with borrowing constraint based on possibility theory

Compared with the conventional probabilistic mean-variance methodology, fuzzy number can better describe an uncertain environment with vagueness and ambiguity. In this paper, the portfolio selection model with borrowing constraint is proposed by means of possibilistic mean, possibilistic variance, and possibilistic covariance under the assumption that the returns of assets are fuzzy numbers. And a quadratic programming model with inequality constraints is presented when the returns of assets are trapezoid fuzzy numbers. Furthermore, Lemke algorithm is utilized to solve the model. Finally, a numerical example of the portfolio selection problem is given to illustrate our proposed effective means and variances. The results of the numerical example also show that the investor can make different decisions according to different requirements for the values of expected returns. And the efficient portfolio frontier of the model with borrowing constraints can be easily obtained.