Soutenance de thèse de Changshun WU

L’un des problèmes fondamentaux de test pour les systèmes à événements discrets (SEDs) est l’identification d’un état final, c’est-à-dire, étant donné un système dont l’état courant est inconnu, trouver une séquence d’événements d’entrée pouvant le conduire à un état connu. Les séquences de synchronisation (SS), sans information de sortie, sont une solution classique à ce problème. Dans cette thèse, nous étudions la détermination des SS pour des systèmes modélisés par des réseaux de Petri synchronisés (SynPN) non bornés, une classe de réseaux de Petri avec des entrées. L’analyse des systèmes avec un espace d’états infini est un problème difficile et il n’existe actuellement aucune approche générale capable de représenter de manière finie les espaces d’états infinis des SynPN non bornés. Ainsi, cette thèse se concentre sur une sous-classe de réseaux, les 1-place-unbounded SynPNs, dans lesquels une seule place est non bornée. Dans la première partie de cette thèse, nous développons deux méthodes: 1) construction d’une représentation finie, appelée improved modified coverability graph (IMCG), pour d’écrire exactement l’espace d’états infini d’un 1-place-unbounded SynPN; 2) conversion d’un 1-place-unbounded SynPN en un automate pondéré (WA) fini et sauf équivalent. Les deux graphes sont ainsi potentiellement des outils puissants pour déterminer les séquences de synchronisation pour une telle sous-classe de réseaux de Petri. Dans la seconde partie de cette thèse, nous développons des algorithmes de calcul pour deux problèmes de synchronisation de localisation dans le cas où l’IMCG ou le WA sont déterministes : synchronisation sur un seul nœud et synchronisation sur un sous-ensemble de nœuds de ces deux graphes. Ensuite, nous montrons que ces approches peuvent être utilisées pour résoudre deux problèmes différents liés au réseau d’origine: la synchronisation sur un seul nœud du graphe qui permet la synchronisation du réseau de Petri dans un marquage connu pour les places bornées ; la synchronisation sur un sous-ensemble de noeuds du graphe avec les mêmes marquages sur les places bornées spécifiées qui correspond à la synchronisation du réseau dans un marquage connu d’un sous-ensemble de places bornées. L’avantage de ces algorithmes de calcul est de réduire le calcul sur les graphes globaux (IMCG ou WA) à celui du plus petit sous-graphe : la composante fortement connectée ergodique peut réduire l’effort de calcul mais peut également être appliquée lorsque le IMCG ou le WA équivalent déterministes ne sont pas fortement connexes.

One of the fundamental testing problems for discrete event systems (DESs) is the identification of a final state, i.e., given a system whose current state is unknown, find an input sequence that can drive it to a known state. Synchronizing sequences (SSs), without output information, are one conventional solution to this problem. In this thesis, we address the computation of SSs for systems modeled by unbounded synchronized Petri nets (SynPNs), a class of Petri nets with inputs. The analysis of systems with an infinite state space is a challenging problem and currently there exists no general approach that can finitely represent the infinite state spaces of unbounded SynPNs. Thus this thesis focuses on a subclass of nets, 1-place-unbounded SynPNs, in which a single place is unbounded. In the first part of this thesis, we utilize two methods : 1) construct a finite representation, called improved modified coverability graph (IMCG), to exactly describe the infinite state space of a 1-place-unbounded SynPN; 2) convert a 1-place-unbounded SynPN into an equivalent finite location weighted automaton (WA) with safety conditions. Both graphs are thus, potentially, useful tools to compute SSs for such subclass of nets. In the second part of this thesis, we develop computation algorithms for two location synchronization problems in the case either the IMCG or the WA is deterministic: synchronization into a single node and synchronization into a subset of nodes of these two graphs. Then we show that this approach can be used to solve two different problems related to the original net : the synchronization into a single node of the graph of its IMCG or WA corresponds to synchronizing the net into a known marking of bounded places, while the synchronization into a subset of nodes of the graph of its IMCG or WA with same marking on specified bounded places corres- ponds to synchronizing the net into a known marking of a subset of bounded places. The advantage of these computation algorithms consists in reducing the computation on the global graphs (IMCGs or WAs) to the one on the smaller subgraph: the ergodic strongly connected component (SCC), which can reduce the computational effort and furthermore can also be applied when the converted deterministic IMCG or WA is not strongly connected.