有限概率过程检验前序的刻画

有限概率演算的检验前序的特征

Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus

我们考虑两个特征的可能性和必须测试前序的概率扩展的有限π演算：一个基于概率弱模拟的概念，和其他的概率扩展的一个片段的米尔纳-帕罗-沃克模态逻辑的π演算。我们基于我们的概念，模拟在以前的工作中使用的概率CSP类似的概念。然而，与CSP（或其他非值传递演算）的情况不同，概率π演算有几种可能的模拟定义，它们来自于不同的量化方法。我们表明，为了捕捉测试前序，需要使用“最早”的模拟关系（类比早期（双）模拟的概念在非概率的情况下）。这两个特征化的关键思想是概率过程的“特征公式”的概念，以及公式的“特征检验”的概念。在早期的工作测试等价性的π演算Boreale和德尼古拉，我们扩展的语言的$π$演算与不匹配的运营商，没有制定的特征测试将是不可能的。

概率过程的逻辑刻画

Characterising Probabilistic Processes Logically

在本文中，我们的工作表现出不确定性和概率行为的过程（双）模拟语义。我们提出了一个概率扩展的模态μ演算，并展示了如何推导出各种模拟的前序无发散的有限状态过程的特征公式。此外，我们表明，即使没有不动点算子，这种概率μ演算可以用来描述这些行为关系的意义上说，两个国家是等价的，当且仅当它们满足相同的公式集。

概率无线网络建模

Modelling Probabilistic Wireless Networks

我们提出了一个过程演算来模拟高层次的无线系统，网络的拓扑结构描述的有向图。演算享有的功能是适当的无线网络，即广播通信和概率行为。我们首先专注于组成无线网络的问题，然后我们提出了一个组合理论的基础上概率概括的著名的可能测试和必须测试前订单。此外，我们定义了一个扩展的语义，我们的演算，这将被用来定义无线网络的模拟和死锁模拟前序。我们证明，我们的模拟前序是健全的，相对于可能的测试前序，同样，死锁模拟前序是健全的，相对于必须测试前序，为一大类网络。我们还提供了一个反例表明，完整的模拟前序，相对于5月测试一，不成立。最后，我们的理论概率路由协议的应用文件。

概率过程的真实回报检验（扩展摘要）

Real-Reward Testing for Probabilistic Processes (Extended Abstract)

通过扩展传统的负回报非负回报测试，我们引入了概率过程实值回报测试的概念。在这个更丰富的测试框架中，may和must前序变成了逆序。我们发现，收敛过程的许多状态和过渡，但不是在发散的存在下，真正的回报必须测试前序与非负回报必须测试前序一致。为了证明这种巧合，我们在流程的弱转换方面对通常的基于分辨率的测试进行了改进，而不必涉及策略、对手、代理人、分辨率或正在调查的流程外部的类似结构。这需要建立我们计算测试结果的功能的连续性。

Characterising Probabilistic Alternating Simulation for Concurrent Games

Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the behaviour of different probabilistic game structures. In this paper, we present a sound and complete modal characterisation of this simulation relation by proposing a new logic based on probabilistic distributions. The logic enables a player to enforce a property in the next state or distribution. Its extension with fixpoints, which also charact…

概率互模拟的逻辑、度量和数学特征

Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation

概率过程的许多行为等价或前序都涉及提升操作，该操作将状态关系转换为状态分布关系。我们表明，现有的几个建议，提升关系可以调和到本质上相同的提升操作的不同介绍。更有趣的是，这种提升操作很好地对应于康托洛维奇度量，这是数学中用于将状态度量提升为状态分布度量的基本概念，此外，提升操作与优化理论中的最大流问题有关。提升操作产生了一个整洁的概念，概率互模拟，我们提供逻辑，度量和算法特征。具体来说，我们扩展了Hennessy-Milner逻辑和模态μ演算与一个新的模态，从而在一个足够的概率双相似性和表达逻辑，分别。提升操作和Kantorovich度量的对应关系导致了互模拟作为伪度量的自然特征，伪度量是单调函数的后不动点。我们还提出了一个“在飞”算法来检查是否在有限系统中的两个状态相关的概率双相似性，利用提升操作和最大流问题之间的密切关系。