SWITSS：计算小型见证子系统
计算机科学中的逻辑
2020-08-11 v1
摘要
离散马尔可夫模型中概率可达性阈值的小型见证子系统是一个重要概念，既作为属性为何成立的诊断信息，也作为精化算法的输入。我们提出 SWITSS，一种用于计算小型见证子系统（Small WITnessing SubSystems）的工具。SWITSS 实现了基于将问题归约为（混合整数）线性规划的精确与启发式方法。返回的子系统可自动图形化渲染，并附带证明该子系统确为见证的证书。
引用
@article{arxiv.2008.04049,
title = {SWITSS: Computing Small Witnessing Subsystems},
author = {Simon Jantsch and Hans Harder and Florian Funke and Christel Baier},
journal= {arXiv preprint arXiv:2008.04049},
year = {2020}
}
备注
9 pages; accepted for publication in the Proceedings of FMCAD'20 (https://fmcad.org/)