嵌套谓词等式系与弱互模拟

Nesting Predicate Equation Systems and Weak Bisimulations

带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解．

Symbolic transition graphs with assignment is a general semantical model for value-passing pro-cesses. Strong bisimulation equivalences between such graphs can be reduced t0 the greatest solutions to simplepredicate equation systems. The aim of this paper is to generalise this result to weak bisimulation equivalences.For this purpose, the notion of nesting predicate equation systems is introduced, and algorithms are presentedto reduce weak bisimulation equivalences to the greatest solutions to nesting predicate equation systems of theform E2μE1.