We apply reinforcement learning to approximate the optimal probability that a stochastic hybrid system satisfies a temporal logic formula. We consider systems with (non)linear continuous dynamics, random events following general continuous probability distributions, and discrete nondeterministic choices. We present a discretized view of states to the learner, but simulate the continuous system. Once we have learned a near-optimal scheduler resolving the choices, we use statistical model checking to estimate its probability of satisfying the formula. We implemented the approach using Q-learning in the tools HYPEG and modes, which support Petri net- and hybrid automata-based models, respectively. Via two case studies, we show the feasibility of the approach, and compare its performance and effectiveness to existing analytical techniques for a linear model. We find that our new approach quickly finds near-optimal prophetic as well as non-prophetic schedulers, which maximize or minimize the probability that a specific signal temporal logic property is satisfied.

Hybrid Petri nets with general transitions (HPnGs) provide a formalism for modeling safety-critical systems and evaluating their dependability with means of model checking. HPnGs form a restricted subclass of Stochastic Hybrid Automata and allow discrete, continuous and stochastic variables. Previously, discrete-event simulation and Statistical Model Checking (SMC) have been used to overcome the restrictions of existing analytical approaches, e.g., to a limited number of random variables. Also when simulating, the evolution of continuous variables has been restricted to piecewise-linear trajectories, where derivatives do not change between two events. Here, we extend the modeling formalism, the simulation and SMC approach to variables with a non-linear continuous evolution. The core idea of this extension lies in transforming the input system into a so-called second-order quantized state system. A case study on the Kinetic Battery Model validates our approach by comparing results to those obtained by Matlab.