Computation Tree Logic Model Checking of Multi-Agent Systems Based on Fuzzy Epistemic Interpreted Systems

Model checking is an automated formal verification method to verify whether epistemic multi-agent systems adhere to property specifications.Although there is an extensive literature on qualitative properties such as safety and liveness,there is still a lack of quantitative and uncertain property verifications for these systems.In uncertain environments,agents must make judicious decisions based on subjective epistemic.To verify epistemic and measurable properties in multi-agent systems,this paper extends fuzzy computation tree logic by introducing epistemic modalities and proposing a new Fuzzy Computation Tree Logic of Knowledge(FCTLK).We represent fuzzy multi-agent systems as distributed knowledge bases with fuzzy epistemic interpreted systems.In addition,we provide a transformation algorithm from fuzzy epistemic interpreted systems to fuzzy Kripke structures,as well as transformation rules from FCTLK formulas to Fuzzy Computation Tree Logic(FCTL)formulas.Accordingly,we transform the FCTLK model checking problem into the FCTL model checking.This enables the verification of FCTLK formulas by using the fuzzy model checking algorithm of FCTL without additional computational overheads.Finally,we present correctness proofs and complexity analyses of the proposed algorithms.Additionally,we further illustrate the practical application of our approach through an example of a train control system.

Cost of Multicast Logical Key Tree Based on Hierarchical Data Processing

How to design a multicast key management system with high performance is a hot issue now. This paper will apply the idea of hierarchical data processing to construct a common analytic model based on directed logical key tree and supply two important metrics to this problem： re-keying cost and key storage cost. The paper gives the basic theory to the hierarchical data processing and the analyzing model to multieast key management based on logical key tree. It has been proved that the 4-ray tree has the best performance in using these metrics. The key management problem is also investigated based on user probability model, and gives two evaluating parameters to re-keying and key storage cost.

Uncertainties in estimation of extrapolated annual occurence rate of earthquakes using logical tree

he logical tree methods are used for evaluate quantitatively relationship between frequency and magnitude, and deduce uncertainties of annual occurrence rate of earthquakes in the periods of lower magnitude earthquake. The uncertainties include deviations from the self-similarity of frequency-magnitude relations, different fitting methods, different methods obtained the annual occurrence rate, magnitude step used in fitting, start magnitude, error of magnitude and so on. Taking Xianshuihe River source zone as an example, we analyze uncertainties of occurrence rate of earthquakes M4, which is needed in risk evaluation extrapolating from frequency-magnitude relations of stronger earthquakes. The annual occurrence rate of M4 is usually required for seismic hazard assessment.The sensitivity analysis and examinations indicate that, in the same frequencymagnitude relations fitting method, the most sensitive factor is annual occurrence rate, the second is magnitude step and the following is start magnitude. Effect of magnitude error is rather small.Procedure of estimating the uncertainties is as follows:①Establishing a logical tree described uncertainties in frequencymagnitude relations by available data and knowledge about studied region.② Calculating frequencymagnitude relations for each end branches. ③ Examining sensitivities of each uncertainty factors, amending structure of logical tree and adjusting original weights. ④ Recalculating frequencymagnitude relations of end branches and complementary cumulative distribution function (CCDF) in each magnitude intervals.⑤ Obtaining an annual occurrence rate of M4 earthquakes under given fractiles.Taking fractiles as 20% and 80%, annual occurrence rate of M 4 events in Xianshuihe seismic zone is 0.643 0. The annual occurrence rate is 0.631 8 under fractiles of 50%, which is very close to that under fractiles 20% and 80%.

基于模糊测度的模糊分支时态逻辑模型检测

针对具有模糊性和不确定性的复杂系统的验证问题,提出一种基于模糊测度的模糊分支时态逻辑模型检测算法。首先,在模糊决策过程模型的基础上引入模糊分支时态逻辑的语法和语义。然后,给出模糊分支时态逻辑模型检测算法,该算法将模型检测问题转化为矩阵运算,具有计算方式简洁、复杂度较低的优点。最后,通过医疗专家系统的实例说明了该模型检测算法的有效性。

Fault detection and identification based on combining logic and model in a wall-climbing robot

A combined logic- and model-based approach to fault detection and identification （FDI） in a suction foot control system of a wall-climbing robot is presented in this paper. For the control system, some fault models are derived by kinematics analysis. Moreover, the logic relations of the system states are known in advance. First, a fault tree is used to analyze the system by evaluating the basic events （elementary causes）, which can lead to a root event （a particular fault）. Then, a multiple-model adaptive estimation algorithm is used to detect and identify the model-known faults. Finally, based on the system states of the robot and the results of the estimation, the model-unknown faults are also identified using logical reasoning. Experiments show that the proposed approach based on the combination of logical reasoning and model estimating is efficient in the FDI of the robot.

模糊Kripke结构的子模型修复算法

