Problème d'accessibilité
Le problème d'accessibilité (aussi appelé le problème d'atteignabilité)[1] est, en informatique, le problème algorithmique qui consiste à déterminer si, dans un système, une situation finale est accessible/atteignable depuis une situation initiale. Le problème d'accessibilité a été étudié dans les automates finis, les automates cellulaires, les automates temporisés, les systèmes infinis, etc.
Graphe fini explicite
[modifier | modifier le code]Le problème d'accessibilité dans un graphe orienté décrit explicitement est NL-complet. Reingold, dans un article de 2008, a démontré que le problème d'accessibilité pour un graphe non-orienté est dans LOGSPACE[2].
En vérification de modèles, l'accessibilité correspond à une propriété de vivacité.
Graphe fini implicite
[modifier | modifier le code]En planification, plus précisément en planification classique, on s'intéresse à savoir si on peut atteindre un état depuis un état initial à partir d'une description des actions. La description des actions définissent un graphe des états implicites, qui est de taille exponentielle en la taille de la description.
En vérification de modèles symbolique, le modèle (le graphe sous-jacent) est décrit à l'aide d'une représentation symbolique comme des diagrammes de décision binaire.
Réseaux de Petri
[modifier | modifier le code]Le problème d'accessibilité dans un réseau de Petri est décidable[3]. Dès 1976, on savait que ce problème était EXPSPACE-dur[4]. Il y a des résultats sur combien implémenter ce problème en pratique[5]. En 2018, le problème a été démontré comme non-élémentaire[6].
Notes et références
[modifier | modifier le code]- (en) RP Organization Committee, « (RP'17) 11th International Workshop on Reachability Problems 2017 », sur rp17.cs.rhul.ac.uk (consulté le )
- Omer Reingold, « Undirected connectivity in log-space », Journal of the ACM, vol. 55, no 4, , p. 1–24 (lire en ligne)
- (en) Ernst W. Mayr, « An algorithm for the general Petri net reachability problem », STOC '81 Proceedings of the thirteenth annual ACM symposium on Theory of computing, Association for Computing Machinery, , p. 238–246 (DOI 10.1145/800076.802477, lire en ligne, consulté le )
- R. Lipton, « The Reachability Problem Requires Exponential Space », Technical Report 62, (lire en ligne)
- P. Küngas « Petri Net Reachability Checking Is Polynomial with Optimal Abstraction Hierarchies » (July 26–29, 2005) (lire en ligne)
—Proceedings of the 6th International Symposium on Abstraction, Reformulation and Approximation—SARA 2005 - (en) Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jerome Leroux et Filip Mazowiecki, « The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract) », .
