Minimal witnesses for probabilistic timed automata

Simon JantschSimon Jantsch, Florian FunkeFlorian Funke, Christel BaierChristel Baier

DOI Link

Simon Jantsch, Florian Funke, Christel Baier
Minimal witnesses for probabilistic timed automata
Automated Technology for Verification and Analysis (ATVA), volume 12302 of Lecture Notes in Computer Science, 501--517, 2020. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-59152-6_28.

@inproceedings{JFB2020,
  author    = {Simon Jantsch and Florian Funke and Christel Baier},
  title     = {Minimal witnesses for probabilistic timed automata},
  booktitle = {Automated Technology for Verification and Analysis (ATVA)},
  series    = {Lecture Notes in Computer Science},
  volume    = {12302},
  publisher = {Springer},
  year      = {2020},
  pages     = {501--517},
  doi       = {10.1007/978-3-030-59152-6_28}
}