π-演算互模拟判定算法的优化和实现

π-演算采用互模拟作为进程等价的准则.对有限状态的π-演算进程互模拟等价是可判定的,由此提出了互模拟检测算法的一种优化技术.该技术基于只将输入名字实例化为在以后的等名测试中用到的自由名字.通过实例说明这一优化技术可大大减少所用的时间和空间,并证明了优化算法的正确性.     

基于社会网络的(α,k)-匿名方法

随着网络技术的快速发展,大量在线社会网络的建立和使用,越来越多的人参加到社会网络中分享和交流信息,而在这种交互过程中,会产生大量的数据。这些数据中有些是用户个人生活领域中不愿意别人知道的事情,可以认为它们是用户的隐私。社会网络数据发布的隐私保护成为新兴的研究课题。本文提出了应用于社会网络的(α,k)-匿名方法,采用基于聚类的方法,对节点的属性及节点之间的关系进行保护。每个聚类中的节点数至少为k个,并且聚类中任一敏感属性值相关的节点的百分比不高于α。理论分析和实验结果表明,基于社会网络的(α,k)-匿名方法能在信息损失尽可能小的情况下有效地保护隐私。     

2-苯乙醇-α-环糊精包合物的分子模拟研究

用分子动力学的方法模拟了2-苯乙醇的α-环糊精包合物在真空中的动态结构和运动轨迹.通过对分子模拟结果的分析,揭示了2-苯乙醇的两种α-环糊精包合物的相对稳定性,并根据PM3量化计算的包合稳定能、包合作用的结果得出了2-苯乙醇的α-环糊精包合物的最稳定结构为A型,即2-苯乙醇的羟乙基在α-环糊精窄口处.最后利用紫外光谱的变化规律给予了实验验证.分子模拟的统计分析结果表明,苯乙醇与α-环糊精形成的A构型包合物不仅物理稳定性最好,而且化学稳定性也最佳.     

(α,β)-软BCK代数

将软集的参数集赋予BCK代数的代数结构,给出了(α,β)-软BCK代数的概念,并验证了得到的(α,β)-软BCK代数是交软BCK代数和α-交软BCK代数的非平凡推广;得到了两个(α,β)-软BCK代数在软集的交、并、且等运算下仍然是(α,β)-软BCK代数的结论,并讨论了(α,β)-软BCK代数的同态像和原像的性质;最后运用对偶软集的方法给出了(α,β)-软BCK代数的等价刻画。     

基于符号迁移图的互模拟验证算法

符号迁移图是传值进程的一种直观而简洁的语义表示模型，该模型由Hennessy和Lin首先提出，随后又被Lin推广至带赋值的符号迁移图，本文不但定义了符号迁移图各种版本（基／符号）的强操作语义和强互模拟，提出了相互的强互模拟算法，而且通过引入符号观察图和符号同余图，给出了其弱互模拟等价和观察同余的验证算法，给出并证明了了τ－循环和τ－边消去定理，在应用任何弱互模拟观察同余验证算法之前，均可利用这些定理对所给符号迁移图进行化简。     

互模拟准局部验证算法的扩展与实现

互模拟是并发系统的分析和验证的一个重要概念。本文主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统。我们用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法。我们以VLTS为实验数据基准,进行大量的实验,发现在大多数情况下,前者的性能比后者更好。同时,我们修改了算法使其能够验证模拟关系。最后,我们用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系。     

粒化(α,k)-匿名方法研究

针对现有个性化隐私匿名技术不能同时满足面向个体需求的个性化和面向敏感属性值的个性化两方面的要求,引入了粒计算思想。建立隐私保护决策度集合,以刻画不同个体对敏感属性同一敏感值的不同保护要求;基于决策度集合的不同取值建立顶层粒度空间;对每个顶层粒度空间中敏感值赋予不同的出现频率约束,以满足面向敏感值的个性化匿名需求。算法分析及仿真实验结果表明,粒化(α,k)-匿名模型和算法以较小的信息损失和执行时间获得更综合、更合理的个性化隐私保护的实现。     

逻辑LTS预备模拟关系的判定算法

