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.展开更多
A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiat...A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.展开更多
In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is ove...In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equivalence classes instead of the unitdelay time equivalence classes restricted by event sequence, and avoids generating the equivalence classes of states only due to the passage of time. The result shows that this algorithm ischeaper.展开更多
文摘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.
基金Supported by the Natural Science Foundation of Guizhou Province(No.20050119)the Natural Science Foundation of Guizhou Education(No.2004219)
文摘A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.
文摘In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equivalence classes instead of the unitdelay time equivalence classes restricted by event sequence, and avoids generating the equivalence classes of states only due to the passage of time. The result shows that this algorithm ischeaper.
