Automates Buchi dans la vérification formelle de logiciels

Question

Alors que j'étudie l'application des automates de Buchi à la vérification formelle de logiciels, je m'intéresse à la complexité informatique (ou aux liens vers des articles) des algorithmes utilisés pour résoudre le problème dans la pratique.

Permettez-moi de rappeler l'intuition mathématique derrière la vérification de modèles utilisant ces techniques.Les automates Buchi sont les automates associés à $\oméga$-langues régulières.Vous pouvez considérer ces langages comme la version infinie des langages réguliers (infinis dans le sens où ils opèrent sur des mots infinis).En tant que langages réguliers, ils bénéficient de propriétés de fermeture sous composition et intersection.Il est également bien connu que ces Automates sont « isomorphes » à la proposition d'une logique appelée S1S.C'est la logique de la logique monadique du second ordre (c'est-à-direvous pouvez avoir une quantification sur les prédicats de la logique, mais les éléments peuvent s'étendre sur un ensemble fini).S1S a la belle propriété d'être décidable, c'est-à-direpour chaque préposition, nous pouvons dire si elle est vraie ou non.Pour savoir si une formule S1S est satisfiable, nous pouvons déterminer si les atomes associés ont un état acceptant.Dans les automates Buchi, cela se fait en trouvant des cycles entre l’état de départ et tout état final.

Pour trouver un "bug" dans un logiciel on procède ainsi :

• nous formalisons notre logiciel comme $\mathbb{S}$ en utilisant une logique S1S (une logique monaïdique du second ordre).
• nous formalisons les propriétés de sécurité de notre logiciel dans la logique $\mathbb{P}$
• maintenant nous utilisons les propriétés de proximité de $\oméga$-des langages, dont les automates associés sont équivalents à la logique S1S :nous construisons des automates Buchi de $\overline{\mathbb{S}} \cap \mathbb{P}$

De cette façon, si le logiciel ne fait pas respectent les propriétés de sécurité, les automates résultants auront au moins un État acceptant.En pratique, l’état acceptant d’un automate Buchi peut être trouvé en trouvant un cycle dans le graphe associé entre l’état de départ et n'importe lequel état final.

Je soupçonne en pratique un algorithme pour détection de cycle Ne peut pas être utilisé.Cela est dû à la contrainte selon laquelle le cycle doit passer du seul état de départ et passer par un état d'acceptation, de sorte que la probabilité de trouver le cycle dont vous avez besoin peut être très faible.Quoi qu'il en soit, le meilleur algorithme de détection de cycle est résolu par le Algorithme de Johnson à l'heure $O((n + e)(c + 1))$ et l'espace délimité par $O(n + e)$).

En pratique, il serait peut-être préférable de résoudre la décidabilité S1S à l'aide d'automates de Buchi avec la connectivité st.Par exemple, NetworkX résout la connectivité avec ce Algorithme par Abdol-Hossein Esfahanian.

Ai-je raison?

Quel algorithme de graphe est utilisé en pratique pour résoudre la satisfiabilité S1S à l'aide d'automates de Buchi ?

j'ai trouvé ce, mais il montre simplement une meilleure réduction de S1S à Buchi, et il ne parle pas de graphiques.