Deep statistical model checking

DOI10.1007/978-3-030-50086-3_6MaRDI QIDQ5041276zbMATH OpenOpenAlexFDO

Authors Timo P. Gros, Holger Hermanns, J. Hoffmann, Michaela Klauck, Marcel Steinmetz

Publication date 13 October 2022

Published in Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-50086-3_6

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Artificial neural networks and deep learning (68T07) Markov and semi-Markov decision processes (90C40)

Recommendations

• Abstract neural networks
• \textsc{NeVer}: a tool for artificial neural networks verification
• Safety verification of deep neural networks
• Formal specification for deep neural networks
• Reluplex: a calculus for reasoning about deep neural networks

Cites work

• A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play
• A logic for reasoning about time and reliability
• Exact and ordinary lumpability in finite Markov chains
• Explicit model checking of very large MDP using partitioning and secondary storage
• Formal verification of piece-wise linear feed-forward neural networks
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 1905115 (Why is no real title available?)
• Multilayer feedforward networks are universal approximators
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Safety verification of deep neural networks
• Sequential Tests of Statistical Hypotheses
• Some inequalities relating to the partial sum of binomial probabilities
• Stochastic model checking
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• DSMC evaluation stages: fostering robust and safe behavior in deep reinforcement learning -- extended version

Describes a project that uses

Uses Software

• PRISM
• APMC
• Storm
• ImageNet
• Jani
• iscasMc
• AlexNet

This page was built for publication: Deep statistical model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5041276)