首页> 外文OA文献 >CSL Model Checking Algorithms for Infinite-state Structured Markov chains
【2h】

CSL Model Checking Algorithms for Infinite-state Structured Markov chains

机译:无限状态结构马尔可夫链的CSL模型检查算法

摘要

Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov chain (CTMC) that underlies such a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues. We present CSL model checking algorithms for labeled JQNs. To do so, we rely on well-known product-form results for the steady-state probabilities in (stable) JQNs. The transient probabilities are computed using an uniformization-based approach. We develop a new notion of property independence that allows us to define model checking algorithms for labeled JQNs.
机译:杰克逊排队网络(JQN)是一类非常通用的排队网络,可以在各种设置中找到其应用。构成此类JQN的连续时间马尔可夫链(CTMC)的状态空间是高度结构化的,但是其大小无限大,与队列一样多。我们提出用于标记JQN的CSL模型检查算法。为此,我们依靠众所周知的乘积形式结果来确定(稳定)JQN中的稳态概率。使用基于均匀化的方法来计算瞬态概率。我们开发了一种新的属性独立性概念,该概念使我们能够为带标签的JQN定义模型检查算法。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号