SWITSS: Computing small witnessing subsystems

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragen

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

OriginalspracheEnglisch
TitelProceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020
Redakteure/-innenAlexander Ivrii, Ofer Strichman
Herausgeber (Verlag)TU Wien Academic Press
Seiten236-244
Seitenumfang9
ISBN (Print)978-3-85448-042-6
PublikationsstatusVeröffentlicht - 2020
Peer-Review-StatusNein

Konferenz

TitelFormal Methods in Computer-Aided Design 2020
KurztitelFMCAD 2020
Dauer21 - 24 September 2020
Webseite
BekanntheitsgradInternationale Veranstaltung
Ortonline

Externe IDs

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

Schlagworte

Schlagwörter

  • computer-aided system design