Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks

arXiv (Cornell University)

Abstract

This paper proposes an algorithm to maximize reachability probabilities for rectangular automata with random clocks via a history-dependent prophetic scheduler. This model class incorporates time-induced nondeterminism on discrete behavior and nondeterminism in the dynamic behavior. After computing reachable state sets via a forward flowpipe construction, we use backward refinement to compute maximum reachability probabilities. The feasibility of the presented approach is illustrated on a scalable model.

Authors 4

1. Joanna Delicaris
2. Stefan Schupp
3. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

4. Anne Remke