Minimal witnesses for probabilistic timed automata

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

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

OriginalspracheEnglisch
TitelAutomated Technology for Verification and Analysis
Redakteure/-innenDang Van Hung, Oleg Sokolsky
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten501-517
Seitenumfang17
ISBN (Print)978-3-030-59151-9
PublikationsstatusVeröffentlicht - 2020
Peer-Review-StatusNein

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 12302
ISSN0302-9743

Konferenz

Titel18ᵗʰ International Symposium on Automated Technology for Verification
KurztitelATVA 2020
Dauer19 - 23 Oktober 2020
Webseite
BekanntheitsgradInternationale Veranstaltung
Ortonline
StadtHanoi
LandVietnam

Externe IDs

Scopus 85093820930
ORCID /0000-0002-5321-9343/work/142236708

Schlagworte

Schlagwörter

  • Minimal witnesses for probabilistic timed automata

Bibliotheksschlagworte