Conference Paper: Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks

I am happy to announce that our approach on the computation of maximal probabilities for rectangular automata extended by random clocks (Delicaris et al.) has been accepted for publication at TASE’23.

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.

References

1. Delicaris, Joanna, et al. “Maximizing Reachability Probabilities In Rectangular Automata with Random Clocks.” 17th International Symposium on Theoretical Aspects of Software Engineering, 2023.accepted for publication
   

   @inproceedings{delicarisRectangularRandomClocks2023,
     title = {Maximizing Reachability Probabilities in
     Rectangular Automata with Random Clocks},
     booktitle = {17th International Symposium on Theoretical Aspects of Software Engineering},
     author = {Delicaris, Joanna and Schupp, Stefan and Ábrahám, Erika and Remke, Anne},
     year = {2023},
     note = {accepted for publication}
   }