Using Probabilistic Kleene Algebra for Protocol Verification
Using Probabilistic Kleene Algebra for Protocol Verification
复制标题
使用概率克林代数进行协议验证
DOI：
10.1007/11828563_20
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Carroll Morgan
中科院分区：
文献类型：
--
作者：
Annabelle McIver;E. Cohen;Carroll Morgan
我们描述了pKA，一个概率Kleene式代数，基于一个众所周知的概率/恶魔计算模型[3，16，10]。我们的技术目标是表达概率版本的科恩分离定理。
分离定理简化了对分布式系统的推理，在纯代数推理的情况下，它们可以将复杂的交织行为减少为“分离”的行为，每个行为都可以单独分析。到目前为止，这对于概率分布式系统来说是不可能的。
代数推理一般来说是非常健壮的，并且容易检查：因此，概率分布式系统的代数方法是有吸引力的，因为在“双重敌对”的环境（概率和交织）中，细微错误的机会比比皆是。特别棘手的是概率和并发所隐含的恶魔或“对抗性”调度的相互作用。
我们的案例研究--基于拉宾的有界等待的互斥--是这样一个问题已经发生的案例：最初的陈述后来被证明有微妙的缺陷。它激发了我们对代数的兴趣，在代数中，与概率和秘密有关的假设被清楚地暴露出来，在某些情况下，尽管它们错综复杂，但可以给出简单的特征。
We describe pKA, a probabilistic Kleene-style algebra, based on a well known model of probabilistic/demonic computation [3,16,10]. Our technical aim is to express probabilistic versions of Cohen's separation theorems.
Separation theorems simplify reasoning about distributed systems, where with purely algebraic reasoning they can reduce complicated interleaving behaviour to “separated” behaviours each of which can be analysed on its own. Until now that has not been possible for probabilistic distributed systems.
Algebraic reasoning in general is very robust, and easy to check: thus an algebraic approach to probabilistic distributed systems is attractive because in that “doubly hostile” environment (probability and interleaving) the opportunities for subtle error abound. Especially tricky is the interaction of probability and the demonic or “adversarial” scheduling implied by concurrency.
Our case study — based on Rabin's Mutual exclusion with bounded waiting — is one where just such problems have already occurred: the original presentation was later shown to have subtle flaws [15]. It motivates our interest in algebras, where assumptions relating probability and secrecy are clearly exposed and, in some cases, can be given simple characterisations in spite of their intricacy.