在模糊模型检测时,如果模糊Kripke结构不满足性质规约,模型检测工具会给出模型中违反性质规约的反例,这往往需要设计人员手工修复,会导致效率低下,因此如何对模糊Kripke结构进行自动修复具有极大的研究意义。由此,提出一个基于模糊tableaux方法的子模型修复算法,从而将经典的模型修复算法提升到模糊系统中,使得模糊Kripke结构能够自动修复。通过一个医疗诊断的例子来阐述该算法在实际中的价值。

Kabbalah Logic and Semantic Foundations for a Postmodern Fuzzy Set and Fuzzy Logic Theory

Despite half a century of fuzzy sets and fuzzy logic progress, as fuzzy sets address complex and uncertain information through the lens of human knowledge and subjectivity, more progress is needed in the semantics of fuzzy sets and in exploring the multi-modal aspect of fuzzy logic due to the different cognitive, emotional and behavioral angles of assessing truth. We lay here the foundations of a postmodern fuzzy set and fuzzy logic theory addressing these issues by deconstructing fuzzy truth values and fuzzy set membership functions to re-capture the human knowledge and subjectivity structure in membership function evaluations. We formulate a fractal multi-modal logic of Kabbalah which integrates the cognitive, emotional and behavioral levels of humanistic systems into epistemic and modal, deontic and doxastic and dynamic multi-modal logic. This is done by creating a fractal multi-modal Kabbalah possible worlds semantic frame of Kripke model type. The Kabbalah possible worlds semantic frame integrates together both the multi-modal logic aspects and their Kripke possible worlds model. We will not focus here on modal operators and axiom sets. We constructively define a fractal multi-modal Kabbalistic L-fuzzy set as the central concept of the postmodern fuzzy set theory based on Kabbalah logic and semantics.

基于风险-可靠性的地铁车辆设备状态评价及维修决策方法研究

地铁车辆设备维修是保障地铁高效运营和安全可靠的重要环节,为提高车辆设备维修质量和维修效率,需研究车辆设备状态评价及维修决策方法。通过对车辆设备部件故障风险和性能可靠性研究,提出了基于风险-可靠性的地铁车辆设备状态评价及维修决策方法。介绍了部件风险等级评价、部件可靠性等级评价和部件重要类型分类的具体内容;通过故障模式、风险等级和可靠性指标对部件进行了重要性分类,介绍了不同重要性部件的维修逻辑决断树;以受电弓为例进行了应用验证。采用该方法可有效提高车辆设备维修质量和维保效率。

基于树形Mux的逻辑电路优化

为实现用case语句描述的逻辑电路的面积和延迟优化,提出了一种基于树形Mux的逻辑电路优化方法.该方法先将case语句转换为树形Mux,通过合并case语句实现Mux树中Mux门的个数和层级减少,并通过化简地址逻辑实现地址再编码电路的精简,进而实现映射后电路面积与延迟的优化.提出的算法使用C++语言实现,电路面积和延迟优化结果由常用学术开源EDA工具abc,结合国内EDA公司提供的映射库得到.实验结果表明,相比于abc工具,使用该方法得到的面积和延迟优化分别提升了26%和21%.

基于BDI逻辑的多Agent系统的学习机制

虽然理性Agent的信念-愿望-意图(BDI)模型很重要,但是它的两个主要缺陷仍没解决:缺少学习能力、缺少明确的多Agent功能。从多Agent学习角度,使用带有学习能力的多Agent系统背景对BDI-Agent结构进行扩展,并利用“作为一阶方法的”逻辑决策树归纳,使得“在Agent的规划可以成功执行时,Agent能够进行学习”。这样的BDI学习Agent体系结构可以在单个表处理语言Lisp中并行执行多Agent系统,而且这一方法可以保持学习与实践推理理论之间的一致性。

基于故障树的某型舰炮异常输出故障分析

舰炮具有射速高、反应快、持续作战能力强、使用效费比高等优点,被越来越多国家所重视。作为舰炮的核心,舰炮逻辑控制系统对于舰炮安全可靠工作发挥着举足轻重的作用。论文针对某型舰炮异常输出故障,采用故障树分析法,对其进行了详细分析与故障定位,找到了故障根本原因,提出了两种解决方法,通过进一步分析比较优选了一种最佳方案。在后续的试验中验证了该方法的可行性和有效性。

软PLC梯形图到语句表转换新策略的研究

提出了一种用于实现软PLC梯形图到语句表转换的新策略。首先将梯形图映射为AOV图,然后对每级的AOV图进行扫描以确定各顶点之间的不同层次的串并联关系,扫描的同时自底向上建立一棵逻辑树以保存扫描结果,最后通过遍历这棵树生成语句表。通过实例说明此策略能清晰地表达出梯形图各元件的逻辑关系,语句表转换过程准确快速。执行过程中还能对梯形图进行逻辑查错和规范检查。

