一个关于通信顺序进程语言的公理系统

通信的顺序进程语言是对分布式系统进行程序设计的一种语言。本文介绍了迹、断言迹集合、断言迹集合的核以及进程迹集合等概念。进程被看成是断言迹集合的一种特例——进程迹集合。采用的断言语言是断言迹集合。在此基础上,文章提出了一个以归纳式为形式的公理系统。利用这个公理系统可以对通信顺序进程语言所写的程序进行部分正确性的证明。     

π-演算中无卫递归的消除

本文提出消除π－演算中无卫递归的公理，证明了将该公理加入到正则π－演算受卫递归子集上的证明系统后，所得到的证明系统在π－演算全体正则子集上关于互模拟等价的可靠性和完备性.     

不一致本体精确调试的公理分割方法

本体调试是解决本体不一致问题的主要手段。现有的本体调试方法能够求解出本体不一致性的一组冲突公理集合,删除这些公理可使本体恢复到一致状态。然而,简单地删除这些冲突公理不可避免地会造成本体信息的损失。为了解决这个问题,采用公理分割的思想,对冲突公理集合进行分割,基于分割后的公理集再次进行调试。该方法能够保留与不一致性无关的本体信息,从而避免了信息损失的情况发生。实验结果表明,在各种类型的实验本体上,所提出的精确调试算法在留存度与调试时间两方面都比类似相关的算法取得较好的效果。     

基于推理信息的本体模块化方法

本体模块化在本体推理和复用等应用中有着极为重要的作用.怎么样将本体划分成小的模块是最基本的问题,目前本体模块化的工作主要集中在本体复用的目的上.在这篇文章中,我们提出了一种基于推理信息的本体模块化方法,该方法以提高推理的性能为目的.在基于同一最小推理集合内的公理之间内聚性将会增强的合理假设下,我们的模块化方法通过分析每次推理的过程,得到推理的最小推理集合,然后增强最小推理集合内公理1之间的内聚度,最后根据内聚度将本体划分成模块.在评估阶段,我们首先使用训练公理划分本体,然后通过测试公理来调查本体推理性能提高的程度.根据训练公理和测试公理所属范围的不同,我们使用了三组实验:训练公理和测试公理限定在同一较小范围,训练公理和测试公理不限定范围,训练公理和测试公理的范围实现三次不同的改变.实验的结果尤其是符合实际应用情况的实验三的结果证明了基于推理信息的本体模块化方法的有效性.     

基于代数规格说明的OOP测试用例生成算法研究

现阶段面向对象软件系统占据了很大的比重,在软件测试方面,形式化规格说明通常作为正确性验证的基础.本文主要研究了基于程序的代数规格化说明生成测试用例的方法.首先,根据代数规格化说明得到一组基本项.为了避免从理想基本项集合中选择一组基本项时受理想基本项集合的制约,本文用基本项模型图生成基本项,然后,从基本项集合中得到等价的范式集合.针对用范式模型树生成范式时,生成的不完全是范式,并且范式的长度可能无穷大的问题,本文提出对基本项模型图路径拆分的方法.最后,用范式替换规格化说明公理系统中的变量,生成测试用例.对于公理中的条件语句和循环语句,还提出一种公理变换方法,保证了测试路径的覆盖.实例分析和实验验证表明,本文的方法可以生成一个范式的最小集合,减少了生成测试用例的数量,提高了测试用例的效率.     

多Agent VSK-AF逻辑

提出了对多Agent系统的信息特征进行推理的形式化体系VSK-AF逻辑，建立了它与多Agent系统的形式化模型间的关系，给出了该逻辑的公理体系和交互公理，证明了该逻辑公理体系的一致性、无矛盾性以及完全性。讨论了进一步的研究工作。     

模糊近似空间上的粗糙模糊集的公理系统

粗糙集理论是近年来发展起来的一种有效的处理不精确、不确定、含糊信息的理论，在机器学习及数据挖掘等领域获得了成功的应用．粗糙集的公理系统是粗糙集理论与应用的基础．粗糙模糊集是粗糙集理论的自然的有意义的推广．作者研究了模糊近似空间上的粗糙模糊集的公理系统，用三条简洁的相互独立的公理完全刻划了模糊近似空间上的粗糙模糊集，同时还把作者给出的公理系统与粗糙集的公理系统做了对比，指出了两者的区别．     

