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

非对称χ-演算是一种移动计算模型。文介绍非对称χ-演算的语法和符号操作语义,给出非对称χ-演算的符号互模拟的验证算法,该算法根据算法输出的谓词等式系,求解最大符号解。并证明算法正确性,这在一定程度上为今后的自动机验证提供了理论基础。

数据传送进程的符号互模拟

本文提出数据传送进程的符号迁移语义，引入符号互模拟的概念，证明了两个进程在传统意义下互模拟当且仅当它们符号互模拟。我穷域上的数据传送进程的传统迁移图是无穷的而其中相当的一部分的符号迁移图是有穷的，文章的结果为在有穷时间和空间内判定这类进程的互模拟关系开辟了可能性。

一种自动验证网络安全协议的互模拟方法

为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为"符号化"的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi演算设计了符号互模拟关系—符号Reded互模拟.结果表明:该符号互模拟关系对传统的互模拟关系是可靠的,符号化的标号转移语义将进程无穷输入导致的迁移限期为有穷种迁移.因此使得基于该关系的安全协议自动验证算法得以实现.