Nov 28, 2017: Arnd Hartmanns: Efficient Statistical Model Checking of Probabilistic Timed Automata with Nondeterminism

November 28, 2017Efficient Statistical Model Checking of Probabilistic Timed Automata with Nondeterminism
Room: ?Arnd Hartmanns
12:30-13:30

Probabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a statistical model checking approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this talk, I present a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the Modest Toolset, I show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models. These results are based on joint work with Pedro D'Argenio and Sean Sedwards that will be presented at the Winter Simulation Conference on December 5.