基于可聚类的强随机互模拟与弱随机互模拟及其同余性质的分类法

中文摘要 AI 辅助

我们研究了在PEPA（性能评估过程代数）上，根据连续时间马尔可夫链（CTMC）的底层过程项所定义的可聚类性（lumpability）概念，所定义的各种随机互模拟风格等价关系之间的关系。可聚类性是分析CTMC的核心工具，因为它导致状态空间的聚合，这些聚合具有的性质有助于高效计算原始链的状态概率分布。在过程项层面，可以在PEPA上定义各种考虑活动类型和累积速率的随机互模拟，它们诱导不同类型的聚类。由于其中一些形式化定义分散在文献中，并以不同且有时冲突的名称出现，我们将它们收集在一个统一的框架中，根据其诱导的聚类类型一致地重命名每个互模拟。我们提出了我们称之为普通、精确和严格互模拟的强变体和弱变体，并表明它们分别诱导普通、精确和严格聚类。然后，我们将这六种互模拟组织成一个分类法，建立它们之间所有且仅有的包含关系。我们还分析了分类法在三种特殊情况下的变化：底层CTMC是时间可逆的过程项、没有不可观察类型活动的过程项以及没有递归的过程项。论文最后研究了这六种互模拟的组合性质。其中一些相对于PEPA的前缀和/或选择算子不是同余。在这种情况下，我们要么找出一个过程项集合，在该集合上相对于这些算子实现同余，要么找出相对于它们包含在所考虑的互模拟中的最粗同余。

英文摘要

We study the relationships among the stochastic bisimulation-style equivalences over PEPA - Performance Evaluation Process Algebra definable according to the well known notions of lumpability for the continuous-time Markov chains (CTMCs) underlying process terms. Lumpability is a central tool in the analysis of a CTMC, because it results in aggregations of the state space enjoying properties that are useful for efficiently computing the state probability distribution of the original chain. At the level of process terms, various stochastic bisimilarities accounting for activity types and cumulative rates can be defined over PEPA, which induce different kinds of lumping. Since the formalisations of some of them are scattered across the literature, where they appear under different, and sometimes clashing, names, we collect them within a single, uniform framework, renaming each bisimilarity in a consistent way after the kind of lumping it induces. We present strong and weak variants of what we call ordinary, exact, and strict bisimilarities and show that they respectively induce ordinary, exact, and strict lumpings. We then organise the six bisimilarities into a taxonomy establishing all and only the inclusions holding among them. We also analyse how the taxonomy changes in three special cases: process terms whose underlying CTMCs are time reversible, process terms with no activities of unobservable types, and process terms with no recursion. The paper concludes by investigating the compositionality properties of the six bisimilarities. Some of them are not congruences with respect to the prefix and/or choice operators of PEPA. In that case we single out either a set of process terms over which congruence with respect to those operators is achieved, or the coarsest congruence with respect to them that is contained in the considered bisimilarity.

发表机构

• Università di Udine（乌迪内大学）
• Università di Napoli Federico II（那不勒斯费德里科二世大学）
• Università di Urbino（乌尔比诺大学）
• Università Ca’ Foscari, Venezia（威尼斯卡福斯卡里大学）

机构由 AI 辅助整理，请以论文原文为准。