• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>2011 Eighth International Conference on Quantitative Evaluation of Systems >COSMOS: A Statistical Model Checker for the Hybrid Automata Stochastic Logic
【24h】

COSMOS: A Statistical Model Checker for the Hybrid Automata Stochastic Logic

机译：COSMOS：混合自动机随机逻辑的统计模型检查器

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This tool paper introduces cosmos, a statistical model checker for the Hybrid Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA), to describe relevant execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which includes, but is not limited to, Markov chains. As a result HASL verification turns out to be a unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. COSMOS takes as input a DESP (described in terms of a Generalized Stochastic Petri Net), an LHA and an expression $Z$ representing the quantity to be estimated. It returns a confidence interval estimation of $Z$. COSMOS is written in C++ and is freely available to the research community.
机译：本工具文件介绍了cosmos，这是混合自动机随机逻辑（HASL）的统计模型检查器。 HASL使用线性混合自动机（LHA）（确定性定时自动机（DTA）的概括）来描述离散事件随机过程（DESP）的相关执行路径，该事件是一类随机模型，包括但不限于马尔可夫链。结果，HASL验证成为一个统一的框架，其中复杂的时间推理与精心设计的基于奖励的分析自然融合在一起。 COSMOS将DESP（以广义随机Petri网描述），LHA和表示要估计数量的表达式$ Z $作为输入。它返回$ Z $的置信区间估计。 COSMOS是用C ++编写的，可供研究社区免费使用。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号