基于Open pNets的组成等价
Compositional equivalences based on Open pNets
摘要：
建立程序或系统之间的等价关系对于验证程序的正确性（通过建立两个实现是等价的）和证明优化和程序转换（通过建立修改后的程序与源程序等价）都是至关重要的。程序存在几种等价关系，互模拟是这些等价关系中最通用的。在互模拟关系中，我们可以区分强互模拟和弱互模拟，强互模拟要求程序的每个动作都由等价程序的单个动作模拟，弱互模拟是一种粗糙的关系，允许某些动作是不可见的或内部移动的，因此不被等价程序模拟。pNet是对开放系统进行建模的自动机的概括。它们以变量和层次结构为特征。开放式pNet是具有洞的pNet，即层次结构内的占位符，稍后可以由子系统填充。本文定义了互模拟关系，用于比较指定为pNet的系统。我们首先定义了一个强互模拟开放pNet。然后，我们定义了一个类似于经典的弱互模拟的等价关系，并研究了它的性质。在这些性质中，我们感兴趣的是组合性：如果两个系统被证明是等价的，那么它们将无法通过它们的上下文来区分，并且当它们的洞被等价系统填充时，它们也将无法区分。我们确定充分条件的自动机，以确保组合的强和弱互模拟。文章用一个传输协议运行的例子来说明，它显示了我们的形式主义和我们的互模拟关系的特点。
英文摘要：
Establishing equivalences between programs or systems is crucial both for verifying correctness of programs, by establishing that two implementations are equivalent, and for justifying optimisations and program transformations, by establishing that a modified program is equivalent to the source one. There exist several equivalence relations for programs, and bisimulations are among the most versatile of these equivalences. Among bisimulation relations one distinguishes strong bisimulation, that requires that each action of a program is simulated by a single action of the equivalent program, a weak bisimulation that is a coarser relation, allowing some of the actions to be invisible or internal moves, and thus not simulated by the equivalent program. pNet is a generalisation of automata that model open systems. They feature variables and hierarchical composition. Open pNets are pNets with holes, i.e. placeholders inside the hierarchical structure that can be filled later by sub-systems. This article defines bisimulation relations for the comparison of systems specified as pNets. We first define a strong bisimulation for open pNets. We then define an equivalence relation similar to the classical weak bisimulation, and study its properties. Among these properties we are interested in compositionality: if two systems are proven equivalent they will be undistinguishable by their context, and they will also be undistinguishable when their holes are filled with equivalent systems. We identify sufficient conditions on the automata to ensure compositionality of strong and weak bisimulation. The article is illustrated with a transport protocol running example; it shows the characteristics of our formalism and our bisimulation relations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