用代数系统描述数据对象及其操作方法的研究

本文旨在研究使用代数系统对CMM管理工具所需数据对象及其上操作进行统一描述的方法，结合代数系统的定义和定理，将数据对象的全体看作集合，将数据对象上的各种操作定义成该集合上的运算，从而构成代数系统，实例证明,本方法可以和已有的抽象代数系统联系起来，从而为控制数据对象上的各种操作提供可靠的理论依据。     

一般术语公理下的模糊描述逻辑FALCN推理

分析了一般术语公理下推理的主要难点:在模糊解释中的隶属度不是离散值,而是区间[0,1]上的连续值.为解决该难点,提出了模糊描述逻辑FALCN下的模糊解释离散化方法,从而使解释中的隶属度都属于一个特殊的有限离散集合.基于该离散化方法,给出一般术语公理下FALCN推理问题的离散Tableau推理技术,包括离散Tableau的定义以及离散Tableau的构造算法,并证明了算法的正确性、完备性和复杂度.     

消息驱动的在线动态系统模板设计与实现

本文讨论了利用消息驱动机制对在线动态系统进行系统设计的思想与方法，介绍了作者用该方法设计的系统模板及其基本构成：即消息发生器集合、消息响应器集合和运行系统。该系统模板集成了过程工业在线动态系统的主要功能，建立了与实际系统的链接关系，可作为过程工业在线动态软件系统设计的系统核心和工具软件。     

粗集公理组的极小化

粗集公理化是粗集理论研究的一个重要部分，它的目标是获得可靠和极小的粗集公理组，以往文献在这一研究中取得了有意义的进展，给出了若干组粗集公理，但是，它们在粗集公理的表示形式，粗集公理组的极小化以及粗集公理组的可行性证明中，尚未达到粗集公理化的理想目前，该文在以往文献的基础上，研究了粗集公理组的极小化，首先，去除了现有的粗集公理组中稳含着沉余性，得到了更为精练的两组粗集公理，并证明了它们的可靠性，其次，定义了极小粗集公理组概念，并证明了给了的两组粗集公理是极小的，最后，讨论了一个典型粗集公理组S5，并证明了它的可靠性和极小化。     

On minimization of axiom sets characterizing covering-based approximation operators

Rough set theory was proposed by Pawlak to deal with the vagueness and granularity in information systems. The classical relation-based Pawlak rough set theory has been extended to covering-based generalized rough set theory. The rough set axiom system is the foundation of the covering-based generalized rough set theory, because the axiomatic characterizations of covering-based approximation operators guarantee the existence of coverings reproducing the operators. In this paper, the equivalent characterizations for the independent axiom sets of four types of covering-based generalized rough sets are investigated, and more refined axiom sets are presented.     

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

为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义．从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系．提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统．以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。     

Proof-Guided Test Selection from First-Order Specifications with Equality

This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally defined for algebraic specifications, to quantifier-free first-order specifications with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the specification axioms. It is based on a proof search for the different instances of the test purpose. Since the calculus is sound and complete, this allows us to provide a full coverage of this property. The generalisation we propose allows to deal with any kind of predicate (not only equality) and with any form of axiom and test purpose (not only equations or Horn clauses). Moreover, it improves our previous works with efficiently dealing with the equality predicate, thanks to the paramodulation rule.     

A parameterized multilevel pattern matching architecture on FPGAs for network intrusion detection and prevention

Pattern matching is one of the most performance-critical components for the content inspection based applications of network security, such as network intrusion detection and prevention. To keep up with the increasing speed network, this component needs to be accelerated by well designed custom coprocessor. This paper presents a parameterized multilevel pattern matching architecture (MPM) which is used on FPGAs. To achieve less chip area, the architecture is designed based on the idea of selected character decoding (SCD) and multilevel method which are analyzed in detail. This paper also proposes an MPM generator that can generate RTL-level codes of MPM by giving a pattern set and predefined parameters. With the generator, the efficient MPM architecture can be generated and embedded to a total hardware solution. The third contribution is a mathematical model and formula to estimate the chip area for each MPM before it is generated, which is useful for choosing the proper type of FPGAs. One example MPM architecture is implemented by giving 1785 patterns of Snort on Xilinx Virtex 2 Pro FPGA. The results show that this MPM can achieve 4.3 Gbps throughput with 5 stages of pipelines and 0.22 slices per character, about one half chip area of the most area-efficient architecture in literature. Other results are given to show that MPM is also efficient for general random pattern sets. The performance of MPM can be scalable near linearly, potential for more than 100 Gbps throughput. Supported by the National Natural Science Foundation of China (Grant No. 60803002), and the Excellent Young Scholars Research Fund of Beijing Institute of Technology     

