Structured Interactive Scores

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 m...

Full description

Bibliographic Details
Main Author: Mauricio, Toro
Language:FRE
Published: Université Sciences et Technologies - Bordeaux I 2012
Subjects:
Online Access:http://tel.archives-ouvertes.fr/tel-00736021
http://tel.archives-ouvertes.fr/docs/00/73/60/21/PDF/phdToro.pdf
http://tel.archives-ouvertes.fr/docs/00/73/60/21/ANNEX/toro-phd-defense-light.pdf
id ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-00736021
record_format oai_dc
collection NDLTD
language FRE
sources NDLTD
topic [INFO:INFO_SD] Computer Science/Sound
[INFO:INFO_CL] Computer Science/Computation and Language
[INFO:INFO_AI] Computer Science/Artificial Intelligence
interactive scores
concurrent constraint programming
ntcc
temporal constraints
spellingShingle [INFO:INFO_SD] Computer Science/Sound
[INFO:INFO_CL] Computer Science/Computation and Language
[INFO:INFO_AI] Computer Science/Artificial Intelligence
interactive scores
concurrent constraint programming
ntcc
temporal constraints
Mauricio, Toro
Structured Interactive Scores
description 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.
author Mauricio, Toro
author_facet Mauricio, Toro
author_sort Mauricio, Toro
title Structured Interactive Scores
title_short Structured Interactive Scores
title_full Structured Interactive Scores
title_fullStr Structured Interactive Scores
title_full_unstemmed Structured Interactive Scores
title_sort structured interactive scores
publisher Université Sciences et Technologies - Bordeaux I
publishDate 2012
url http://tel.archives-ouvertes.fr/tel-00736021
http://tel.archives-ouvertes.fr/docs/00/73/60/21/PDF/phdToro.pdf
http://tel.archives-ouvertes.fr/docs/00/73/60/21/ANNEX/toro-phd-defense-light.pdf
work_keys_str_mv AT mauriciotoro structuredinteractivescores
_version_ 1716394592104873984
spelling ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-007360212013-01-07T16:41:03Z http://tel.archives-ouvertes.fr/tel-00736021 http://tel.archives-ouvertes.fr/docs/00/73/60/21/PDF/phdToro.pdf http://tel.archives-ouvertes.fr/docs/00/73/60/21/ANNEX/toro-phd-defense-light.pdf Structured Interactive Scores Mauricio, Toro [INFO:INFO_SD] Computer Science/Sound [INFO:INFO_CL] Computer Science/Computation and Language [INFO:INFO_AI] Computer Science/Artificial Intelligence interactive scores concurrent constraint programming ntcc temporal constraints 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. 2012-09-25 FRE PhD thesis Université Sciences et Technologies - Bordeaux I