COMICS工具——计算离散时间马尔可夫链的最小反例
软件工程
2015-03-20 v1
摘要
本报告介绍了工具COMICS，它执行模型检验并为离散时间马尔可夫链（DTMC）生成反例。对于输入的DTMC，COMICS计算一个携带模型检验信息的抽象系统，并利用该结果计算一个关键子系统，从而导出反例。该抽象子系统可以分层精化并具体化。该工具提供命令行版本以及图形用户界面，允许用户交互式地影响反例的精化过程。
引用
@article{arxiv.1206.0603,
title = {The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains},
author = {Nils Jansen and Erika Ábrahám and Maik Scheffler and Matthias Volk and Andreas Vorpahl and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
journal= {arXiv preprint arXiv:1206.0603},
year = {2015}
}