SWITSS: Computing Small Witnessing Subsystems
From International Center for Computational Logic
SWITSS: Computing Small Witnessing Subsystems
Simon JantschSimon Jantsch, Hans HarderHans Harder, Florian FunkeFlorian Funke, Christel BaierChristel Baier
Simon Jantsch, Hans Harder, Florian Funke, Christel Baier
SWITSS: Computing Small Witnessing Subsystems
Proc. of 20th Conference on Formal Methods in Computer-Aided Design (FMCAD 2020), 236-244, 2020
SWITSS: Computing Small Witnessing Subsystems
Proc. of 20th Conference on Formal Methods in Computer-Aided Design (FMCAD 2020), 236-244, 2020
- KurzfassungAbstract
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. - Weitere Informationen unter:Further Information: Link
- Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@inproceedings{JHFB2020,
author = {Simon Jantsch and Hans Harder and Florian Funke and Christel
Baier},
title = {SWITSS: Computing Small Witnessing Subsystems},
booktitle = {Proc. of 20th Conference on Formal Methods in Computer-Aided
Design (FMCAD 2020)},
year = {2020},
pages = {236-244},
doi = {10.34727/2020/isbn.978-3-85448-042-6_31}
}