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.

Completeness of bounded model checking temporal logic of knowledge

In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.

An Extended Ontology Model and Ontology Checking Based on Description Logics

Ontology is defined as an explicit specification of a conceptualization. In this paper, an extended ontology model was constructed using description logics, which is a 5-tuples including term set, individual set, term definition set, instantiation assertion set and term restriction set. Based on the extended model, the issue on ontology checking was studied with the conclusion that the four kinds of term checking, including term satisfiability checking, term subsumption checking, term equivalence checking and term disjointness checking, can be reduced to the satisfiability checking, and satisfiability checking can be transformed into instantiation consistence checking.

Intrusion Detection Algorithm Based on Model Checking Interval Temporal Logic

Model checking based on linear temporal logic reduces the false negative rate of misuse detection.However,linear temporal logic formulae cannot be used to describe concurrent attacks and piecewise attacks.So there is still a high rate of false negatives in detecting these complex attack patterns.To solve this problem,we use interval temporal logic formulae to describe concurrent attacks and piecewise attacks.On this basis,we formalize a novel algorithm for intrusion detection based on model checking interval temporal logic.Compared with the method based on model checking linear temporal logic,the new algorithm can find unknown succinct attacks.The simulation results show that the new method can effectively reduce the false negative rate of concurrent attacks and piecewise attacks.

Model Checking over Paraconsistent Temporal Logic

Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a guasi-classical temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures (extended standard Kripke structures), in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.

基于可靠度差值特征的自适应判决多元LDPC译码算法

利用变量节点符号可靠度在迭代过程中的分布特征,提出了一种基于可靠度差值特征的自适应判决多元低密度奇偶校验(Low Density Parity Check, LDPC)译码算法。整个迭代过程划分为两个阶段,针对不同阶段节点可靠度的差值特征分别采用不同的判决策略:前期阶段,采用传统的基于最大可靠度的判决策略;后期阶段,根据最大、次大可靠度之间的差值特征,设计自适应的码元符号判决策略。仿真结果表明,所提算法在相当的译码复杂度前提下,能获得0.15~0.4 dB的性能增益。同时,对于列重较小的LDPC码,具有更低的译码错误平层。

基于XMG的乘法器电路等价性验证算法

组合电路等价性验证是数字集成电路设计自动化(EDA)中的重要部分,随着算术电路在现代计算机系统中的占比逐渐增大,传统的等价性验证算法在验证多比特算术电路,尤其是乘法器电路时面临挑战.对此,提出一种基于XOR-Majority Graph(XMG)逻辑表示的组合电路等价性验证算法.首先将2个待验证电路构建成的联接(Miter)电路进行XMG逻辑重写;然后在等价性一致的前提下对XMG的节点个数和逻辑深度进行逻辑重写优化;最后调用布尔可满足性(SAT)求解器和仿真器进行验证,得到最终等价性验证结果.实验结果表明,与ABC,Lingeling等工具相比,所提算法在验证时间上实现了平均489倍、最高1472倍的加速.

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

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

25 Hz相敏轨道电路与ZPW-2000A结合处的逻辑检查故障分析

25 Hz相敏轨道电路与ZPW-2000A轨道电路特性不同,但在自动闭塞及站内电码化改造过程中两种制式轨道电路常结合应用。不同的特性会导致结合处的逻辑检查失效。针对场联进路无法正常解锁、三接近闭塞分区遗留失去分路故障进行分析,介绍故障发生的场景及原因,并讨论计算机联锁、列控中心、区间综合监控系统以及继电逻辑检查电路对于此类故障的解决方案,为后续工程设计及故障处理提供参考。

构建电子病历逻辑校验原则对医院国际疾病分类编码正确率的影响

目的:分析构建电子病历逻辑校验原则对医院国际疾病分类(ICD)编码正确率的影响。方法:选取2021年1月—2022年12月高州市人民医院归档的220000份电子病历及作为研究对象,其中2021年1—12月112000份,2022年1—12月108000份。筛查2021年1—12月违反ICD编码逻辑规则的电子病历,分析错误原因,制定适合高州市人民医院的电子病历ICD逻辑校验原则。将ICD逻辑校验原则应用于2022年1—12月住院病案首页编码工作中。比较2021年及2022年住院病案首页ICD编码填写正确率及住院病案首页数据质量。结果:2022年ICD编码正确率高于2021年,差异有统计学意义(P<0.001)。2022年住院病案首页数据质量评分高于2021年,差异有统计学意义(P<0.001)。结论:构建电子病历逻辑校验原则可减少逻辑编码错误率,提高住院病案首页数据质量。

基于一阶谓词逻辑的结构设计规范表示方法

