Réduction d'ordre partiel statique sur un espace d'état donné

Question

La plupart des articles sur la réduction d'ordre partiel supposent que le système à analyser est donné comme un ensemble de processus avec un opérateur de composition. Cela a beaucoup de sens, puisque vous ne voulez pas d'abord calculer l'espace d'état, puis le réduire en utilisant la réduction d'ordre partiel. Mais, en supposant que vous ayez déjà donné un espace d'état plat, pouvez-vous encore le réduire en utilisant la réduction d'ordre partiel? Je pensais que cela devrait être possible en utilisant un DFS modifié. Certaines propriétés peuvent être vérifiées localement, et la condition du cycle peut être prise en compte en utilisant les informations que vous avez sur les états de la pile.

Existe-t-il une référence papier ou autre où un tel algorithme est présenté?

Answer 1

Oui, c'est possible. Comme vous l'avez décrit, l'algorithme est très similaire à l'approche traditionnelle. La seule différence est la façon dont l'information sur l'indépendance des actions est recueillie. Conceptuellement, tout cela est assez simple. Par conséquent, je ne pense pas qu'il existe de documents sur un tel algorithme.

Pour votre cas d'utilisation, la minimisation de bisimulation est plus utile. Baier et Katoen donnent une bonne introduction dans leur livre "Principles of Model Checking". L'état de la technique est décrit dans "Paige et Tarjan - Trois algorithmes de raffinement de partition" pour la bisimulation forte et "Groote et Wijs - Un algorithme O (m log n) pour l'équivalence du bégaiement et la bisimulation de branchement" pour la bisimulation.