STIC AmSud – Dylo-MPC

Dylo-MPC – Dynamic Logics: Madel Theory, Proof Theory and Computational Complexity

Pays impliqués : France, Argentine, Brésil

Projets Stic_AmSud

Au cours du projet, nous ferons progresser la compréhension d’une nouvelle famille de logiques modales appelée logiques dynamiques. Les logiques dynamiques sont caractérisées par l’inclusion d’opérateurs modaux qui peuvent modifier le modèle dans lequel ils sont évalués. Cette caractéristique les a rendus particulièrement adaptés à la description de scénarios d’évolution comme, par exemple, l’évolution temporelle d’un réseau de communication, où les connexions sont créées et éliminées de manière dynamique, en changeant constamment la topologie réelle. Plusieurs logiques dynamiques différentes ont été étudiées par les membres du projet, mais il manque encore une vue d’ensemble, et un certain nombre de questions importantes restent ouvertes, allant des caractérisations théoriques appropriées du modèle à une compréhension adéquate de la façon de définir les calculs de test pour ces logiques, qui ne sont normalement pas fermées dans le cadre de substitutions uniformes. Le projet vise à rassembler les forces des quatre équipes de recherche internationales pour unifier les résultats existants et tenter de répondre à ces questions ouvertes.

Coordinateurs :
Carlos Eduardo Areces, Universidad Nacional de Córdoba, Argentina [UNC-AR],  Facultad de Matemática, Astronomía, Física y Computación, ARGENTINA

Mario Roberto Folhadela Benevides, Universidade Federal do Rio de Janeiro, Brazil [UFRJ-BR]
Departamento de Ciência da Computação, BRASIL
Lutz Strassburger, Laboratoire d’Informatique de l’Ecole Polytechnique and CNRS, FRANCIA
Stéphane Demri, ENS Paris-Saclay and CNRS [LSV-FR] Laboratoire Spécification et Vérification, FRANCIA