非对称_(χ-)演算的符号互模拟验证算法  

Algorithm for the Verification of Symbolic Bisimulations In Asymmetric Chi-Calculus

作　　者：黄银强[1] 钟发荣[1] 

机构地区：[1]浙江师范大学数理与信息工程学院,浙江金华321004

出　　处：《微电子学与计算机》2006年第9期193-196,共4页Microelectronics & Computer

基　　金：浙江省自然科学基金项目(Y105272)

摘　　要：非对称χ-演算是一种移动计算模型。文介绍非对称χ-演算的语法和符号操作语义,给出非对称χ-演算的符号互模拟的验证算法,该算法根据算法输出的谓词等式系,求解最大符号解。并证明算法正确性,这在一定程度上为今后的自动机验证提供了理论基础。The asymmetric Chi-calculus is a mobile computing model. This paper introduces the syntax and the symbolic operational semantics of the asymmetric Chi-calculus. Then the algorithm for the verification of symbolic bisimulations is presented which computes bisimulations for finite state symbolic transition graphs, by the greatest solutions of predicate equation systems. And the correctness of this algorithm is also given.

关 键 词：进程代数 非对称X-演算 符号互模拟 符号迁移图 验证算法 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]