Wait or act : parameterized verification with wait-only protocols and non-blocking communication

Attendre ou agir : vérification paramétrée avec protocoles wait-only et communication non bloquante Cette thèse s'inscrit dans le cadre de la vérification formelle de systèmes distribués / concurrents paramétrés, dans lesquels un nombre non borné de processus identiques exécutent le même programme et qui intéragissent via deux mécanismes de communication : 1) les rendez-vous non bloquants : un processus envoie un message qui est reçu instantanément par un autre processus et si aucun processus n'est prêt à recevoir le message, celui-ci est simplement perdu (mais bien envoyé). 2) les broadcasts : un processus envoie un message reçu simultanément par tous les processus capables de le recevoir. Le programme exécuté par les processus est donné comme une machine à états finis, appelé un protocole. Le nombre de processus n'est pas fixé, et il s'agit donc d'un paramètre du système. Vérifier ces systèmes revient alors à le faire pour tout nombre de processus possible. On obtient alors un nombre infini de systèmes rendant impossible l'utilisation de méthodes classiques de model checking. Dans ce cadre, nous étudions plusieurs problèmes de vérification paramétrée. Chaque problème vise à établir l'existence d'un nombre de processus pour lequel une exécution du système satisfait une propriété donnée : la couverture d'un état (un processus peut-il atteindre un état particulier ?), la couverture d'une configuration (le système peut-il évoluer vers une configuration qui couvre une cible ?), la synchronisation (tous les processus peuvent-ils atteindre un même état simultanément ?), et la couverture répétée (une transition peut-elle être exécutée indéfiniment ?). Nous montrons que les problèmes de couverture d'un état et de configuration sont ExpSpace-complets dans les réseaux où les processus communiquent seulement avec le mécanisme de rendez-vous non-bloquant, améliorant un résultat antérieur qui ne démontrait que la décidabilité. En revanche, le problème de synchronisation est indécidable tout comme le problème de la couverture répétée. Notre contribution principale consiste en l'introduction des protocoles "Wait-Only", une restriction syntaxique où chaque état est soit un état d'attente (ne pouvant effectuer aucune emission de message) soit un état d'action (ne pouvant recevoir aucun message). Cette séparation claire entre états d'action et d'attente permet d'obtenir une propriété fondamentale appelée la « propriété de copier-coller", qui garantit que si un état d'action et un autre état sont séparément couvrables, alors il le sont également ensemble. Pour cette classe de protocoles, nous prouvons que la couverture d'un état est résolvable en temps polynomial, tandis que la couverture de configuration est elle, PSpace-complète. Cela représente une réduction significative de complexité par rapport au cas général (Ackermann-complet et ExpSpace-complet lorsque l'on se restreint aux rendez-vous non-bloquants). En restreignant la communication aux rendez-vous non-bloquants, la couverture de configuration peut être résolue en temps polynomial, avec pour conséquence remarquable que tout état couvrable est soit couvrable par au plus un processus, soit par un nombre arbitraire de processus. Pour les protocoles Wait-Only avec communication par broadcast, nous prouvons que la synchronisation est décidable (mais Ackermann-difficile), tandis que la synchronisation vers un état d'action est ExpSpace-complète et que la couverture répétée est dans ExpSpace. De manière surprenante, la synchronisation dans les protocoles Wait-Only où le seul mécanisme de communication est le rendez-vous non-bloquant, reste indécidable. Enfin, nous introduisons les protocoles "Single Wait-Only", où depuis chaque état d'attente, un unique message peut être reçu. Dans ce cadre, la couverture répétée devient décidable en temps polynomial.