La plupart des scénarios multimédia interactifs sont basés sur des spécifications informelles, il n'est donc pas possible de vérifier formellement des propriétés de ces systèmes. Nous préconisons la nécessité d'un modèle général et formel. Partitions interactives est un formalisme pour décrire des scénarios multimédia interactifs. Nous proposons une nouvelle sémantique pour les partitions interactives basée sur les structures d'événements temporisés. Avec une telle sémantique, nous pouvons spécifier des propriétés pour le système, en particulier, des propriétés sur les traces, qui sont difficiles à préciser avec la programmation par contraintes. Nous présentons également une sémantique opérationnelle des partitions interactives basée sur le calcul non-déterministe, temporisé, concurrent, par contraintes (ntcc) et nous rapportons la sémantique operationelle à la semantique en structures d'événements temporisés. Avec la sémantique opérationnelle, nous pouvons décrire formellement le comportement d'un scenario dont les durées des objets temporels peuvent être des intervalles d'entiers arbitraires. La sémantique opérationnelle est obtenue à partir de la sémantique en structures d'événements temporisés de la partition interactive. Pour fournir une telle traduction, nous avons d'abord défini la forme normale d'une structure d'événements temporisés, dans laquel les événements liés avec une durée zéro sont regroupés en un seul. Nous avons également défini la notion de structures d'événements temporisés répartissables, de telle sorte que son graphe de contraintes peut être expédié en se fondant uniquementsur la propagation locale. Nous croyons que la sémantique opérationnelle basée sur ntcc offre certains avantages par rapport à la sémantique des partitions interactives basée sur des réseaux de Petri; par exemple, les durées des objets temporels peuvent être des intervalles d'entiers arbitraires, tandis que dans la plupart des modèles de partitions interactives, les intervalles ne peut être utilisés que pour représenterles relations telles que l'égalité et les inégalités. Nos modèles ntcc de partitions interactives sont exécutés en utilisant Ntccrt, un interprète temps réel pour ntcc. Nos modèles peuvent également être vérifiés automatiquement en utilisant ntccMC, un vérificateur pour ntcc, de temps borné, basée sur les automates finis, que nous introduisons dans cette thèse. En utilisant ntccMC, nous pouvons vérifier des propriétés de logique de temps linéaire avec des contrantes (CLTL). Dans cette thèse, nous introduisons deux extensions du formalisme de partitions interactives:(1) l'une pour gérer le traitement audio en utilisant le langage de programmation français Faustet (2) l'autre pour traiter des condition et des branchements, permettant de spécifier des choix et des boucles. Pour la première extension, nous présentons une sémantique basée sur les structures d'événements temporisés et des idées sur la façon de définir une sémantique opérationnelle. Pour la deuxième extension, nous présentons une mise en oeuvre et la comparaison des résultats du jitter relative moyenne d'une implémentation d'un arpège base sur l'algorithme de Karplus-Strong par rapport aux implémentations existants écrits dans Pure Data. Nous définissons aussi un format de sauvegarde XML pour les partitions interactives et pour la extension avec branchement conditionnel. Un format de sauvegarde est crucial pour assurer la persistance des partitions. / Technology has shaped the way on which we compose and produce music. Notably, the invention of microphones and computers pushed the development of new music styles in the 20th century. In fact, several artistic domains have been benefiting from such technology developments ; for instance, Experimental music, non-linear multimedia, Electroacoustic music, and interactive multimedia. In this dissertation, we focus on interactive multimedia.Interactive multimedia deals with the design of scenarios where multimedia content and interactive events are handled by computer programs. Examples of such scenarios are multimedia art installations, interactive museum exhibitions, some Electroacoustic music pieces, and some Experimental music pieces. Unfortunately, most interactive multimedia scenarios are based on informal specifications, thus it is not possible to formally verify properties of such systems. We advocate the need of a general and formal model. Interactive scores is a formalism to describe interactive multimedia scenarios. We propose new semantics for interactive scores based on timed eventstructures. With such a semantics, we can specify properties for the system, in particular, properties about traces, which are difficult to specify as constraints. In fact, constraints are an important part of the semantic model of interactive scores because the formalism is based on temporal constraints among the objects of the scenario. We also present an operational semantics of interactive scores based on the non-deterministic timed concurrent constraint (ntcc) calculus and we relate such a semantics to the timed event structures semantics. With the operational semantics, we formally describe the behavior of a score whose temporal object durations can be arbitrary integer intervals. The operational semantics is obtained from the timed event structures semantics of the score. To provide such a translation, we first define the normal form of a timed event structure in which events related with zero-duration delays are collapsed into a single one. We also define the notion of dispatchable timed event structures. Event structures such that its constraint graph can be dispatched by relying only on local propagation.We believe that operational semantics in ntcc offers some advantages over existing Petri nets semantics for interactive scores; for instance, the duration of the temporal objects can be arbitrary integer intervals, whereas inprevious models of interactive scores, such durations can only be intervals to represent equalities and inequalities. In this dissertation, we also introduce two extensions of the formalism of interactive scores : (1) one to handle audio processing using the Fast AUdio Stream (Faust) languageand (2) another one to handle conditional branching, allowing designers to specify choices and loops. For the first extension, we present a timed event structures semantics and ideas on how to define operational semantics. For the second extension, we present an implementation and results comparing the average relative jitter of an implementation ofan arpeggio based on Karplus-Strong with respect to existing implementations of Karplus written in Pure Data. We also define a XML file format for interactive scores and for the conditional branching extension. A file format is crucial to assure the persistence of the scores. Ntcc models of interactive scores are executed using Ntccrt, a real-time capable interpreter for ntcc. They can also be verified automatically using ntccMC, a bounded-time automata based model checker for ntcc which we introduce in this dissertation. Using ntccMC, we can verify properties expressed on constraint linear-time logic. Ntcc has been used in the past, not only for multimedia interaction models, but alsofor system biology, security protocols and robots.

