• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Computer and Information Sciences(ISCIS 2004); 20041027-29; Kemer-Antalya(TR) >CSL Model Checking for the GreatSPN Tool
【24h】

CSL Model Checking for the GreatSPN Tool

机译：GreatSPN工具的CSL模型检查

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

摘要

CSL is a stochastic temporal logic that has been defined for continuous time Markov chains, and that allows the checking of whether a single state, or a set of states, satisfies a given probabilistic condition defined over states or over a path of states. In this paper we consider the problem of CSL model checking in the context of Generalized Stochastic Petri Nets. We present a translation from Generalized Stochastic Petri Nets to the input formats of two well-known CSL model checkers, namely ETMCC and PRISM. The transformation to ETMCC is realized at the Markov Chain level, while that to PRISM is defined, as much as possible, at the net level. The translations are applied to a multiserver polling model taken from the literature.
机译：CSL是为连续时间马尔可夫链定义的随机时间逻辑，它允许检查单个状态或一组状态是否满足在状态或状态路径上定义的给定概率条件。在本文中，我们考虑了在广义随机Petri网中CSL模型检查的问题。我们提供了从广义随机Petri网到两种著名的CSL模型检查器（即ETMCC和PRISM）的输入格式的翻译。向ETMCC的转换是在马尔可夫链层次上实现的，而向PRISM的转换则尽可能在网络层次上进行定义。将该翻译应用于从文献中获取的多服务器轮询模型。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号