Minimal witnesses for probabilistic timed automata

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

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

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
EditorsDang Van Hung, Oleg Sokolsky
PublisherSpringer, Berlin [u. a.]
Pages501-517
Number of pages17
ISBN (print)978-3-030-59151-9
Publication statusPublished - 2020
Peer-reviewedNo

Publication series

SeriesLecture Notes in Computer Science, Volume 12302
ISSN0302-9743

Conference

Title18ᵗʰ International Symposium on Automated Technology for Verification
Abbreviated titleATVA 2020
Duration19 - 23 October 2020
Website
Degree of recognitionInternational event
Locationonline
CityHanoi
CountryViet Nam

External IDs

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

Keywords

Keywords

  • Minimal witnesses for probabilistic timed automata

Library keywords