SWITSS: Computing Small Witnessing Subsystems
Logic in Computer Science
2020-08-11 v1
Abstract
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.
Cite
@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}
}
Comments
9 pages; accepted for publication in the Proceedings of FMCAD'20 (https://fmcad.org/)