Deep statistical model checking

Abstract

Neural networks (NN) are taking over ever more decisions thus far taken by humans, even though verifiable system-level guarantees are far out of reach. Neither is the verification technology available, nor is it even understood what a formal, meaningful, extensible, and scalable testbed might look like for such a technology. The present paper is a modest attempt to improve on both the above aspects. We present a family of formal models that contain basic features of automated decision making contexts and which can be extended with further orthogonal features, ultimately encompassing the scope of autonomous driving. Due to the possibility to model random noise in the decision actuation, each model instance induces a Markov decision process (MDP) as verification object. The NN in this context has the duty to actuate (near-optimal) decisions. From the verification perspective, the externally learnt NN …

@inproceedings{grosDeepStatisticalModelChecking2020,
 author = {Timo P. Gros and Holger Hermanns and Jörg Hoffmann and Michaela Klauck and Marcel Steinmetz},
 booktitle = {Formal Techniques for Distributed Objects, Components, and Systems: 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta. Distributed Applications and Interoperable Systems: IFIP WG 6.1 International Conference (DAIS-2020), located at 5th International Federated Conference on Distributed Computing Techniques, June 15-19, Valetta, Malta},
 doi = {10.1007/978-3-030-50086-3_6},
 month = {6},
 organization = {Springer International Publishing},
 pages = {96-114},
 publisher = {Springer International Publishing},
 title = {Deep statistical model checking},
 year = {2020}
}