Another set of conditions for average optimality in Markov control processes

The existence of an average cost optimal stationary policy in a countable state Markov decision chain is shown under assumptions weaker than those given by Sennott (1989). This treatment is a modification of that given by Hu (1992), and is related to conditions of Hordijk (1977). An example is given for which the new axiom set holds whereas the axiom set of Sennott (1989) fails to hold.     

The axiomatic characterizations on L-fuzzy covering-based approximation operators

Axiomatic characterization is the foundation of L-fuzzy rough set theory: the axiom sets of approximation operators guarantee the existence of L-fuzzy relations or L-fuzzy coverings that reproduce the approximation operators. Axiomatic characterizations of approximation operators based on L-fuzzy coverings have not been fully explored, although those based on L-fuzzy relations have been studied thoroughly. Focusing on three pairs of widely used L-fuzzy covering-based approximation operators, we establish an axiom set for each of them, and their independence is examined. It should be noted that the axiom set of each L-fuzzy covering-based approximation operator is different from its crisp counterpart, with an either new or stronger axiom included in the L-fuzzy version.     

MPM simulation of interacting fluids and solids

The material point method (MPM) has attracted increasing attention from the graphics community, as it combines the strengths of both particle‐ and grid‐based solvers. Like the smoothed particle hydrodynamics (SPH) scheme, MPM uses particles to discretize the simulation domain and represent the fundamental unknowns. This makes it insensitive to geometric and topological changes, and readily parallelizable on a GPU. Like grid‐based solvers, MPM uses a background mesh for calculating spatial derivatives, providing more accurate and more stable results than a purely particle‐based scheme. MPM has been very successful in simulating both fluid flow and solid deformation, but less so in dealing with multiple fluids and solids, where the dynamic fluid‐solid interaction poses a major challenge. To address this shortcoming of MPM, we propose a new set of mathematical and computational schemes which enable efficient and robust fluid‐solid interaction within the MPM framework. These versatile schemes support simulation of both multiphase flow and fully‐coupled solid‐fluid systems. A series of examples is presented to demonstrate their capabilities and performance in the presence of various interacting fluids and solids, including multiphase flow, fluid‐solid interaction, and dissolution.     

Thermodynamics-inspired inverse halftoning viamultiple halftone images

Based on an analogy between thermodynamics and Bayesian inference,inverse halftoning was formulated using multiple halftone images based on Bayesian inference using the maximizer of the posterior marginal(MPM) estimate.Applying Monte Carlo simulation to a set of snapshots of the Q-Ising model,it was demonstrated that optimal performance is achieved around the Bayes-optimal condition within statistical uncertainty and that the performance of the Bayes-optimal solution is superior to that of the maximum-a-posteriori(MAP) estimation which is a deterministic limit of the MPM estimate.These properties were qualitatively confirmed by the mean-field theory using an infinite-range model established in statistical mechanics.Additionally,a practical and useful method was constructed using the statistical mechanical iterative method via the Bethe approximation.Numerical simulations for a 256-grayscale standard image show that Bethe approximation works as good as the MPM estimation if the parameters are set appropriately.     

F-SHIQ公理体系及其OWL扩展

随着计算机和Internet的快速发展,语义网和描述逻辑在人工智能等领域扮演着越来越重要的角色。但在日常生活中,越来越多不确定的、不完整的知识需要解决,而现存的OWL只能表述确定的完整的概念和关系。为了能够表示和推理模糊知识,给出了一个基于描述逻辑SHIQ的全新的模糊描述逻辑公理体系——F-SHIQ公理体系,并以此公理体系为基础,扩展了OWL本体语言,能够描述和推理模糊知识。该文首先给出了系统详细的定义、公理、定理以及定理的证明;然后详述了如何用FSRL,即基于F-SHIQ的OWL扩展,来表示和推理模糊信息;最后通过一个例子来检验扩展语言的应用效果。