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.

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.

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.

Generating test case specifications of web service composition using model checking

Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.

Model checking web services choreography in process analysis toolkit

Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view. However, it lacks of a formal semantics and could easily lead to misunderstanding and different implementations. In this paper, the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models. In addition, formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit （PAT）.

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

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

基于Solibri Model Checker的BIM模型质量检查方法探究

BIM模型的正确性与协调一致性是BIM技术应用的基础。本文介绍了关于模型检查工作的基本现状,简述了建筑、结构专业的模型检查的基本内容和方法。主要借助芬兰Solibri公司的模型检查软件Solibri Model Checker(SMC)v8.0对BIM模型质量的检查方法和流程进行了初步探究。

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.

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.

Automatic Verification of Biochemical Network Using Model Checking Method

这研究集中于用模型检查的在生物过程的所有可能的路径的为活动范围能力，转变逻辑和层次结构的方法的自动寻找并且验证。为在在生物过程的复杂、大的网络以内的其他的路径的自动搜索和确认能提供解决方案的可观的数量，它是困难的手工地处理。模型检查是为如果，验证的一个自动方法一个电路或一个条件，表示了为一个并发的转变系统，满足在时间的逻辑表示的一套性质，例如计算的树逻辑(CTL ) 。这篇文章表示模型检查在生物化学的网络确认是可行的，它为在生化法特殊行为的性质查询并且寻找在模拟上显示出某些优点。

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.

Model Checking for Probabilistic Multiagent Systems

In multiagent systems,agents usually do not have complete information of the whole system,which makes the analysis of such systems hard.The incompleteness of information is normally modelled by means of accessibility relations,and the schedulers consistent with such relations are called uniform.In this paper,we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic,which can specify both temporal and epistemic properties.However,the problem is undecidable in general.We show that it becomes decidable when restricted to memoryless uniform schedulers.Then,we present two algorithms for this case:one reduces the model checking problem into a mixed integer non-linear programming(MINLP)problem,which can then be solved by Satisfiability Modulo Theories(SMT)solvers,and the other is an approximate algorithm based on the upper confidence bounds applied to trees(UCT)algorithm,which can return a result whenever queried.These algorithms have been implemented in an existing model checker and then validated on experiments.The experimental results show the efficiency and extendability of these algorithms,and the algorithm based on UCT outperforms the one based on MINLP in most cases.

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.

Bounded Model Checking of CTL＊

Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.

Improved Bounded Model Checking for the Universal Fragment of CTL

SAT-based bounded model checking （BMC） has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic （LTL） formulae and then also adapted to check formulae of the universal fragment of computation tree logic （ACTL） by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an improved BMC approach for ACTL based on Penczek＇s method. We consider two aspects of the approach. One is reduction of the number of variables and transitions in the κ-model by distinguishing the temporal operator EX from the others. The other is simplification of the transformation of formulae by using uniform path encoding instead of a disjunction of all paths needed in the κ-model. With these improvements, for an ACTL formula, the length of the final encoding of the formula in the worst case is reduced. The improved approach is implemented in the tool BMV and is compared with the original one by applying both to two well known examples, mutual exclusion and dining philosophers. The comparison shoves the advantages of the improved approach with respect to the efficiency of 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.

Verifying ReLU Neural Networks from a Model Checking Perspective

Neural networks, as an important computing model, have a wide application in artificial intelligence (AI) domain. From the perspective of computer science, such a computing model requires a formal description of its behaviors, particularly the relation between input and output. In addition, such specifications ought to be verified automatically. ReLU (rectified linear unit) neural networks are intensively used in practice. In this paper, we present ReLU Temporal Logic (ReTL), whose semantics is defined with respect to ReLU neural networks, which could specify value-related properties about the network. We show that the model checking algorithm for theΣ2∪Π2 fragment of ReTL, which can express properties such as output reachability, is decidable in EXPSPACE. We have also implemented our algorithm with a prototype tool, and experimental results demonstrate the feasibility of the presented model checking approach.