Analysing and Comparing Encodability Criteria for Process Calculi
Analysing and Comparing Encodability Criteria for Process Calculi
复制标题
DOI：
10.4204/eptcs.190.4
复制
发表时间：
2015-08
期刊：
影响因子：
--
通讯作者：
Kirstin Peters;R. V. Glabbeek
中科院分区：
文献类型：
--
作者：
Kirstin Peters;R. V. Glabbeek
编码或证明其不存在是比较过程演算的主要方法。为了分析编码的质量，并排除琐碎或无意义的编码，它们被增加了质量标准。为了在不同的环境中进行推理，存在着一系列不同的标准和标准的不同变体。这导致了无与伦比的结果。此外，并不总是清楚在特定环境下取得结果所使用的标准是否确实适合这种环境。我们展示了如何正式的原因和比较编码标准，通过映射它们的要求源和目标之间的关系，诱导的编码功能。特别是，我们分析的共同标准充分抽象，操作对应，发散反射，成功的敏感性，并尊重倒钩;例如，我们分析的确切性质的模拟关系（耦合模拟与互模拟），这是由不同的变种操作对应。通过这种方式，我们将分析或比较可编码性标准的问题减少到更好地理解比较进程关系的问题。
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are augmented with quality criteria. There exists a bunch of different criteria and different variants of criteria in order to reason in different settings. This leads to incomparable results. Moreover it is not always clear whether the criteria used to obtain a result in a particular setting do indeed fit to this setting. We show how to formally reason about and compare encodability criteria by mapping them on requirements on a relation between source and target terms that is induced by the encoding function. In particular we analyse the common criteria full abstraction, operational correspondence, divergence reflection, success sensitiveness, and respect of barbs; e.g. we analyse the exact nature of the simulation relation (coupled simulation versus bisimulation) that is induced by different variants of operational correspondence. This way we reduce the problem of analysing or comparing encodability criteria to the better understood problem of comparing relations on processes.