Avhandling--Aalborg, 2003. / bibliogr. p. 357-373.

Th.--Lett.--Paris 4, 1979. / Index.

Nous présentons une méthode symbolique pour représenter des modèles probabilistes à espace d'états continu (LMP). Ces modèles représentent des systèmes de transitions qui ont un nombre d'états non-dénombrable. L'objectif de l'utilisation d'une méthode symbolique est de consommer moins de mémoire lors de l'enregistrement du modèle. Notre technique pour enregistrer symboliquement les modèles est l'utilisation des diagrammes de décision binaire à terminaux multiples (MTBDD). Ces diagrammes offrent la possibilité d'enregistrer des fonctions à variables booléennes, ainsi que des graphes, de façon plus concise que les techniques plus fréquemment utilisées. Nous employons les MTBDD dans un vérificateur de modèles de type LMP nommé CISMO. La vérification de modèles est une technique entièrement automatique qui est utilisée pour vérifier si un modèle respecte ou non sa spécification. L'espace mémoire nécessaire pour faire la vérification dépend entre autres des structures utilisées pour enregistrer le modèle. Dans la première version de CISMO, le modèle était enregistré à l'aide de structures de données traditionnelles, comme des vecteurs. Cette façon de faire est qualifiée d'explicite. Nos modifications de CISMO lui permettent maintenant de faire la vérification de façon symbolique, à l'aide des MTBDD, en plus de la façon explicite. Nos principales contributions sont la description de deux heuristiques qui, dans certains contextes, réduisent la taille des diagrammes de décision binaire ordonnés, ainsi que la modification de CISMO. L'analyse de la mémoire consommée par CISMO après nos modifications nous montre que l'utilisation des diagrammes de décision permet de sauver de la mémoire.

Nous nous intéressons aux erreurs qui apparaissent lors de la vérification de systèmes probabilistes en utilisant la technique d’évaluation de modèle avec l’outil PRISM. L’évaluation de modèle probabiliste est une technique de vérification qui consiste à déterminer si un modèle probabiliste M vérifie une propriété donnée. Les modèles sont décrits par des systèmes de transitions tandis que la logique temporelle est utilisée comme langage de spécification des propriétés. L’algorithme d’évaluation de modèle qui est appliqué consiste essentiellement à résoudre un système d’équations linéaires Ax = b. Nous montrons à quelles étapes du processus d’évaluation de modèle les erreurs apparaissent. Nous distinguons essentiellement deux types d’erreurs à savoir les erreurs d’arrondi (arithmétique à point flottant, model-checking symbolique), et les erreurs de troncature qui proviennent du fait qu’on a remplacé une méthode de calcul direct par des opérations mettant en jeu un nombre fini d’étapes. Nous utilisons la notion de bisimulation approchée pour comparer le modèle M à l’étude et celui réellement encodé par PRISM. Nous faisons aussi une analyse numérique de l’écart entre la solution x du système linéaire Ax = b et celle calculée par PRISM suite aux effets de l’erreur d’arrondi. / We are interested in errors that occur during the verification of probabilistic systems using the technique of model-checking with PRISM tool. Probabilistic model-checking is a technique for verification that aims at determining whether a probabilistic model satisfies a given property. The models are described by transition systems while temporal logic is used as specification language for properties. The model-checking algorithm under study essentially involves solving a system of linear equations Ax = b.We show at what stages of the model-checking process the errors appear. We basically distinguish two types of errors, namely rounding errors (floatingpoint arithmetic, symbolic model checking), and truncation errors, which arise because a direct method of calculation is replaced by operations involving a finite number of steps. We use a notion of approximate bisimulation to compare the model under study and the one actually encoded by PRISM. We also carry a numerical analysis of the difference between the solution of the linear system Ax = b and the one calculated by PRISM, due to the effects of rounding errors.

