Minimum Reachability Probabilities in Rectangular Automata with Random Clocks

TL;DR

This paper introduces a novel method for computing lower bounds on reachability probabilities in rectangular automata with random clocks, enabling worst-case safety guarantees for cyber-physical systems.

Contribution

It extends existing analysis by providing a way to compute lower bounds, complementing upper bounds, for safety-critical stochastic hybrid systems.

Findings

The method enables worst-case safety analysis for systems modeled by rectangular automata.

Implementation on an electric vehicle charging scenario demonstrates practical feasibility.

Meaningful safety guarantees can be obtained using the proposed approach.

Abstract

Control applications for cyber-physical systems must make reliably safe control decisions in the presence of continuous dynamics as well as stochastic uncertainty. Providing safety guarantees for such systems requires formal modeling and analysis techniques that capture these aspects. For modeling, in this paper we consider rectangular automata with random clocks under prophetic scheduling. For this model class, existing methods can compute only upper bounds on reachability probabilities, enabling optimistic, best-case safety reasoning. We complement this view by introducing a novel method to compute lower bounds, thereby enabling worst-case analysis that is essential for safety-critical applications. Although both upper and lower bounds rely on reachability analysis, they are not dual: computing lower bounds requires an explicit separation of stochastic and nondeterministic choices along executions. We implement our approach and demonstrate its practical feasibility on an electric vehicle charging scenario, showing that meaningful worst-case guarantees can be obtained.