Réduction de la commande partielle

La réduction de la commande partielle est une technique pour réduire la taille de l’espace d’état à rechercher par une vérification de modèle ou de planification. Il exploite la commutativité des transitions exécutées simultanément, qui aboutissent au même état lorsqu'elles sont exécutées dans des ordres différents.

Dans l'exploration d'espace de l'état explicite, la réduction partielle des ordres fait généralement référence à la technique spécifique consistant à développer un sous-ensemble représentatif de toutes les transitions activées. Cette technique a également été décrite comme une vérification de modèle avec des représentants (Peled, 1993). Il existe différentes versions de la méthode, la méthode dite du set obstiné (Val mari 1990), la méthode du set complet (Peled 1993) et la méthode du set persistant (Godefroid 1994).