Nous considérons une sous classe d'automates temporisés probabilistes où les contraintes temporelles au niveau des gardes et des invariants sont exprimées par des paramètres. Cette sous classe est appelée la classe des automates Temporisés Probabilistes Paramétrés Semi Déterminés (ATPP Semi Déterminés). Cette classe d'automates se définit en particulier par l'attribution d'une unique distribution à chaque état et par des gardes de la forme x<=a où a est un paramètre ou un entier naturel. Nous imposons de plus deux propriétés sur ces automates qui sont celles de non blocage et fortement non zenon. Notre travail vise à calculer le temps moyen maximal de convergence vers un état dit absorbant q_end dans ce type d'automates. L'unique méthode traitant déjà ce type de problème fait appel à la discrétisation du temps et à l'application de techniques de programmation linéaire. Elle est cependant exponentielle car elle dépend du nombre d'horloges et de la plus grande constante à laquelle sont comparées les horloges, lors de la discrétisation. Le graphe résultant peut être de taille exponentielle. Pour tout ATPP Semi Déterminé, on définit un automate totalement déterministe, appelé ATPP Déterminé, en remplaçant toute garde de la forme x<=a par une garde de la forme x=a. Le temps d'attente en chaque état est ainsi fixé par la valuation de l'état initial qui remet toutes les horloges à zéro. Nous démontrons que le temps moyen de convergence vers q_end dans l'ATPP Déterminé est égal au temps moyen maximal de convergence dans l'ATPP Semi Déterminé dont il découle. Pour calculer le temps moyen de convergence vers q_end nous construisons à partir de l'ATPP Déterminé un graphe appelé "graphe des macro-steps" qui contient de façon concise l'information nécessaire au calcul du coût moyen de convergence vers q_end. Ce graphe est de taille polynomiale et se construit en temps polynomial. Le calcul du temps moyen de convergence dans le graphe des macro-steps est solution d'un système linéaire, comme dans le cas des chaînes de Markov avec coûts. On résout ce système linéaire en temps polynomial, ce qui permet d'obtenir finalement le temps moyen maximal de convergence vers q_end dans l'ATPP Semi Déterminé. Nous appliquons enfin cette méthode à certains protocoles de communication, notamment BRP (Bounded Retransmission Protocol) et CSMA/CD (Carrier Sense Multiple Access with Collision Detection).
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00626062 |
| Date | 27 October 2009 |
| Creators | Chamseddine, Najla |
| Publisher | École normale supérieure de Cachan - ENS Cachan |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds