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.

Identifying Counterexamples Without Variability in Software Product Line Model Checking

Product detection based on state abstraction technologies in the software product line(SPL)is more complex when compared to a single system.This variability constitutes a new complexity,and the counterexample may be valid for some products but spurious for others.In this paper,we found that spurious products are primarily due to the failure states,which correspond to the spurious counterexamples.The violated products correspond to the real counterexamples.Hence,identifying counterexamples is a critical problem in detecting violated products.In our approach,we obtain the violated products through the genuine counterexamples,which have no failure state,to avoid the tedious computation of identifying spurious products dealt with by the existing algorithm.This can be executed in parallel to improve the efficiency further.Experimental results showthat our approach performswell,varying with the growth of the system scale.By analyzing counterexamples in the abstract model,we observed that spurious products occur in the failure state.The approach helps in identifying whether a counterexample is spurious or genuine.The approach also helps to check whether a failure state exists in the counterexample.The performance evaluation shows that the proposed approach helps significantly in improving the efficiency of abstraction-based SPL model checking.

Influence of initial check, information exchange, final accuracy check, reaction information nursing on the psychology of elderly with lung cancer

BACKGROUND As one of the fatal diseases with high incidence,lung cancer has seriously endangered public health and safety.Elderly patients usually have poor self-care and are more likely to show a series of psychological problems.AIM To investigate the effectiveness of the initial check,information exchange,final accuracy check,reaction(IIFAR)information care model on the mental health status of elderly patients with lung cancer.METHODS This study is a single-centre study.We randomly recruited 60 elderly patients with lung cancer who attended our hospital from January 2021 to January 2022.These elderly patients with lung cancer were randomly divided into two groups,with the control group taking the conventional propaganda and education and the observation group taking the IIFAR information care model based on the conventional care protocol.The differences in psychological distress,anxiety and depression,life quality,fatigue,and the locus of control in psychology were compared between these two groups,and the causes of psychological distress were analyzed.RESULTS After the intervention,Distress Thermometer,Hospital Anxiety and Depression Scale(HADS)for anxiety and the HADS for depression,Revised Piper’s Fatigue Scale,and Chance Health Locus of Control scores were lower in the observation group compared to the pre-intervention period in the same group and were significantly lower in the observation group compared to those of the control group(P<0.05).After the intervention,Quality of Life Questionnaire Core 30(QLQ-C30),Internal Health Locus of Control,and Powerful Others Health Locus of Control scores were significantly higher in the observation and the control groups compared to the pre-intervention period in their same group,and QLQ-C30 scores were significantly higher in the observation group compared to those of the control group(P<0.05).CONCLUSION The IIFAR information care model can help elderly patients with lung cancer by reducing their anxiety and depression,psychological distress,and fatigue,improving their tendencies on the locus of control in psychology,and enhancing their life qualities.

Review of Software Model-Checking Techniques for Dealing with Error Detection in Program Codes

Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.

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 Example of Machine Vision Applied in Printing Quality Checking——Research on the Checking of Printing Quality by Image Processing

The traditional printing checking method always uses printing control strips,but the results are not very well in repeatability and stability. In this paper,the checking methods for printing quality basing on image are taken as research objects. On the base of the traditional checking methods of printing quality,combining the method and theory of digital image processing with printing theory in the new domain of image quality checking,it constitute the checking system of printing quality by image processing,and expound the theory design and the model of this system. This is an application of machine vision. It uses the high resolution industrial CCD(Charge Coupled Device) colorful camera. It can display the real-time photographs on the monitor,and input the video signal to the image gathering card,and then the image data transmits through the computer PCI bus to the memory. At the same time,the system carries on processing and data analysis. This method is proved by experiments. The experiments are mainly about the data conversion of image and ink limit show of printing.

基于Model Checking的系统脆弱性分析

基于规则的脆弱性分析技术依赖于对系统组件间关系的经验知识,系统复杂性、竞态条件、隐含假设等因素,使规则的生成异常困难。该文提出了采用NuSMV作为Model Checking执行机验证系统安全行为模型的脆弱性分析方法,并详细描述了对两个模型实例进行验证的过程。结果显示,这种方法具有识别已知和未知脆弱性的能力。

DIAGNOSTIC CHECKING FOR TIME SERIES MODELS USING NONPARAMETRIC APPROACH

In time series modeling, the residuals are often checked for white noise and normality. In practice, the useful tests are Ljung Box test. Mcleod Li test and Lin Mudholkar test. In this paper, we present a nonparametric approach for checking the residuals of time series models. This approach is based on the maximal correlation coefficient ρ 2 * between the residuals and time t . The basic idea is to use the bootstrap to form the null distribution of the statistic ρ 2 * under the null hypothesis H 0:ρ 2 * =0. For calculating ρ 2 * , we proposes a ρ algorithm, analogous to ACE procedure. Power study shows this approach is more powerful than Ljung Box test. Meanwhile, some numerical results and two examples are reported in this paper.

层厚对使用CT/SIM Check模体联合iQA软件检测CT模拟机的影响

