Discrete-Time Verification and Control for Probabilistic Rectangular Hybrid Automata

Hybrid automata provide a modeling formalism for systems characterized by a combination of discrete and continuous components. Probabilistic rectangular automata generalize the class of rectangular hybrid automata with the possibility of representing random behavior of the discrete components of the system. We consider the following two problems regarding probabilistic rectangular automata: verification concerns the computation of the maximum probability with which the system can satisfy a certain omega-regular specification, control concerns the computation of a strategy which guides certain choices of the system in order to maximize the probability of satisfying a certain omega-regular specification. Our main contribution is to give algorithms for the verification and control problems for probabilistic rectangular automata in a semantics in which discrete control transitions can occur only at integer points in time. Additionally, we give algorithms for verification of omega-regular specifications of probabilistic timed automata, a subclass of probabilistic rectangular automata, with the usual dense-time semantics.