毕业设计（论文）交互进程行为等价性判定算法研究.docVIP

摘 要 在计算机硬件或软件系统中，往往会存在多个相同或同构的组件，对应的模型在结构上会存在对称性，这种对称结构具有相近或相同的性质。因此，采取对称约简可化简冗余的系统设计。 进程代数是刻画并发系统的有效工具。若事件结构具有对称性，意味着存在非平凡的置换群，诱导出一个等价关系，则事件结构互模拟等价于它的商结构，且在动作细化下保持。论文阐述了事件结构的对称约简，讨论交织互模拟等价在动作细化下的保持及对称约简问题。 由进程代数语言，引入进程的对称性。针对事件结构，引用了置换群的对称性，建立商进程与进程之间的互模拟，从而得到进程的互模拟等价关系。进一步讨论，在动作细化下，商进程与进程具有相同的行为特征，也就是说，一个事件结构的格局和它对应的商事件结构的格局在动作细化下是同构的。因此，对称约简不改变等价性在动作细化下的保持。 论文给出论证例子。例子给出商进程和进程的变迁关系图，表明两者之间是行为等价的。再列出交织并发进程等价例子，验证了约简算法的正确性。在计算机硬件或软件系统设计和分析的形式化验证中，对称约简方法已经成为解决组合状态爆炸问题的有效方法之一。 关键词：事件结构；动作细化；交织互模拟；约简算法；互模拟等价 Abstract In computer hardware or software systems, there are multiple identical or homogeneous components, in which corresponding models will exist in the structure symmetry, and this symmetric structure has the similar or the same character. Therefore, the system design of symmetrical reduction is adopted. Process algebra is an effective tool for depicting concurrent systems. If the event structure has a symmetry one that means that the existence of nontrivial permutation group can induce an equivalence relation, then the event structure simulation is equivalent to its quotient structure in the action refinement. The paper expounds the symmetry event structure, where we discuss the maintenance of the interweaving and the reduction of symmetry in the operation. The symmetrical properties of the process are introduced by the process algebraic language. For the structure of events, the symmetry of the permutation group is referenced, where the bi-simulation relation between the two processes is established, thus the inter simulation equivalence of the process is obtained. The process and its quotient process have the same behavior characteristics, that is, an event structure pattern and the pattern of its corresponding quotient event structure is homogeneous under the action refinement, where symmetric reduction does not change the maintenance of equivalence. The paper gives an example of an argument. The example gives a transition diagram o