La vérification de systèmes est aujourd’hui un sujet de recherche récurrent et différentes techniques permettent de vérifier formellement des systèmes critiques dont il faut impérativement garantir la correction. Nous consacrons ce mémoire à l’une des techniques les plus utilisées et les plus efficaces, l’évaluation de modèle. Schématiquement, pour vérifier un système par évaluation de modèle, on abstrait d’abord son comportement sous la forme d’un système de transitions appelé modèle. Ensuite, on formule une propriété désirée du système dans une logique temporelle. Enfin, on utilise un outil logiciel appelé vérificateur pour vérifier automatiquement si le modèle satisfait la propriété. Dans ce mémoire, nous voulons vérifier des propriétés d’atteignabilité dans des modèles probabilistes appelés processus de Markov étiquetés (en anglais, LMP pour Labelled Markov processes) et qui ont possiblement un ensemble d’états non dénombrable. Malheureusement, le vérificateur CISMO dédié à une famille de LMP ne gère pas les propriétés d’atteignabilité et aucun autre outil ne peut vérifier les LMP. Pour améliorer CISMO et atteindre notre objectif, nous avons rendu d’abord plus expressive sa logique de spécification de propriétés pour qu’elle exprime les propriétés d’atteignabilité sur les LMP. Ces propriétés expriment le fait qu’un état souhaité dans un système peut être atteint avec une certaine probabilité. Ensuite, nous avons implémenté dans CISMO une nouvelle approche de vérification d’une famille de propriétés d’atteignabilité qui contribue à l’évolution de la vérification probabiliste. Nous utilisons le théorème de la moyenne pour prouver que, pour tout LMP acceptable par CISMO et toute propriété d’atteignabilité, il existe une chaîne de Markov à temps discret (en anglais, DTMC pour Discrete Time Markov Chains) équivalent au LMP de point de vue atteignabilité moyenne et auquel on peut appliquer les algorithmes connus pour les systèmes probabilistes finis. Le DTMC est construit de telle sorte que nous inférons que le LMP satisfait la propriété d’atteignabilité, si et seulement si le DTMC la satisfait. Théoriquement, notre approche donne un résultat ultime exact et nous l’avons prouvé. À l’implémentation, nous utilisons une méthode d’intégration numérique pour déterminer les probabilités de transition dans le DTMC. Malgré les imprécisions numériques qui peuvent nuire au résultat d’une vérification, nous avons prouvé que notre approche a du sens en quantifiant les erreurs. Nous avons démontré d’une part que les erreurs numériques sont toujours bornées supérieurement dans le DTMC et avons montré d’autre part, qu’il existe une relation de bisimulation entre le LMP et le DTMC. Notre méthode est originale et repousse les limites de l’évaluation de modèle, notamment l’explosion combinatoire de l’espace d’états ou de chemins dans la vérification de systèmes probabilistes infinis. / Systems verification is nowadays a major issue and various techniques verify formally critical systems for which correction must be ensured. The focus of this master’s thesis is on one of the most used and most effective systems verification techniques, modelchecking. Conceptually, to apply model-checking to a system, we first abstract its behavior in the form of a transitions system, the model. Then, we formulate a system property of interest in a temporal logic. Finally, a software called model-checker is used to verify automatically if the model satisfies the property. In this paper, we want to check reachability property in the probabilistic models called labelled Markov process (LMP) and which have possibly an uncountable set of states. Unfortunately, the model-checker CISMO dedicated to a family of LMP does not handle reachability properties and no other tool can verify LMP. To improve CISMO and achieve our goal, we first made more expressive its properties specification logic so that it can express reachability property on LMP. These properties express the fact that a desired state in a system can be reached with a certain probability. Secondly, we implemented in CISMO a new approach for the verification of a family of reachability properties. This is a contribution to the evolution of the probabilistic verification. We use the mean theorem to prove that, for any LMP acceptable by CISMO and for any reachability property, there is a discrete time process (DTMC) equivalent to the LMP according to the average reachability and on which we can apply known algorithms for probabilistic systems which have a countable set of states. The DTMC is constructed in such a way that we can infer the LMP satisfies the reachability property, if and only if the DTMC also satisfies it. Theoretically, our approach gives a precise final result and we prove it. At implementation, since the DTMC is subjected to numerical errors the result can be false, as expected. We use a numerical integration method to determine the transitions probabilities in the DTMC. Despite the errors that can affect the outcome of a verification, we have shown that our approach makes sense at implementation by quantifying the errors. We have shown on one hand that numerical errors are always bounded from above in the DTMC and we established, on the other hand, bisimulation relations between LMP, DTMC constructed theoretically, and DTMC generated algorithmically with errors. Our method is original and pushes the limits of model-checking, especially combinatorial explosion of the states space or paths in the verification of infinite probabilistic systems.

Thèse (Ph.D.)--Université Laval, 1998. / Mode d'accès: World Wide Web. Comprend des réf. bibliogr.

No description available.

