Towards Automated Proof Support for Probabilistic Distributed Systems
Towards Automated Proof Support for Probabilistic Distributed Systems
复制标题
为概率分布式系统提供自动证明支持
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Tjark Weber
中科院分区：
文献类型：
--
作者：
Annabelle McIver;Tjark Weber
概率系统证明的机械化特别具有挑战性，因为要验证概率所带来的实值属性：经验表明[12,4,11]，在其他程序功能的背景下实现实数运算的自动化存在许多困难。
在本文中，我们提出了一种基于 Kleene 代数推广的概率分布式系统验证框架，该框架已被用作标准编程中并发控制开发的基础 [7]。我们表明，这些系统中实值属性的验证可以大大简化，而且尽管存在底层实数域，但存在一种易于通过状态探索进行反例搜索的解释。
The mechanisation of proofs for probabilistic systems is particularly challenging due to the verification of real-valued properties that probability entails: experience indicates [12,4,11] that there are many difficulties in automating real-number arithmetic in the context of other program features.
In this paper we propose a framework for verification of probabilistic distributed systems based on the generalisation of Kleene algebra with tests that has been used as a basis for development of concurrency control in standard programming [7]. We show that verification of real-valued properties in these systems can be considerably simplified, and moreover that there is an interpretation which is susceptible to counterexample search via state exploration, despite the underlying real-number domain.