• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Integrated formal methods >On Model Checking Techniques for Randomized Distributed Systems
【24h】

On Model Checking Techniques for Randomized Distributed Systems

机译：随机分布式系统模型检查技术研究

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an w-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the "worst-case" is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account. The worst-case analysis relying on this general notion of schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partial-information schedulers yield more realistic worst-case probabilities, but computationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers.
机译：随机分布式系统的基于自动机的模型检查方法依赖于系统的可操作交织语义，借助马尔可夫决策过程以及所需事件E的形式化通过w规则线性时间属性（例如LTL公式） 。然后的任务是计算即使在最坏的情况下也可以保证的E概率的最大下限。可以通过将多项式时限图算法与求解线性程序的方法相结合来计算此类边界。在经典方法中，当遍历所有决定下一步执行哪个调度程序的调度程序时，将确定“最坏情况”。特别地，考虑了系统模型中所有其他不确定性选择的可能的交织和解析。依赖于调度程序这一一般概念的最坏情况分析通常过于悲观，并导致只能通过对于并行系统不切实际的调度程序才能获得的极端概率值。这促使人们转向更现实的调度程序类，这些调度程序尊重各个进程仅具有有关全局系统状态的部分信息这一事实。这种类型的部分信息调度程序会产生更现实的最坏情况概率，但在计算上却更加困难。当目标是检查所有部分信息调度程序下是否存在某些概率界限时，各种各样的验证问题就变得不可确定。

著录项

  • 来源
    《Integrated formal methods》|2010年|p.1-11|共11页
  • 会议地点 Nancy(FR);Nancy(FR)
  • 作者

    Christel Baier;

  • 作者单位

    Technische Universitat Dresden, Faculty of Computer Science, Germany;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 理论、方法;
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号