Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks

2023/04/28 by Delicaris, Joanna, Schupp, Stefan, Ábrahám, Erika +1 · 2 citations
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)

paper · doi:10.48550/arxiv.2304.14996

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.

Cited by

• Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
• Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata

Related

• Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
• Probabilistic Timed Automata with Clock-Dependent Probabilities
• Backwards Reachability for Probabilistic Timed Automata: A Replication Report
• Unknown Biases and Timing Constraints in Timed Automata
• A Hierarchy of Scheduler Classes for Stochastic Automata