L'électronique de lecture des tomographes à émission de positrons (TEP) est performante, mais possède son lot de qualités et de défauts. Hautement incriminée, spontanément, dans l'explication de la sensibilité assez pauvre de ces instruments, il ressort tout d'abord de l'étude présentée que les temps morts répartis relatifs à l'électronique n'incombent aux pertes de données qu'à hauteur de 16% pour une activité injectée typique de 10 microCi/ml. Les taux d'acquisition bruts pourraient ainsi être majorés de 20% par la suppression des saturations. A regarder plus en détails la philosophie de l'acquisition sur ces imageurs, il apparaît un caractère limitant davantage encore la sensibilité : la résolution temporelle. Elle conditionne, au premier ordre, les possibilités de réjection des événements fortuits, d'une partie des diffusés et donc du bruit, finalement rapporté au signal matérialisé par les vraies coïncidences. Une minimisation de la résolution temporelle passe par la suppression des acteurs inutiles et l'adoption d'une technique d'étiquetage temporel adaptée (filtrage optimal). Ce faisant, la résolution intrinsèque des voies de lecture est diminuée d'un facteur 7, se réduisant à 350 ps. Le plancher du fenêtrage en coïncidence peut être abaissé substantiellement et le NECR augmente de 50% en conséquence. A ce stade, un algorithme de mesure du temps de vol (TOF) peut être implémenté. Opportuniste, il promet une réduction de la variance associée au bruit de 430%, ce gain se répercute sur le NECR. Au final, le cumul des idées permet d'espérer gagner un ordre de grandeur sur le rapport signal sur bruit NECR, avec l'espoir d'examens cliniques raccourcis d'autant. Dans ce contexte, il est apparu légitime d'imaginer un nouveau synoptique d'acquisition pour TEP entièrement pixélisés. Le nombre de canaux explose au passage, par rapport à ce qui existe. Ceci est en partie compensé par la décision d'intégrer l'électronique au maximum. Les mesures d'énergie et de temps sont prévues sur une seule et même voie d'acquisition, avec une lecture en continue et sans temps mort des événements incidents. Le développement de l'électronique est en cours, ce manuscrit donne une description des trois premiers blocs. A terme, la réalisation d'un démonstrateur est prévue.

Dans le domaine des systèmes informatisés où la fiabilité est la première priorité, les méthodes formelles ont prouvé leur efficacité pour la conception de logiciels sûrs. La dépendance à de tels systèmes augmente, et les contraintes rencontrées se font plus diverses et précises, en particulier les contraintes temporelles. Certaines méthodes formelles, notamment la méthode B, rendent la conception malaisée sous de telles contraintes, puisqu'elles n'ont pas été prévues pour cela à l'origine.<br /><br />Nous nous proposons donc d'étendre la méthode B pour lui permettre de spécifier et valider des systèmes à contraintes temporelles complexes. Nous utilisons pour ce faire des calculs de durées pour exprimer la sémantique du langage B et en déduire une extension conservative qui permet de l'utiliser à la fois dans son cadre d'origine et dans le cadre de systèmes à contraintes temporelles.<br /><br />Nous nous penchons également sur le problème de l'utilisation d'un outil de preuve générique pour valider des formules de calcul des durées. La généricité de ce type d'outil répond à la multiplication des méthodes formelles, mais pose le problème de l'intégration des fondations mathématiques de ces méthodes à un outil générique. Nous proposons donc d'étudier la mise en oeuvre en plongement léger du calcul des durées dans l'assistant de preuve Coq. Nous en déduisons un retour sur expérience de la définition d'une logique modale particulière dans un outil à vocation générique.

Le comportement des valeurs extrêmes de pluie en France a été analysé au travers de variables locales telles que les maxima annuels ou saisonniers de pluies mesurées sur différents pas de temps entre l'heure et la journée, les valeurs supérieures à un seuil élevé, ou la série temporelle de succession d'averses. Différents modèles, issus de la théorie des valeurs extrêmes uni-variée et bi-variée ou de générateurs stochastiques de pluie, ont été présentés pour étudier le comportement asymptotique de ces variables aléatoires. Dans le cas des séries temporelles d'averses, la persistance dans le temps des valeurs fortes a été modélisée à l'aide d'un processus Markovien. Les incertitudes associées aux différents modèles ont également été analysées, avec des méthodes bayésiennes ou fréquentielles. Nous avons pu valider nos modèles avec de longues séries de mesures pluviométriques, avec des chroniques de pluies horaires et avec des chroniques d'événements pluvieux décrits par des averses fournis par Météo-France et le Cemagref. Dans de nombreux cas, nous avons en particulier noté que la distribution des extrêmes est non bornée, et de queue plus lourde qu'une loi Gumbel ou exponentielle.

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs.