La plupart des sc\'narios multimédia interactifs sont bas\'{e}s sur des sp\'cifications informelles, il n'est donc pas possible de v\'{e}rifier formellement des propri\'t\'{e}s de ces syst\'mes. Nous pr\'{e}conisons la n\'cessit\'{e} d'un mod\'le g\'{e}n\'ral et formel. Partitions interactives est un formalisme pour d\'{e}crire des sc\'narios multim\'{e}dia interactifs. Nous proposons une nouvelle s\'mantique pour les partitions interactives bas\'{e}e sur les structures d'\'v\'{e}nements temporisés. Avec une telle s\'mantique, nous pouvons sp\'{e}cifier des propri\'t\'{e}s pour le syst\'me, en particulier, des propri\'{e}t\'s sur les traces, qui sont difficiles \'{a} pr\'ciser avec la programmation par contraintes. Nous pr\'{e}sentons \'galement une s\'{e}mantique op\'rationnelle des partitions interactives bas\'{e}e sur le calcul non-d\'terministe, temporis\'{e}, concurrent, par contraintes (ntcc) et nous rapportons la s\'mantique operationelle \'{a} la semantique en structures d'\'v\'{e}nements temporisés. Avec la s\'mantique op\'{e}rationnelle, nous pouvons d\'crire formellement le comportement d'un scenario dont les dur\'{e}es des objets temporels peuvent \^{e}tre des intervalles d'entiers arbitraires. La s\'mantique op\'{e}rationnelle est obtenue \' partir de la s\'{e}mantique en structures d'\'v\'{e}nements temporisés de la partition interactive. Pour fournir une telle traduction, nous avons d'abord d\'fini la forme normale d'une structure d'\'{e}v\'nements temporisés, dans laquel les \'{e}v\'nements li\'{e}s avec une dur\'e z\'{e}ro sont regroup\'s en un seul. Nous avons \'{e}galement d\'fini la notion de structures d'\'{e}v\'nements temporisés r\'{e}partissables, de telle sorte que son graphe de contraintes peut \^{e}tre exp\'di\'{e} en se fondant uniquement sur la propagation locale. Nous croyons que la s\'mantique op\'{e}rationnelle bas\'e sur ntcc offre certains avantages par rapport \'{a} la s\'mantique des partitions interactives bas\'{e}e sur des r\'seaux de Petri; par exemple, les dur\'{e}es des objets temporels peuvent \^{e}tre des intervalles d'entiers arbitraires, tandis que dans la plupart des mod\'les de partitions interactives, les intervalles ne peut \^tre utilis\'{e}s que pour repr\'senter les relations telles que l'\'{e}galit\' et les inégalités. Nos mod\'{e}les ntcc de partitions interactives sont ex\'cut\'{e}s en utilisant Ntccrt, un interpr\'te temps r\'{e}el pour ntcc. Nos mod\'les peuvent \'{e}galement \^{e}tre v\'rifi\'{e}s automatiquement en utilisant ntccMC, un verificateur pour ntcc, de temps born\', bas\'{e}e sur les automates finis, que nous introduisons dans cette th\'se. En utilisant ntccMC, nous pouvons v\'{e}rifier des propri\'t\'{e}s de logique de temps lin\'aire avec des contrantes (CLTL). Dans cette th\'{e}se, nous introduisons deux extensions du formalisme de partitions interactives: (1) l'une pour g\'rer le traitement audio en utilisant le langage de programmation fran\c cais Faust et (2) l'autre pour traiter des condition et des branchements, permettant de sp\'{e}cifier des choix et des boucles. Pour la premi\'re extension, nous pr\'{e}sentons une s\'mantique bas\'{e}e sur les structures d'\'v\'{e}nements temporisés et des id\'es sur la fa\c con de d\'{e}finir une s\'mantique op\'{e}rationnelle. Pour la deuxi\'me extension, nous pr\'{e}sentons une mise en \oe uvre et la comparaison des r\'sultats du jitter relative moyenne d'une impl\'{e}mentation d'un arp\'ge base sur l'algorithme de Karplus-Strong par rapport aux impl\'{e}mentations existants \'crits dans Pure Data. Nous d\'{e}finissons aussi un format de sauvegarde XML pour les partitions interactives et pour la extension avec branchement conditionnel. Un format de sauvegarde est crucial pour assurer la persistance des partitions.

