Séance de cours
Cette séance de cours couvre l'analyse formelle des systèmes stochastiques, axée sur les martingales et leurs applications dans les programmes probabilistes, le contrôle stochastique et l'analyse quantitative des terminaisons. Il explore le concept de martingales comme processus stochastiques constant ou décroissant dans l'attente, avec des exemples comme la ruine de Gambler. Le discours se transforme en invariants stochastiques, en supermartingales, et leur rôle dans la certification des probabilités de terminaison. Il examine également l'exhaustivité des invariants stochastiques pour l'analyse quantitative des terminaisons et la synthèse des certificats de terminaison. La séance de cours se termine par une discussion sur la vérification et le contrôle de la stabilité dans les systèmes stochastiques, y compris l'utilisation des supermartingales du réseau neuronal. Les travaux futurs comprennent l'amélioration des algorithmes pour améliorer les limites et le conditionnement.