论文标题
SWITS：计算小型见证子系统
SWITSS: Computing Small Witnessing Subsystems
论文作者
论文摘要
在离散的马尔可夫模型中见证概率可达到性阈值的子系统既是关于财产为什么拥有的诊断信息，又是对改进算法的投入的重要概念。我们提出SWITS，这是计算小型见证子系统的工具。 SWITS基于将问题简化为（混合整数）线性编程的精确和启发式方法。返回的子系统可以自动以图形方式渲染，并伴有证书，证明子系统确实是证人。
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.