组播密钥管理的研究进展

缺乏安全机制限制了组播在各种网络业务中的应用.组播密钥管理通过为组播成员生成、发送和更新组密钥来满足加密认证等安全需求.组播密钥管理方案的设计,除了要满足基本的安全需求,还要兼顾可扩展性、健壮性、可靠性等多方面因素.分析了组播密钥管理所面临的问题,并通过对已有的几种组播密钥树方案的介绍,探讨和总结了组播密钥管理的研究现状和发展趋势.

基于多阈值融合的图像分割

提出了一种基于知识的多阈值融合图像分割新方法 .首先利用一组多阈值分割结果建立连通域生长树 .然后判断树叉对应的连通域合并是否合理 ,为此提出了连通体元、体元生命期、体元体积等概念 ,结合灰度均匀性定义出通用合并准则 .最后将图像各位置的最佳连通域组合为最终图像分割结果 .该算法充分利用了目标的灰度和空间属性 ,对灰度平稳和渐近变化的多目标图像分割非常有效 .此外 ,该算法可以有效融合具体应用的先验知识 ,具有很高的智能性 .

基于事故场景的海洋平台应急撤离风险分析

为提高海洋平台事故发生时应急撤离(EER)效率、减少人员伤亡,基于事故案例调研结果对应急撤离过程进行风险分析。首先提取各阶段事故致因因素,采用逻辑树模型探索致因因素内在逻辑关系和人员死亡事故模式及风险路径,进而提出风险控制措施,最后基于屏障理论建立安全屏障模型。结果表明:海洋平台应急撤离事故是环境、人因、设备、管理多因耦合结果;逻辑树模型能直观系统地展示事故发生的因果关系,利用逻辑树模型得出应急撤离事故的4种人员死亡模式和9条风险传播路径;基于控制措施的安全屏障模型是应急撤离有效响应的保障。

基于粗糙集的逻辑故障树方法及其应用

故障树是一种分析复杂系统可靠性、诊断系统故障的有效方法。在传统的故障树方法中 ,故障树的生成通常靠人工完成。故障知识的获取以及故障树结构的确定一直是有待解决的瓶颈问题。这里结合粗糙集、专家系统及人工智能等理论 ,提出了构造逻辑故障树进行故障诊断的方法并给出了相应的故障树评价标准。这种方法利用粗糙集对知识系统的知识发现和知识提取能力 ,从系统运行状态样本中建立基于知识的故障树模型。通过实例讨论了如何运用该方法对工业监控过程进行故障建模 ,检测系统运行过程中所发生的故障。

利用场址的地震影响烈度资料的地震危险性分析

本文提出一种依据场址历史地震资料进行危险性分析的方法。在证明其地震影响烈度的频次与相应的烈度值呈对数线性关系的基础上,利用最大似然法,求出β,λ和I_(max)并得出各场址的危险性分析结果。同时,用“逻辑树”方法对各场址的危险性结果进行不确定性校正,得到的各场址的危险性分析的最终结果表明,这种方法是可行的,尤对呈现过烈度异常的区域,本方法的结果更能显示其特殊性。

基于逻辑树的水尺计重误差分析

在全面介绍逻辑树方法的原理及水尺计重方法的基础上,将"问题树"作为基本构造框架,经过逐层分析,找到影响水尺计重误差的所有相关问题,并据此建立水尺计重误差逻辑树。根据各类误差的定义,对26种误差源进行分类,并结合水尺计重算法分析各类误差的修正方法。在水尺计重的众多误差源中,甄别出水流导致的船体下沉造成的误差尚未得到修正。该误差属于系统误差,理应通过改进测量方法或增加修正量予以消减。

基于Petri网的服务组合故障诊断与处理

通过分析服务组合的故障需求,给出服务组合故障处理的框架.该框架采用Petri网来解决服务组合的错误发现及其处理问题.重点讨论了可用服务失败、组件失败及网络故障的情况,并相应地给出了服务组合故障模型.在此基础上对故障处理模型进行分析,给出服务组合故障处理正确性准则,并证明了其正确性.最后,采用CTL(computational tree logic)描述相关性质并提出验证服务组合故障分析的实施算法.仿真结果表明,该方法在处理服务组合故障时具有一定的优越性.

联锁逻辑模型的安全性分析

故障树分析法(FTA)用于静态分析系统失效的可能事件和状态,是分析安全苛求系统的可靠性和安全性的一种有效方法。时间Petri网(TPN)描述具有时序关系的并发系统,用于系统行为的动态建模。但利用时间Petri网无法严格证明其模型是安全的。提出了一种用于时间Petri网模型的安全性分析方法,该方法有效地结合故障树分析法和时间Petri网的各自优点,实际应用于联锁逻辑模型的安全性分析,并对不安全的模型提出修正方案。