期刊文献+
共找到6篇文章
< 1 >
每页显示 20 50 100
Computation Tree Logic Model Checking of Multi-Agent Systems Based on Fuzzy Epistemic Interpreted Systems
1
作者 Xia Li Zhanyou Ma +3 位作者 Zhibao Mian Ziyuan Liu Ruiqi Huang Nana He 《Computers, Materials & Continua》 SCIE EI 2024年第3期4129-4152,共24页
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 s... 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. 展开更多
关键词 Model checking multi-agent systems fuzzy epistemic interpreted systems fuzzy computation tree logic transformation algorithm
下载PDF
Model Checking Workflow Net Based on Petri Net 被引量:2
2
作者 ZHOU Conghua CHEN Zhenyu 《Wuhan University Journal of Natural Sciences》 CAS 2006年第5期1297-1301,共5页
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 t... 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. 展开更多
关键词 model checking computation tree logic (CTL *) Petri nets WORKFLOW
下载PDF
Automatic Verification of Biochemical Network Using Model Checking Method
3
作者 Jinkyung Kim Younghee Lee Il Moon 《Chinese Journal of Chemical Engineering》 SCIE EI CAS CSCD 2008年第1期90-94,共5页
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 sear... 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. 展开更多
关键词 automatic verification path networks biological process model checking computational tree logic
下载PDF
Aspect-Oriented Design Method for Embedded Systems Based on Timed Statecharts
4
作者 文欣秀 虞慧群 郑红 《China Communications》 SCIE CSCD 2013年第9期33-42,共10页
The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded ... The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded applications,but they do not realise the reasonable separation of system concerns,which would result in code scattering and tangling.Aspect-Oriented Software Development(AOSD)technology could separate crosscutting concerns from core concerns and identify potential problems in the early phase of the software development life cycle.Therefore,the paper proposes aspect-oriented timed statecharts(extended timed statecharts with AOSD)to separately model base functional requirements and other requirements(e.g.,scheduling,error handling),thereby improving the modularity and development efficiency of embedded systems.Furthermore,the dynamic behaviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties(e.g.,liveness,safety)described by computation tree logic formulae.Finally,a given case demonstrates some desired properties processed with respect to the aspect-oriented timed statecharts model. 展开更多
关键词 embedded systems model check-ing timed statecharts computation tree logic
下载PDF
Fair Preorder for Partial Fair Kripke Structures
5
作者 徐蔚文 陆鑫达 《Journal of Shanghai Jiaotong university(Science)》 EI 2003年第1期15-18,共4页
This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of s... This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae. 展开更多
关键词 FAIRNESS Kripke structure computation tree logic(CTL)
下载PDF
Nondeterministic Probabilistic Petri Net -- A New Method to Study Qualitative and Quantitative Behaviors of System 被引量:4
6
作者 Yang Liu Huai-Kou Miao +2 位作者 Hong-Wei Zeng Yan Ma Pan Liu 《Journal of Computer Science & Technology》 SCIE EI CSCD 2013年第1期203-216,共14页
There are many variants of Petri net at present, and some of them can be used to model system with both function and performance specification, such as stochastic Petri net, generalized stochastic Petri net and probab... There are many variants of Petri net at present, and some of them can be used to model system with both function and performance specification, such as stochastic Petri net, generalized stochastic Petri net and probabilistic Petri net. In this paper, we utilize extended Petri net to address the issue of modeling and verifying system with probability and nondeterminism besides function aspects. Using probabilistic Petri net as reference, we propose a new mixed model NPPN (Nondeterministic Probabilistic Petri Net) system, which can model and verify systems with qualitative and quantitative behaviours. Then we develop a kind of process algebra for NPPN system to interpret its algebraic semantics, and an action- based PCTL (Probabilistic Computation Tree Logic) to interpret its logical semantics. Afterwards we present the rules for compositional operation of NPPN system based on NPPN system process algebra, and the model checking algorithm based on the action-based PCTL. In order to put the NPPN system into practice, we develop a friendly and visual tool for modeling, analyzing, simulating, and verifying NPPN system using action-based PCTL. The usefulness and effectiveness of the NPPN system are illustrated by modeling and model checking an elaborate model of travel arrangements workflow. 展开更多
关键词 NONDETERMINISM probabilistic Petri net model checking action-based probabilistic computation tree logic
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部