首页>
外文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.
展开▼