Le raisonnement epistémique joue un rôle en théorie de la concurrence de plusieurs manières distinctes mais complémentaires; cette thèse en décrit trois. La première, et presque certainement la moins explorée jusqu'à présent, est l'idée d'utiliser les modalités épistémiques comme éléments d'un langage de programmation. La programmation logique émergea sous le slogan <> et dans le paradigme de la programmation concurrente par contraintes, le lien est manifeste de manière très claire. Dans la première partie de cette thèse, nous explorons le rôle des modalités épistémiques, ainsi que celui des modalités spatiales qui leur sont étroitement liées, en tant que partie intégrante du langage de programmation et non simplement en tant que partie du meta-langage du raisonnement à propos des protocoles. La partie suivante explore une variante de la logique épistémique dynamique adaptée aux systèmes de transitions étiquetés. Contrairement à la partie précédente, on serait tenté de croire que tout ce qu'on pouvait dire à ce sujet a déjà été dit. Cependant, le nouvel ingrédient que nous proposons est un lien étroit entre la logique épistémique et la logique de Hennessy-Milner, cette dernière étant \emph{la} logique des systèmes de transitions étiquetés. Plus précisement, nous proposons une axiomatisation et une preuve d'un théorème de complétude faible, ce qui est conforme au principe général qu'on utilise pour des logiques telles que la logique dynamique mais nécessite des adaptations non triviales. La dernière partie de la thèse se concentre sur l'étude d'agents en interaction dans les processus concurents. Nous présentons une sémantique des jeux pour l'interaction d'agents qui rend manifeste le rôle de la connaissance et du flux d'information dans les interactions entre agents, et qui permet de contrôler l'information disponible aux agents en interaction. Nous utilisons les processus comme support de jeu et définissons des stratégies pour les agents de telle sorte que deux agents qui interagissent conformément à leurs stratégies respectives déterminent l'exécution du processus, rempla{\c}cant ainsi l'ordonnanceur traditionnel. Nous démontrons que des restrictions différentes sur les stratégies réprésentent des quantités d'information différentes disponibles à l'ordonnanceur. Ces restrictions sur les stratégies ont un aspect épistémique explicite, et nous présentons une logique modale pour les stratégies et une caractérisation logique de plusieurs restrictions possibles sur les stratégies. Ces trois approches d'analyse et de représentation de l'information épistémique en théorie de la concurrence apportent une nouvelle manière de comprendre la connaissance des agents dans des processus conncurrents, ce qui est vital dans le monde d'aujourd'hui, dans lequel les systèmes distribués composés de multiples agents sont omniprésents.