Carina Da Silva, Stefan Schupp, Anne Remke

Optimizing Reachability Probabilities for a Restricted Class of Stochastic Hybrid Automata via Flowpipe Construction

  • Computer Science Applications
  • Modeling and Simulation
Save to CiteDrive Show PDF

Stochastic hybrid automata (SHA) are a powerful tool to evaluate the dependability and safety of critical infrastructures. However, the resolution of nondeterminism, which is present in many purely hybrid models, is often only implicitly considered in SHA. This article instead proposes algorithms for computing maximum and minimum reachability probabilities for singular automata with urgent transitions and random clocks that follow arbitrary continuous probability distributions. We borrow a well-known approach from hybrid systems reachability analysis, namely flowpipe construction, which is then extended to optimize nondeterminism in the presence of random variables. First, valuations of random clocks that ensure reachability of specific goal states are extracted from the computed flowpipes, and second, reachability probabilities are computed by integrating over these valuations. We compute maximum and minimum probabilities for history-dependent prophetic and non-prophetic schedulers using set-based methods. The implementation featuring the library HyPro and the complexity of the approach are discussed in detail. Two case studies featuring nondeterministic choices show the feasibility of the approach.

Need a simple solution for managing your BibTeX entries? Explore CiteDrive!

  • Web-based, modern reference management
  • Collaborate and share with fellow researchers
  • Integration with Overleaf
  • Comprehensive BibTeX/BibLaTeX support
  • Save articles and websites directly from your browser
  • Search for new articles from a database of tens of millions of references
Try out CiteDrive

More from our Archive