Dans la pratique de la planification urbaine, la prévision de la demande de transport fait en général appel au modèle à quatre étapes (génération, distribution, répartition modale et affectation), malgré des avancées théoriques considérables dans le domaine.Cette persistance s'explique par une facilité relative de mise en œuvre, liée notamment à la forme des données disponibles et susceptibles d'alimenter les modèles. Cependant, la nature statique de l'approche pose des interrogations quant à sa pertinence pour faire des prévisions de moyen-long terme. Cette thèse étudie, la validité de l'hypothèse de stabilité temporelle des trois premières étapes du modèle de prévision. Pour ce faire, en prenant l'agglomération lyonnaise comme terrain d'étude, nous avons codifié des réseaux routiers et de transports en commun à différentes dates (1985, 1995 et 2006). Cette donne, généralement indisponible, combinée aux enquêtes ménages déplacements correspondantes,nous permet de calibrer les trois premières étapes du modèle traditionnel et de tester leur capacité prédictive. Pour les modèles de génération, on note des prévisions acceptables à un horizon de 10 ans. À 20 ans, certaines évolutions dans les styles de vie se sont traduites paru ne baisse du nombre moyen de sorties pour le motif travail, que les modèles traditionnels ne permettent pas de prévoir complètement. Au niveau de la distribution, l'allongement des distances entre lieux de réalisation de certaines activités et le lieu de domicile peut être relativement bien reproduit par des modèles gravitaires avec des paramètres stables dans le temps. Au niveau de la répartition modale, les paramètres ne sont pas stables et les modèles estimés n'auraient pas permis de prévoir le regain de parts de marché des transports en commun observé ces dernières années.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

Le Québec vit un vieillissement marqué de sa population et doit faire face aux problèmes que cela engendre. Cette situation soulève des enjeux sociaux et économiques liés à la santé comme l'augmentation des problèmes chroniques de santé en fin de vie, le maintien de la qualité des soins à la population et plus généralement le financement du domaine de la santé. Le Centre de recherche sur les habitats intelligents (CRHI) de l'Université de Sherbrooke cherche à développer une solution technologique socialement acceptable à ces enjeux. Les travaux qui y sont faits visent à favoriser l'autonomie de personnes atteintes de troubles cognitifs afin de leur permettre de demeurer à domicile le plus longtemps possible. Cette recherche doctorale porte spécifiquement sur l'utilisation des technologies de l'habitat intelligent pour soutenir le travail coopératif entre les professionnels de la santé, les intervenants sociaux et les proches aidants. On y aborde la problématique du travail "même lieu/temps différents" dans l'équipe hétérogène sous l'angle du travail coopératif assisté par ordinateur (TCAO). Un collecticiel asynchrone distribué dans l'habitat intelligent a été développé à titre de preuve de concept. Des activités de communication, de coordination et de production des intervenants ont été scénarisées afin de démontrer le fonctionnement du prototype. Le collecticiel C4C intègre notamment des outils de travail éprouvés comme le système de mesure de l'autonomie fonctionnelle (SMAF) qui est utilisé pour déterminer et suivre le niveau de service à offrir à une personne en perte d'autonomie. Notre recherche a permis d'élaborer : - une infrastructure distribuée de services sous l'approche par réseau de pairs pour un habitat intelligent ; - un modèle de gestion de l'information dans une perspective historique et spatiale intérieure tridimensionnelle ; - un modèle de gestion de la coopération en mode "pousser de l'information" basé sur le contexte de travail. Ensemble, ces contributions structurent et définissent le mode de travail dans l'équipe de soins et de maintien à domicile. En facilitant la coopération dans l'habitat intelligent, notre recherche vise la continuité accrue des soins pour permettre à plus de personnes souffrant de limitations cognitives ou physiques de vivre à la maison dans leur communauté.

Afin d'analyser le rôle de la plasticité striatale dans la perception temporelle, nous avons réalisé une étude comportementale et électrophysiologique d'un modèle rat transgénique de la maladie de Huntington impliquant la dégénérescence progressive du striatum. Pour ce faire, nous avons élaboré une étude longitudinale (4-15 mois) du suivi de la maladie de Huntington au niveau moteur, motivationnel et temporel, et une étude présymptomatique (4-5 mois) de l'estimation temporelle et électrophysiologique in vivo de la voie préfronto-striatale. Nous avons détecté un dysfonctionnement de la perception temporelle et de la plasticité synaptique de manière présymptomatique, suggérant une corrélation entre ces deux dysfonctionnements. En symptomatique, le comportement temporel discriminatif est plus fortement altéré, corrélat d'une dégénérescence du striatum.

