Recherche dans les graphes, model checking et techniques d'ordre partiel

Le problème de recherche dans un graphe est un problème fondamental pour beaucoup d'applications. Souvent, l'espace d'états est énorme, et optimiser la recherche est crucial.

Par exemple, certaines des actions peuvent commuter, c'est à dire que l'ordre dans lequel elle sont exécutées n'a aucune incidence sur l'état atteint (par exemple parce que ses actions sont sur deux processus concurrents). Les techniques d'ordre partiel se servent exactement des propriétés de commutation pour optimiser la recherche.

Nous exposerons tout d'abord les techniques de model checking dans un graphe, avant de considérer le cas d'un système distribué. Nous parlerons ensuite des techniques d'ordre partiel pour un graphe sans boucle (ensemble fini de chemins), puis des techniques pour réduire les états en général, avant de poursuivre avec les techniques pour réduire les transitions. Nous concluerons en considérant un contexte différent, les systèmes biologiques.