进程代数与时序逻辑是并发理论中应用最为广泛的两大规范系统。近来,Gerald Luttgen等人将二者进行结合,提出了逻辑标记转换系统以及相应的精化关系--LLTS预备模拟。提出了一种LLTS预备模拟关系的等价描述方式--泛化预备模拟,并从划分对的角度出发,给出与该描述等价的稳定划分对概念。基于这一概念给出一种判定两个逻辑标记转换系统之间是否具有LLTS预备模拟关系的理论算法,并证明其正确性。     

非对称χ≠-演算的互模拟格

非对称χ≠-演算是一种移动计算模型.通过研究该演算的互模拟格,能够增强理解非对称性和不等名算子对移动进程代数理论的影响.在给出非对称χ≠-演算的语法和转移语义系统的基础上,定义了该演算的L-互模拟关系.研究表明非对称χ≠-演算的63个L-互模拟关系重叠为12个不同的互模拟关系,而且这12个互模拟关系构成了一个关于集包含的互模拟格.最后证明了barbed互模拟和开互模拟分别与该互模拟格的顶元和底元互模拟关系相重合.     

Potential of 5,10,15,20-Tetrakis(3′,5′-di-tertbutylphenyl)porphyrinatocopper(II) for a multifunctional sensor

An organic compound 5,10,15,20-Tetrakis(3′,5′-di-tertbutylphenyl)porphyrinatocopper(II) (TDTPPCu) is synthesized and studied as an active material for multifunctional capacitive sensor. The capacitance of the device as a function of illumination, humidity and temperature has been investigated. It is observed that the capacitance increases by 4.7 times from the dark condition under an illumination of 3850 lx. The capacitance is also changed 9.5 times with the increase in relative humidity (RH) from 30% to 95%. No change in capacitance appeared below critical temperature 120 °C. Based on the experimental results for the multifunctional sensor a mathematical model has been developed. The model is mainly based on the assumption that the capacitive response of the sensor is associated with dielectric polarization. The sensors are simulated using this model. The simulated results match well with experimental results.     

(λ,μ)Vague商环

引入了[(λ,μ)]Vague环,[(λ,μ)]Vague理想的概念,利用截集给出了它们的等价刻画,研究了同态映射下它们的像与原像的问题,在此基础上通过构造陪集的方法引入了[(λ,μ)]Vague商环,给出了[(λ,μ)]Vague商环的同构定理,初步探索了[(λ,μ)]Vague环的理论。     

Requirements for computational rule checking of requests for proposals (RFPs) for building designs in South Korea

This study reports on the requirements for developing computer-interpretable rules for checking the compliance of a building design in a request for proposal (RFP), especially in the building information modeling (BIM) environment. It focuses on RFPs for large public buildings (over 5 million dollars) in South Korea, which generally entail complex designs. A total of 27 RFPs for housing, office, exhibition, hospital, sports center, and courthouse projects were analyzed to develop computer-interpreted RFP rules. Each RFP was composed of over 1800 sentences. Of these, only three to 366 sentences could be translated into a computer-interpretable sentence. For further analysis, this study deployed context-free grammar (CFG) in natural language processing, and classified morphemes into four categories: i.e., object (noun), method (verb), strictness (modal), and others. The subcategorized morphemes included three types of objects, twenty-nine types of methods, and five levels of strictness. The coverage applicability of the derived objects and methods was checked and validated against three additional RFP cases and then through a test case using a newly developed model checker system. The findings are expected to be useful as a guideline and basic data for system developers in the development of a generalized automated design checking system for South Korea.     

Intuitionistic (<Emphasis Type="Italic">S</Emphasis>, <Emphasis Type="Italic">T</Emphasis>)-fuzzy hyperquasigroups

The concept of intuitionistic fuzzy subhyperquasigroups in a hyperquasigroup with respect to an s-norm and a t-norm on intuitionistic fuzzy sets is introduced and their properties of such hyperquasigroups are studied. Intuitionistic (S, T)-fuzzy relations on a hyperquasigroup G are discussed. In particular, we investigate connections hyperquasigroups with binary quasigroups.     

A novel local search algorithm with configuration checking and scoring mechanism for the set k‐covering problem

