Entropie et quantité d’information dans les modèles des systèmes computationnels – EQINOCS

Nous 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é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.

Nous attendons des nouveaux résultats sur l'entropie pour des nombreuses classes de systèmes computationnels et leurs applications théoriques et pratiques.

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

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.