SWITSS: Computing Small Witnessing Subsystems
Simon Jantsch, Hans Harder, Florian Funke, Christel Baier
TL;DR
SWITSS is a tool that computes small witnessing subsystems in probabilistic models, aiding diagnostics and refinement through exact and heuristic methods with graphical and certifiable outputs.
Contribution
Introduces SWITSS, a novel tool that efficiently computes small witnessing subsystems using linear programming techniques, with automatic visualization and certification.
Findings
Effective computation of witnessing subsystems demonstrated
Both exact and heuristic approaches implemented
Subsystems are accompanied by verifiable certificates
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNetwork Security and Intrusion Detection · Advanced Malware Detection Techniques · Security and Verification in Computing