Minimal witnesses for probabilistic timed automata

TL;DR

This paper introduces a new approach for identifying minimal witnessing subsystems in probabilistic timed automata, aiding in system analysis and refinement by translating bisimulation certificates into useful diagnostic components.

Contribution

It presents novel algorithms for computing minimal witnessing subsystems in PTA using a new operation on difference bounds matrices, with multiple notions of minimality and complexity analysis.

Findings

Algorithms for minimal witnessing subsystems are developed and analyzed.

Farkas certificates can be translated into witnessing subsystems.

Multiple notions of minimality are considered for different perspectives.

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.