Deep Statistical Model Checking - Formal Techniques for Distributed Objects, Components, and Systems Access content directly
Conference Papers Year : 2020

Deep Statistical Model Checking

Timo P. Gros
  • Function : Author
  • PersonId : 1104894
Holger Hermanns
  • Function : Author
  • PersonId : 915840
Joerg Hoffmann
  • Function : Author
  • PersonId : 932988
Michaela Klauck
  • Function : Author
  • PersonId : 1104895
Marcel Steinmetz

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 serves as a determinizer of the MDP, the result being a Markov chain which as such is amenable to statistical model checking. The combination of a MDP and a NN encoding the action policy is central to what we call “deep statistical model checking” (DSMC). While being a straightforward extension of statistical model checking, it enables to gain deep insight into questions like “how high is the NN-induced safety risk?”, “how good is the NN compared to the optimal policy?” (obtained by model checking the MDP), or “does further training improve the NN?”. We report on an implementation of DSMC inside The Modest Toolset in combination with externally learnt NNs, demonstrating the potential of DSMC on various instances of the model family.
Fichier principal
Vignette du fichier
495615_1_En_6_Chapter.pdf (678.43 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03283238 , version 1 (09-07-2021)

Licence

Attribution

Identifiers

Cite

Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Marcel Steinmetz. Deep Statistical Model Checking. 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.96-114, ⟨10.1007/978-3-030-50086-3_6⟩. ⟨hal-03283238⟩
84 View
6 Download

Altmetric

Share

Gmail Facebook X LinkedIn More