An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs b...An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs by a set of rules at first. Next, the algorithm computes a predicate equation system (PES) from the STGs. This is the key step of the whole algorithm. Finally, the PES is solved and the greatest symbolic solution is got. Correctness of the algorithm is proved and time complexity discussed. It is shown that the worst-case time complexity is exponential.展开更多
This paper proposes a novel method to quantify the error of a nominal normalized right graph symbol （NRGS） for an errors- in-variables （EIV） system corrupted with bounded noise. Following an identification framewo...This paper proposes a novel method to quantify the error of a nominal normalized right graph symbol （NRGS） for an errors- in-variables （EIV） system corrupted with bounded noise. Following an identification framework for estimation of a perturbation model set, a worst-case v-gap error bound for the estimated nominal NRGS can be first determined from a priori and a posteriori information on the underlying EIV system. Then, an NRGS perturbation model set can be derived from a close relation between the v-gap metric of two models and H∞-norm of their NRGSs＇ difference. The obtained NRGS perturbation model set paves the way for robust controller design using an H∞ loop-shaping method because it is a standard form of the well-known NCF （normalized coprime factor） perturbation model set. Finally, a numerical simulation is used to demonstrate the effectiveness of the proposed identification method.展开更多
A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are des...A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.展开更多
基金National Natural Science Foundation of China ( No. 6 98730 32 ) 86 3Hi-Τ ech Project ( 86 3-30 6 -ZT-0 6 -0 2 -2 )
文摘An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs by a set of rules at first. Next, the algorithm computes a predicate equation system (PES) from the STGs. This is the key step of the whole algorithm. Finally, the PES is solved and the greatest symbolic solution is got. Correctness of the algorithm is proved and time complexity discussed. It is shown that the worst-case time complexity is exponential.
基金supported in part by the National Natural Science Foundation of China(Nos.61203119,61304153)the Key Program of Tianjin Natural Science Foundation,China(No.14JCZDJC36300)the Tianjin University of Technology and Education funded project(No.RC14-48)
文摘This paper proposes a novel method to quantify the error of a nominal normalized right graph symbol （NRGS） for an errors- in-variables （EIV） system corrupted with bounded noise. Following an identification framework for estimation of a perturbation model set, a worst-case v-gap error bound for the estimated nominal NRGS can be first determined from a priori and a posteriori information on the underlying EIV system. Then, an NRGS perturbation model set can be derived from a close relation between the v-gap metric of two models and H∞-norm of their NRGSs＇ difference. The obtained NRGS perturbation model set paves the way for robust controller design using an H∞ loop-shaping method because it is a standard form of the well-known NCF （normalized coprime factor） perturbation model set. Finally, a numerical simulation is used to demonstrate the effectiveness of the proposed identification method.
基金Supported by the Intel Strategic CAD Labs, the National Natural Science Foundation of China （Grant No. 60421001）, and the Chinese Academy of Sciences.
文摘A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.
