离散马尔可夫模型中概率可达阈值的见证子系统是一个重要的概念，既是关于属性为什么成立的诊断信息，也是算法输入的细化。我们提出了 SWITSS，一个计算小见证子系统的工具。在将问题简化为(混合整数)线性规划的基础上，SWITSS实现了精确的启发式方法。返回的子系统可以自动以图形方式呈现，并附带证明子系统确实是见证人的证书。
原文题目：SWITSS: Computing Small Witnessing Subsystems
原文：Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear programming. Returned subsystems can automatically be rendered graphically and are accompanied with a certificate which proves that the subsystem is indeed a witness.
原文作者: Simon Jantsch, Hans Harder, Florian Funke, Christel Baier
原文地址：https://arxiv.org/abs/2008.04049
SWITSS- 小型见证子系统的计算(cs.LO).pdf