Le problème de la stéréovision à partir de caméras multiples calibrées capturant une scène fixe est étudié depuis plusieurs décennies. Les résultats présentés dans le benchmark de stéréovision proposé par Strecha et al., attestent de la qualité des reconstructions obtenues. En particulier, les travaux du laboratoire IMAGINE, mènent à des résultats visuellement impressionnant. Aussi, il devient intéressant de calibrer des scènes de plus en plus vastes, afin d'appliquer ces algorithmes de stéréovision de façon optimale. Trois objectifs essentiels apparaissent : - La précision de la calibration doit être améliorée. En effet comme pointé par Yasutaka Furukawa, même les benchmarks de stéréovision fournissent parfois des caméras bruitées à la précision imparfaite. Un des moyen d'améliorer les résultats de stéréovision est d'augmenter la précision de la calibration. - Il est important de pouvoir prendre en compte les cycles dans le graphe des caméras de façon globale. En effet la plupart des méthodes actuelles sont séquentielles, et dérivent. Ainsi ces méthodes ne garantissent pas, pour une très grande boucle, de retrouver cette configuration cyclique, mais peuvent plutôt retrouver une configuration des caméras en spirale. Comme on calibre des réseaux d'images, de plus en plus grand, ce point est donc crucial. - Pour calibrer des réseaux d'images très grands, il convient d'avoir des algorithmes rapides. Les méthodes de calibration que nous proposons dans la première partie, permettent de calibrer des réseaux avec une précision très proche de l'état de l'art. D'autre part elle permettent de gérer les contraintes de cyclicité par le biais d'optimisations linéaires sous contraintes linéaires. Ainsi ces méthodes permettent de prendre en compte les cycles et bénéficient de la rapidité de la programmation linéaire. Enfin, la recherche en stéréovision étant arrivée à maturité, il convient de s'intéresser à l'étape suivante, à savoir la reconstruction spatio-temporelle. La méthode du laboratoire IMAGINE représentant l'état de l'art en stéréovision, il est intéressant de développer cette méthode et de l'étendre à la reconstruction spatio-temporelle, c'est-à-dire la reconstruction d'une scène dynamique capturée par un dôme de caméras. Nous verrons cette méthode dans la seconde partie de ce manuscrit

Le développement croissant des réseaux et en particulier l'Internet a considérablement développé l'écart entre les systèmes d'information hétérogènes. En faisant une analyse sur les études de l'interopérabilité des systèmes d'information hétérogènes, nous découvrons que tous les travaux dans ce domaine tendent à la résolution des problèmes de l'hétérogénéité sémantique. Le W3C (World Wide Web Consortium) propose des normes pour représenter la sémantique par l'ontologie. L'ontologie est en train de devenir un support incontournable pour l'interopérabilité des systèmes d'information et en particulier dans la sémantique. La structure de l'ontologie est une combinaison de concepts, propriétés et relations. Cette combinaison est aussi appelée un graphe sémantique. Plusieurs langages ont été développés dans le cadre du Web sémantique et la plupart de ces langages utilisent la syntaxe XML (eXtensible Meta Language). Les langages OWL (Ontology Web Language) et RDF (Resource Description Framework) sont les langages les plus importants du web sémantique, ils sont basés sur XML.Le RDF est la première norme du W3C pour l'enrichissement des ressources sur le Web avec des descriptions détaillées et il augmente la facilité de traitement automatique des ressources Web. Les descriptions peuvent être des caractéristiques des ressources, telles que l'auteur ou le contenu d'un site web. Ces descriptions sont des métadonnées. Enrichir le Web avec des métadonnées permet le développement de ce qu'on appelle le Web Sémantique. Le RDF est aussi utilisé pour représenter les graphes sémantiques correspondant à une modélisation des connaissances spécifiques. Les fichiers RDF sont généralement stockés dans une base de données relationnelle et manipulés en utilisant le langage SQL ou les langages dérivés comme SPARQL. Malheureusement, cette solution, bien adaptée pour les petits graphes RDF n'est pas bien adaptée pour les grands graphes RDF. Ces graphes évoluent rapidement et leur adaptation au changement peut faire apparaître des incohérences. Conduire l'application des changements tout en maintenant la cohérence des graphes sémantiques est une tâche cruciale et coûteuse en termes de temps et de complexité. Un processus automatisé est donc essentiel. Pour ces graphes RDF de grande taille, nous suggérons une nouvelle façon en utilisant la vérification formelle " Le Model checking ".Le Model checking est une technique de vérification qui explore tous les états possibles du système. De cette manière, on peut montrer qu'un modèle d'un système donné satisfait une propriété donnée. Cette thèse apporte une nouvelle méthode de vérification et d'interrogation de graphes sémantiques. Nous proposons une approche nommé ScaleSem qui consiste à transformer les graphes sémantiques en graphes compréhensibles par le model checker (l'outil de vérification de la méthode Model checking). Il est nécessaire d'avoir des outils logiciels permettant de réaliser la traduction d'un graphe décrit dans un formalisme vers le même graphe (ou une adaptation) décrit dans un autre formalisme