En 1651, Pierre-Esprit Radisson, jeune Français d'environ 16 ans, rejoint deux de ses soeurs à Trois-Rivières, en Nouvelle-France. L'année suivante, les Iroquois le capturent, le torturent, puis l'adoptent. Radisson répondit au défi que posait sa survie parmi les Iroquois en s'intégrant le plus possible à eux, et en tentant de se distinguer comme guerrier. Après 18 mois de vie iroquoise, Radisson s'évada par la Nouvelle-Hollande, regagna l'Europe puis la Nouvelle-France, où il profita des connaissances amérindiennes qu'il avait acquises en devenant explorateur et commerçant de fourrures, d'abord au côté des jésuites français et des commerçants de Nouvelle-France, puis au côté des marchands anglais de la Hudson's Bay Company, fondée à Londres, en 1670. Cette nouvelle biographie de Radisson se veut d'abord une réflexion sur l'exceptionnelle capacité d'adaptation de celui qui sut non seulement s'acclimater à des environnements socioculturels très contrastés, comme la France, la Nouvelle-France, l'Iroquoisie, l'Angleterre et la baie d'Hudson des bandes nomades cries, mais qui parvint aussi à remporter du succès dans presque tous ces environnements. J'ai trouvé utile et pertinent de m'inspirer des développements théoriques récents en sciences pures, autour des concepts d'analyse relationnelle et d'ordre émergent, pour mieux comprendre la personnalité dynamique de Radisson, mieux situer ses diverses « colorations » culturelles et mieux sentir la profondeur volatile et concrète des cultures et des milieux auxquels il a dû s'adapter. Le personnage de Radisson, les événements et les situations historiques qu'il a connus, sont perçus et analysés ici comme des phénomènes complexes. Cette étude historique innove donc par la manière dont elle observe et explique un phénomène humain qui évolue dans le temps: un personnage, un événement, une époque; par la définition des objectifs de recherche et par la manière de présenter les résultats de cette recherche. Puisque la stratégie de démonstration ne suffit plus dans la perspective relationnelle à éclairer la complexité des phénomènes humains, j'accorde ici une importance égale à la stratégie de communication de la connaissance historique, et des éléments de cette connaissance entre eux, pour mieux cerner la richesse et la complexité de mon sujet d'étude: Radisson. / Québec Université Laval, Bibliothèque 2013

L'explorateur, anthropologue, collectionneur, homme d'affaires, industriel et poète Auguste Genin (1862-1931), sillonna le territoire mexicain dans le cadre de ses multiples activités professionnelles dès les années 1880. Parallèlement, il développa un grand intérêt pour l'archéologie, l'histoire, la culture et les populations du Mexique. Son « œuvre archéologique» comprend l'ensemble de ses activités d'exploration et ses travaux archéologiques (fouilles, collectes, acquisitions) ainsi que leurs résultats, c'est à dire les collections archéologiques, et la documentation créée autour de ses ensembles. Pendant presque quatre décennies, entre la fin des années 1890 et le début des années 1930, Genin envoya plus de 1100 objets archéologiques à différents musées et institutions, notamment en Europe. Dans une époque charnière pour l'archéologie au Mexique, Genin fut témoin privilégié et acteur de l'évolution de la politique en matière d'études archéologiques et de l'appréciation pour les cultures préhispaniques. Ses travaux préservèrent la « mémoire » des pratiques et du collectionnisme «anciens», tout en s'ouvrant à une nouvelle ère. L'objectif principal de cette recherche est de dresser un profil du collectionneur et, par extension, d'une époque, et d'établir sa place dans l'histoire de la discipline au Mexique, par l'analyse de son œuvre archéologique. Cette dernière n'avait pas encore fait l'objet d'une étude complète, détaillée et synthétique et, en dépit de leur importance et de leur intérêt scientifique, aucun inventaire complet des ensembles n'en avait été dressé. / Explorer, anthropologist, collector, businessman, entrepreneur, and poet Auguste Genin (1862-1931), travelled throughout Mexican lands since the 1880's whilst carrying on his diverse business activities. At the same time, he developed a great interest in the archaeology, history, culture and peoples of Mexico .. His "archaeological work" is here understood as the whole of h.is exploration and archaeological activities (excavation, surface collection, acquisitions), as well as their direct results, that is, the archaeological collections themselves and ail the documentation associated with them. Over the span of more than forty years, between the end of the 1890's and the beginning of the 1930's, Genin sent more than 11 000 archaeological objects to various museums and institutions, mostly in Europe. During a pivotal moment for Mexican archaeology, Genin was a privileged witness and participant of the evolution concerning archaeological practice and study and the appreciation of pre-Columbian cultures. His work preserved the "memory" of "old-time" methods and collecting, and at the same time embraced a new era. The main goal of this research project is to draw a portrait of Genin as collector and, by extension, of a specific period, as well as to establish his place in the history of the discipline in Mexico, through the examination of his archaeological work. The latter had not yet been subject to a complete, detailed and integrated study, despite its importance and scientific interest, nor had a complete inventory of his collections been drawn up.

Texte remanié de : Thèse : Lettres : Paris : 1969. / Titre provenant de l'écran d'accueil. Bibliogr. p. 483-498. Index.