目的探讨层厚大小对使用CT/SIM Check模体联合iQA软件检测放疗CT模拟机数据结果的影响。方法对1台西门子Sensation Open CT模拟机,使用6种放疗扫描协议扫描1套CT/SIM Check模体,扫描完成后重建1.5、2、3、4和5 mm共5种层厚的CT图像序列。使用iQA软件对这些CT图像序列进行自动分析并生成报表,对报表上的质控数据结果进行分析和比较。结果通过对报表数据进行分析,得到了6种扫描协议和5种层厚情形下22种参数的质控数据,对5种不同层厚的数据计算得到了相应的四分位数间距值。由数据结果可见,HU均一性和插件4内标准差的数据随层厚的增加而减小;扫描中心纵向坐标的数值随层厚的增加有下降的趋势;线宽比-灵敏度截面的数据随层厚的增加而变大。结论使用CT/SIM Check模体联合iQA软件检测CT模拟机,层厚对HU均一性、插件4内标准差、扫描中心纵向坐标和线宽比-灵敏度截面的质控数据结果有较大影响,对其他参数的数据也有不同程度的影响。本研究为物理师使用CT/SIM Check模体联合iQA软件检测放疗CT模拟机的质控工作,提供了有益的数据参考。

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-Based Testing of Web Applications

A formal model representing the navigation behavior of a Web application as the Kripke structure is proposed and an approach that applies model checking to test case generation is presented. The Object Relation Diagram as the object model is employed to describe the object structure of a Web application design and can be translated into the behavior model. A key problem of model checking-based test generation for a Web application is how to construct a set of trap properties that intend to cause the violations of model checking against the behavior model and output of counterexamples used to construct the test sequences. We give an algorithm that derives trap properties from the object model with respect to node and edge coverage criteria.

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.

Probabilistic Model Checking-Based Survivability Analysis in Vehicle-to-Vehicle Networks

Probabilistic model checking has been widely applied to quantitative analysis of stochastic systems, e.g., analyzing the performance, reliability and survivability of computer and communication systems. In this paper, we extend the application of probabilistic model checking to the vehicle to vehicle(V2V) networks. We first develop a continuous-time Markov chain(CTMC) model for the considered V2V network, after that, the PRISM language is adopted to describe the CTMC model, and continuous-time stochastic logic is used to describe the objective survivability properties. In the analysis, two typical failures are considered, namely the node failure and the link failure, respectively induced by external malicious attacks on a target V2V node, and interrupt in a communication link. Considering these failures, their impacts on the network survivability are demonstrated. It is shown that with increasing failure strength, the network survivability is reduced. On the other hand, the network survivability can be improved with increasing repair rate. The proposed probabilistic model checking-based approach can be effectively used in survivability analysis for the V2V networks, moreover, it is anticipated that the approach can be conveniently extended to other networks.

A New Design and Implementation of an Attendance Checking Node for Coal Mines

A novel design and implementation of an attendance checking node for coal mines based on the CAN bus is presented in this paper. Hardware circuits and programming methods for the attendance checking node are discussed,including the single-chip computer with CAN controller AT89C51CC03,the CAN bus transceiver TJA1050,the large capacity DataFlash memory,the real-time clock DS1302,the voice chip ISD2560 and the card-reading circuit in Wie-gand format. All the extended hardware satisfies the requirements for intrinsically safe circuits (GB3836.4-2000) and intrinsically safe authentication promoted by the national explosion-proof institute. Further,the software programming methods for the CAN controller (AT89C51CC03) and the implementation of the CAN communications protocol are presented as well.

Spatial Topology Rule Checking Algorithm of Linear Entity Based on Quadtree

Spatial topology rule is the primary method to insure the consistency and validity of spatial topology relation in GIS software. Topology rule can be divided into three categories according to geographic entity’s geometric shape: point topology rule, line topology rule and polygon topology rule. At first, this paper summarizes the various linear geographic entities’ topological relations which have practical application, then designs a series of linear entity topology rules detailedly. Based on these rules, this paper proposes a topology rule checking algorithm using quadtree, which is designed on the basis of MAPGIS7.4 spatial data model. The algorithm has already been applied to MAPGIS platform and gained good effects.

Significance of three step prescription checking by pharmacists

In many hospitals,prescription checks are conducted by 2 or 3 individual pharmacists at each step of prescription checking,dispensing,and final checking to maintain the safety and efficacy of pharmaceutical therapies in Japan[1,2].In Gunma University Hospital,we also check all prescriptions by 3 pharmacists at each step of dispensing(3 step prescription check system)with the exception of night time.In this study,to assess the significance of our 3 step prescription check system for managing safety of pharmaceutical therapies,we investigated prescriptions that needed the confirmation of questionable points and prescription corrections.

Analysis of Security of Quantum Key Distribution Based on Entangled Photon Pairs by Model Checking

Quantum key distribution is a technique to securely distribute a bit string between two parties by using the laws of quantum mechanics. The security of this technique depends on the basis of quantum mechanics rather than the difficulty of the mathematical calculation as in the classical encoding. Researches in this field have shown that the quantum key distribution will be fully functioning outside the laboratory in a few years. Due to the complexity and the high efficiency of the device, the verification is needed. In this article, we use PRISM to verify the security of the quantum key distribution protocol, which uses the entangled photon based on BB84 protocol.

GPS based checking survey and precise DEM development in Open mine

The checking survey in Open mine is one of the most frequent and important work.It plays the role of forming a connecting link between open mine planning and pro- duction.Traditional checking method has such disadvantages as long time consumption, heavy workload,complicated calculating process,and lower automation.Used GPS and GIS technologies to systematically study the core issues of checking survey in open mine. A detail GPS data acquisition coding scheme was presented.Based on the scheme an algorithm used for computer semiautomatic cartography was made.Three methods used for eliminating gross errors from raw data which were needed for creating DEM was dis- cussed.Two algorithms were researched and realized which can be used to create open mine fine DEM model with constrained conditions and to dynamically update the model. The precision analysis and evaluation of the created model were carried out.

Abstract Model Checking for Web Services

Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.