SWITSS: Computing small witnessing subsystems

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributed

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.

Details

Original languageEnglish
Title of host publicationProceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020
EditorsAlexander Ivrii, Ofer Strichman
PublisherTU Wien Academic Press
Pages236-244
Number of pages9
ISBN (print)978-3-85448-042-6
Publication statusPublished - 2020
Peer-reviewedNo

Conference

TitleFormal Methods in Computer-Aided Design 2020
Abbreviated titleFMCAD 2020
Duration21 - 24 September 2020
Website
Degree of recognitionInternational event
Locationonline

External IDs

ORCID /0000-0002-5321-9343/work/142236704
Bibtex jantsch+harder++2020_switss
Scopus 85099178494

Keywords

Keywords

  • computer-aided system design