Sur la terminaison des programmes probabilistes récursifs d’ordre supérieur
Charles Grellois
LIS, LIRICA team, Aix-Marseille Université
http://www.grellois.fr/
Date(s) : 20/06/2019 iCal
11h00 - 12h30
Au cours des vingt dernières années, il y a eu beaucoup de progrès sur le model-checking des programmes probabilistes et des programmes fonctionnels, mais le model-checking des programmes qui sont à la fois fonctionnels et probabilistes n’a pas reçu d’intérêt, alors que de tels programmes commencent à émerger dans des langages de programmation comme Church ou Anglican. Nous avons donc travaillé sur ce problème, et avons introduit les schémas de récursion d’ordre supérieur probabilistes (PHORS) pour modéliser les programmes fonctionnels probabilistes. On peut également voir les PHORS comme des généralisations des chaînes de Markov récursives d’Etessami et de Yannakakis. Nous avons, dans cette première approche, considéré le problème de la terminaison probabiliste, qui équivaut à la question de l’accessibilité probabiliste. Nous avons montré que la question est indécidable dès l’ordre 2. Nous avons donné une caractérisation de la terminaison à l’aide de points fixes, et développé une méthode adéquate (mais peut-être incomplète) pour calculer de façon approximée la probabilité de terminaison d’un PHORS d’ordre 2.
Ce travail a été réalisé par Naoki Kobayashi, Ugo Dal Lago et Charles Grellois.
Catégories