目前,基于BIM模型的合规性审查采用人工方式,工作量繁重且自动化程度低,开展自动合规性审查研究具有重要意义。在结构设计领域能够有效支撑规范知识表示与推理并支持设计审查自动化的设计规范表达方法有待开发。基于一阶谓词逻辑,通过转译《混凝土结构设计规范》中的设计条款,提出一种结构设计规范规则表达和推理方法。该方法可实现将半结构化设计规范条款转换为结构化知识并支持灵活查询与推理,通过“谓词定义”和“函数定义”转译设计规范中语言类、表格类和计算公式类设计条款,提出两种规范条款谓词定义方式。对于语言模糊类、表后注释类和条款补充类的设计条款给出转译解决方案。提出的方法有效地解决了传统一阶谓词对于结构设计条款表示不充分和不精确的问题,进而为设计规范的计算机表达提供一种参考方法。

Model Checking Workflow Net Based on Petri Net

The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.

Automatic Verification of Biochemical Network Using Model Checking Method

This study focuses on automatic searching and verifying methods for the teachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic （CTL）. This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.

Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study

A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.

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

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

一种引入积分修正的二维信息大数逻辑LDPC译码算法

为了解决基于可靠度的迭代大数逻辑译码(Modified Reliability-based Iterative Majority Logic Decoding,MRBI-MLGD)算法的错误平层问题,提出了一种基于大数逻辑的低密度奇偶校验(Low Density Parity Check,LDPC)译码算法。所提算法在译码函数中引入积分修正项,实现了基于二维信息修正的译码策略,可有效降低错误平层。此外,与基于二元译码信息的的迭代大数逻辑译码(Binary Message Majority Logic Decoding,BM-MLGD)算法不一样,所提算法可适用于不同列重的LDPC码。仿真结果表明,所提译码算法在整个工作信噪比区间内都具有稳定的译码性能,表现出更好的普适性和鲁棒性。

基于装置监视自检逻辑的直流保护系统架构可靠性分析

针对当前特高压直流保护系统架构可靠性建模求解困难的问题,提出基于装置监视自检逻辑的直流保护系统架构可修复Markov状态空间分析方法。首先,根据直流保护系统架构层间、层内运行模式特点及装置监视自检逻辑,进一步细化保护装置的故障状态分类,并针对不同故障状态的保护装置采用不同的保护退出策略;其次,根据监视自检逻辑下具体运行情景的冗余保护退出情况,确定直流保护系统架构的运行状态,建立基于监视自检逻辑的直流保护系统架构可修复Markov模型;最后,根据实际故障参数、检修经验及通过概率统计得到的状态转换率,对模型进行算例仿真。仿真结果表明:运维人员巡检频率一定时,采用基于装置监视自检逻辑的保护退出策略,能使直流保护系统架构不可用度降低约23,具有一定的实际意义。

既有线增加区间占用逻辑检查试验方法思考

区间占用逻辑检查功能的实现,高速铁路、城际铁路多以增加列控中心功能方式,普速铁路多以增加继电电路、区间综合监控系统(QJK)的方式。既有线在非同步大修的情况下增加逻辑检查功能受施工条件、天窗时间和人员组织等限制,难度大,风险高。针对既有线施工实际情况,分别就以上两种方式对试验方法进行归纳总结,详细论述试验项目、试验方法和试验内容,对联锁试验方案进行优化,在降低工作量的同时确保联锁关系正确。

区间逻辑检查进站外方区段延迟解锁原因分析及对策

从增加区间逻辑检查设备功能入手,分析增加设备后存在进站外方闭塞分区晚于站内区段出清及不能正常解锁现象的原因,分析产生该现象的原因,提出改进电路图设计等措施和建议,在保证联锁安全的同时减小对运输影响,具有易操作、可推广的现实价值和意义,供设计、施工、维护、运营单位在日常工作中参考和借鉴。

低密度奇偶校验码的低复杂度迭代译码算法

迭代大数逻辑(iterative majority-logic decoding,IMLGD)译码算法是低密度奇偶校验(low-density parity-check,LDPC)码的一类重要的迭代译码算法。相对LDPC码基于置信传播准则的译码算法,IMLGD译码算法的复杂度有所降低,但是性能有所下降。针对这一问题,提出了一种修正迭代大数逻辑译码算法(modified iterative majority-logic decoding,MIMLGD)。该算法利用校验方程的置信度对译码迭代过程中的各比特外信息进行修正。仿真结果表明,提出的MIMLGD译码算法相对于原始迭代大数逻辑译码算法在同样信噪比下具有更低的误比特率。此外,该算法保持了IMLGD译码算法的低复杂度特征,并且避免了对于特定的码搜索修正因子的过程,具有良好的通用性,是实际应用的良好选择。