• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>12th International Conference on CONCUR 2001 - Concurrency Theory, 12th, Aug 20-25, 2001, Aalborg, Denmark >Symbolic Computation of Maximal Probabilistic Reachability
【24h】

Symbolic Computation of Maximal Probabilistic Reachability

机译：最大概率可达性的符号计算

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

摘要

We study the maximal reachability probability problem for infinite-state systems featuring both nondeterministic and probabilistic choice. The problem involves the computation of the maximal probability of reaching a given set of states, and underlies decision procedures for the automatic verification of probabilistic systems. We extend the framework of symbolic transition systems, which equips an infinite-state system with an algebra of symbolic operators on its state space, with a symbolic encoding of probabilistic transitions to obtain a model for an infinite-state probabilistic system called a symbolic probabilistic system. An exact answer to the maximal reachability probability problem for symbolic probabilistic systems is obtained algorithmically via iteration of a refined version of the classical predecessor operation, combined with intersection operations. As in the non-probabilistic case, our state space exploration algorithm is semi-decidable for infinite-state systems. We illustrate our approach with examples of probabilistic timed automata, for which previous approaches to this reachability problem were either based on unnecessarily fine subdivisions of the state space, or which obtained only an upper bound on the exact reachability probability.
机译：我们研究具有不确定性和概率选择的无限状态系统的最大可达概率问题。该问题涉及计算达到给定状态集的最大概率，并为用于概率系统自动验证的决策程序奠定了基础。我们扩展了符号转移系统的框架，该框架为无限状态系统在其状态空间上配备了符号算符的代数，并通过概率转移的符号编码来获得称为符号概率系统的无限状态概率系统的模型。通过符号化经典前任运算的精炼版本并与交集运算相结合，可以通过算法获得符号概率系统的最大可达概率问题的精确答案。与非概率情况一样，我们的状态空间探索算法对于无限状态系统是半确定的。我们以概率定时自动机为例来说明我们的方法，针对该方法的先前可达性问题要么基于状态空间的不必要细分，要么仅获得精确可达性概率的上限。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号