传值系统的互模拟与谓词等式系

本文引入描述传值并系统的新模型“带赋值符号迁移图（ＳＴＧＡ）”推广了Ｈｅｎｎｅｓｓｙ和Ｌｉｎ提出的“符号迁移图”的概念，允许迁移上带有赋值，从而能将更大的一类传值系统表示为有穷状态图，ＳＴＧＡ的中车优点是在并行运算不封闭，文中给给ＳＴＧＡ的操作语义，在此基础上定义了ＳＴＧＡ的互模拟等价关系，为了刻划ＳＴＧＡ的互模拟，以谓词等式系的形式在一阶逻辑的正子集中扩充了最大和最小不动点，并设计了一个算法将Ｓ

BISIMULATIONS OF VALUE-PASSING SYSTEMS AND PREDICATE EQUATION SYSTEMS

Symbolic transition graphs with assignment (STGA) is introduced as anew model for value-passing concurrent systems. STGA generalizes the notion ofsymbolic transition graphs of Hennessy and Lin by allowing assignments to becarried in transitions. As a consequence, a wider class of processes can be representedas finite state graphs. Another advantage of this generalization is that STGAs areclosed under parallel composition. An operational semantics is given to suchgraphs. On top of the operational semantics, the notion of bisimulation equivalenceis defined. In order to characterize bisimulations between STGAs, the positivesegment of first order logic is extended with maximal and minimal fixpoints by meansof predicate equation systems. An algorithm is presented, which reduces theproblem of checking bisimulations for STGAs to finding the greatest solutions ofpredicate equation systems.