The set k‐covering problem, an extension of the classical set covering problem, is an important NP‐hard combinatorial optimization problem with extensive applications, including computational biology and wireless network. The aim of this paper is to design a new local search algorithm to solve this problem. First, to overcome the cycling problem in local search, the set k‐covering configuration checking (SKCC) strategy is proposed. Second, we use the cost scheme of elements to define the scoring mechanism so that our algorithm can find different possible good‐quality solutions. Having combined the SKCC strategy with the scoring mechanism, a subset selection strategy is designed to decide which subset should be selected as a candidate solution component. After that, a novel local search framework, as we call DLL_ccsm (diversion local search based on configuration checking and scoring mechanism), is proposed. DLL_ccsm is evaluated against two state‐of‐the‐art algorithms. The experimental results show that DLL_ccsm performs better than its competitors in terms of solution quality in most classical instances.     

Coherence checking and propagation of lower probability bounds

 In this paper we use imprecise probabilities, based on a concept of generalized coherence (g-coherence), for the management of uncertain knowledge and vague information. We face the problem of reducing the computational difficulties in g-coherence checking and propagation of lower conditional probability bounds. We examine a procedure, based on linear systems with a reduced number of unknowns, for the checking of g-coherence. We propose an iterative algorithm to determine the reduced linear systems. Based on the same ideas, we give an algorithm for the propagation of lower probability bounds. We also give some theoretical results that allow, by suitably modifying our algorithms, the g-coherence checking and propagation by working with a reduced set of variables and/or with a reduced set of constraints. Finally, we apply our algorithms to some examples. RID="*" ID="*" This paper is a revised and substantially extended version of a previous paper by the same authors, appeared in the Proc. of the 5th Workshop on Uncertainty Processing (WUPES'2000), Jindřichu̇v Hradec, Czech Republic, June 21–24, 1–13, 2000.     

一种有效的基于LTL和Petri网的模型检测方法

模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。     

灰色GM(1,1,t α)模型与自忆性原理的耦合及应用

针对实际工程应用中传统GM(1,1)模型预测的局限性,以含时间幂次项的灰色GM(1,1,tα)模型为基础,构建了灰色GM(1,1,tα)与自忆性原理的耦合预测模型;用动力系统自忆性原理来克服传统灰色模型对初值比较敏感的弱点;将灰色GM(1,1,t2)自忆性模型应用于某沿海高速软土地基沉降的模拟和预测,获得了满意的模拟和预测精度.实验算例表明,所提出的新模型显著地改善了传统灰色预测模型的模拟预测精度.     

接口自动机的良构性检测算法及其实现

针对构件式系统中任一构件的非良构性会导致系统不能正常运行的问题,提出一种基于接口自动机（IA）来分析和检测构件良构性（well-formedness）的算法,并据此实现了一个构件良构性检测原型系统。该算法首先构造与接口自动机同构的可达图;其次,基于可达图通过深度优先遍历生成一条覆盖所有迁移的有序集;最后,根据该有序集检测在外界环境满足其输入假设的情况下,每个属于方法的活动到其对应返回活动的路径的自治无异常可达性,从而实现接口自动机的良构性检测。根据所提算法在Eclipse平台设计并实现了构件良构性检测原型系统T-CWFC,该系统通过JFLAP建立构件的接口自动机模型并构造其可达图,进而对接口自动机作良构性检测并输出相关检测信息。最后通过对一组构件的良构性检测实验验证了算法的有效性。     

An alternative version of Lauritzen et al.'s algorithm for checking representation of independencies

 Conditional independence relations induced by discrete probabilistic distributions can be represented or approximated by relations defined on Directed Acyclic Graphs (DAGs). An alternative way for representing such relations on “Annotated Graphs” (term defined in the text) is provided. An efficient algorithm, which is an alternative version of a known algorithm, is given, for checking whether a given independency is represented in a given annotated graph. RID="*" ID="*" This work was partially supported by NSF Grant #4-442510-21141. The author thanks to the referees for their helpful remarks and Milan Studeny for his suggestions and help in the preparation of the revised version of the paper.