Projet ANR-11-BS02-0004 – EQINOCS : Entropie et quantité d’information dans les modèles des systèmes computationnels
Programme : Blanc - SIMI 2 - Science informatique et applications (Blanc SIMI 2)
Année de financement : 2011
Coordinateur du projet : Monsieur Eugene ASARIN (UNIVERSITE DE PARIS 7)
Partenaires : Laboratoire Verimag; Institut de Recherche en Informatique Fondamentale; Laboratoire d'Algorithmique, Complexité et Logique; Laboratoire d'Informatique Gaspard-Monge
Montant : 374063.0 euros
Date de début : 2011
Durée : 48 mois
Résumé : EQINOCS : Entropie et Quantité d’INformation dans les mOdèles des systèmes ComputationnelSCe projet est centré sur l'analyse de l'entropie dans les modèles computationnels, en particulier ceux issus de la vérification. L'objectif est d'y adapter et d'y appliquer la notion d'entropie.
Enjeux et objectifs1.contribuer significativement à la théorie relative à l'entropie (ou l'entropie généralisée) de systèmes dynamiques associés à des transducteurs, des arbres, des jeux et des automates cellulaires et temporisés. 2.étudier les processus d'information dans les systèmes computationnels. Nous voulons mesurer la quantité d'information circulant dans ou générée par de tels systèmes. Outre un éclairage nouveau sur ceux-ci, cette étude fournirait de nouveaux outils pour mesurer leur niveau de sécurité et la qualité des protocoles de communication et suggèrerait une nouvelle approche de la compression de données. 3.identifier et explorer les applications à l'analyse et au model-checking quantitatifs des systèmes computationnels. Nous pensons que, par rapport aux approches probabilistes traditionnelles, les méthodes basées sur l'entropie ont deux avantages importants : elles ne nécessitent pas une connaissance exacte de tous les évènements du système et elles peuvent être beaucoup plus simples à mettre en œuvre.
MéthodesNous appliquerons les techniques de la théorie d'automates et celle de codes, de la théorie d'information et la complexité de Kolmogorov, de la dynamique symbolique et théorie ergodique, de la vérification, de l'analyse fonctionnelle des opérateurs linéaires positifs, de la combinatoire, de l'analyse numériques. Nous implémenterons et testerons les algorithmes développés sur des études des cas.
Résumé de la soumission : Ce projet est centré sur l'analyse de l'entropie pour les modèles computationnels. L'objectif est d'adapter et d'appliquer la notion d'entropie aux modèles computationnels issus du domaine de la vérification. L'analyse permettra de progresser dans trois directions. 1: Nous souhaitons obtenir des contributions théoriques significatives concernant l'entropie (ou l'entropie généralisée) de systèmes dynamiques associés à des transducteurs, des arbres, des jeux et des automates cellulaires et temporisés. 2: Nous voulons aussi étudier les processus d'information dans les systèmes computationnels. Il est bien connu que les systèmes computationnels traitent et transmettent de l'information. Dans ce projet nous voulons mesurer la quantité d'information circulant dans ou génrérée par de tels systèmes. Ceci donnerait un éclairage nouveau aux systèmes computationnels, fournirait de nouveaux outils pour mesurer le niveau de sécurité des systèmes et la qualité des protocoles de communication, et donnerait une nouvelle approche pour la compression de données. 3:Nous identifierons et explorerons les applications à l'analyse quantitative et au model-checking quantitatif des systèmes computationnels. Nous pensons que, en comparaison avec les approches probabilistes traditionnelles, les méhodes basées sur l'entropie ont deux avantages importants : elles ne nécessitent pas une connaisance exacte de tous les évènements du système, et elles peuvent être beaucoup plus simples à implémenter.
Résultats : Résultat marquant : Dynamique symbolique temporisée et sa théorie spectrale
     Les langages temporisés réguliers ont été représentés par des systèmes dynamiques de décalage. Un opérateur intégral linéaire positif sur un espace de Banach est naturellement associé à ce système. Cet opérateur contient l’information essentielle sur le langage : son rayon spectral caractérise l’entropie du langage, sa résolvante correspond à la fonction génératrice du langage. L’opérateur possède un trou spectral ce qui garantit la convergence des simples algorithmes numériques.  
Fait marquant : un colloque co-organisé. 
Ce colloque, qui  apparait sur la page Web de l’AMS comme “PIMS/EQINOCS Workshop on Automata and Ergodic Theory” aura lieu à Vancouver  en juin 2013 et mettra ensemble les mathématiciens et les informaticiens travaillant sur les thèmes proches à notre projet.
Perspectives : Nous attendons des nouveaux résultats sur l'entropie pour des nombreuses classes de systèmes computationnels et leurs applications théoriques et pratiques.
Publications et brevets : 1.Asarin E., Basset N., Degorre A., Perrin D. Generating functions of timed languages. - MFCS’2012 :124-135
2.E. Asarin, N. Basset, M.-P. Béal, A. Degorre, D. Perrin: Toward a Timed Theory of Channel Coding. FORMATS 2012: 27-42  
3.R. Bozianu, C. Dima,C. Enea. Model-checking an Epistemic ?-calculus with Synchronous and Perfect Recall Semantics TARK 2013
4.Asarin E., Basset N., Degorre A., Spectral gap in timed automata. Submitted to FORMATS 2013
5.L. Bienvenu, B. Monin. von Neumann's biased coin revisited. LICS 2012  :145-154
6.J. Cervelle: Covering Space in the Besicovitch Topology. LATA 2012: 169-178
7.D. P. Guelev, C. Dima: Epistemic ATL with Perfect Recall, Past and Strategy Contexts. CLIMA (Computational Logic in Multi-Agent Systems) 2012: 77-93
8.N. Basset: A maximal entropy stochastic process for a timed automaton. ICALP 2013
9.Slissenko, A., Towards analysis of information structure of computations, International Conf. Philosophy, Mathematics, Linguistics: Aspects of Interaction (PhML'2012), Saint  Petersburg, Russia,  2012, 182—192
10.J.-F.  Kempf, M. Bozga, O. Maler: As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. TACAS 2013: 385-400
11.A. Donzé, T. Ferrère, Oded Maler, Efficient Robust Monitoring for STL. CAV 2013
12.N. Basset : Counting and generating permutations using timed languages. Submitted to MFCS 2013 
13. N. Aubrun and M.-P. Béal,Tree algebra of sofic tree languages, submitted