Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2021 | 10.1145/3487212.3487339 | 2021 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE) |
Keywords | DocType | ISBN |
statistical model,hybrid automata-based models,linear model,nonprophetic schedulers,specific signal temporal logic property,optimal decisions,stochastic hybrid system,optimal probability,temporal logic formula,random events,general continuous probability distributions,discrete nondeterministic choices,continuous system,near-optimal scheduler | Conference | 978-1-6654-1449-4 |
Citations | PageRank | References |
0 | 0.34 | 30 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Mathis Niehage | 1 | 1 | 0.69 |
Arnd Hartmanns | 2 | 0 | 0.34 |
Anne Remke | 3 | 175 | 23.96 |