Minimal witnesses for probabilistic timed automata
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen
Beitragende
Abstract
Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity.
Details
Originalsprache | Englisch |
---|---|
Titel | Automated Technology for Verification and Analysis |
Redakteure/-innen | Dang Van Hung, Oleg Sokolsky |
Herausgeber (Verlag) | Springer, Berlin [u. a.] |
Seiten | 501-517 |
Seitenumfang | 17 |
ISBN (Print) | 978-3-030-59151-9 |
Publikationsstatus | Veröffentlicht - 2020 |
Peer-Review-Status | Nein |
Publikationsreihe
Reihe | Lecture Notes in Computer Science, Volume 12302 |
---|---|
ISSN | 0302-9743 |
Konferenz
Titel | 18ᵗʰ International Symposium on Automated Technology for Verification |
---|---|
Kurztitel | ATVA 2020 |
Dauer | 19 - 23 Oktober 2020 |
Webseite | |
Bekanntheitsgrad | Internationale Veranstaltung |
Ort | online |
Stadt | Hanoi |
Land | Vietnam |
Externe IDs
Scopus | 85093820930 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236708 |
Schlagworte
Schlagwörter
- Minimal witnesses for probabilistic timed automata