[English Version] []

Dynamic Logics: Model Theory, Proof Theory and Computational Complexity [DyLo-MPC]

DyLo-MPC is a STIC AmSud proyect for the period 2020-2021 between the Universidad Nacional de Córdoba (Argentina), the Universidade Federal do Rio de Janerio (Brazil), INRIA Saclay (France), and the Laboratoire Spécification et Vérification (France).



Dynamic logics are those that include modal operators that can modify the model in which they are being evaluated. Different dynamic logics have been investigated in the past, but a general perspective is still missing. In this project we aim to pursue the following goals.

  • [G1] Advance our knowledge on the model theory of dynamic logics by:
    • a. Developing general notions of model equivalence (e.g., bisimulations)
    • b. Relating these notions to their counterpart as logic games.
    • c. Understanding the relation between dynamic "moves" in a graph game, and the notions mentioned above.
    • d. Proving characterizations of these logics as fragments of classical logics (e.g., "van Benthem characterization theorems") using the notions of model equivalence previously introduced.
  • [G2] Design suitable proof calculi by:
    • a. Understanding how to cope with logics which are not closed under uniform substitution.
    • b. Defining the role of hybridization techniques (e.g., the use of nominals and labeling operators) in the context of evolving models.
    • c. Demonstrating general completeness results (e.g., stable under the addition of axioms with particular properties).
    • d. Developing general tableau calculi that can lead to implementations.
    • e. Defining translations into classical logics.
  • [G3] Investigate complexity issues by:
    • a. Understanding the relation between dynamic operators and binders/quantifiers.
    • b. Delineating the borderline between decidable and undecidable fragments.
    • c. Proposing weak dynamic operators that give rise to decidable logics.


  • At [UNC-AR]
    • Carlos Areces, Senior Researcher.
    • Luciana Benotti, Senior Researcher.
    • Raul Fervari, Junior Researcher.
    • Beta Ziliani, Junior Researcher.
    • Valentín Cassano, Junior Researcher.
    • Nahuel Seiler, PhD Student.
    • Francisco Trucco, PhD Student.
    • Mauricio Mazuecos, PhD Student.
  • At [UFRJ-BR]
    • Mario Benevides, Senior Researcher.
    • Paulo Veloso, Senior Researcher.
    • Sheila Veloso, Senior Researcher.
    • Bruno Lopes Vieira, Junior Researcher.
    • Vitor Pereira Machado, PhD Student.
    • Isaque Macalam Saab Lima, PhD Student.
  • At [LIX-FR]
    • Lutz Strassburger, Senior Researcher.
    • Gabriel Scherer, Junior Researcher.
    • Beniamino Accattoli, Junior Researcher.
    • Marianela Morales, PhD Student.
    • Maico Leberle, PhD Student.
  • At [LSV-FR]
    • Stéphane Demri, Senior Researcher.
    • Sylvain Schmitz, Senior Researcher.
    • Benedikt Bollig, Senior Researcher.
    • David Baelde, Junior Researcher.
    • Alessio Mansutti, PhD Student.

Relevant Publications

  • Stéphane Demri, Étienne Lozes, Alessio Mansutti: Internal Calculi for Separation Logics. CSL 2020: 19:1-19:18.
  • Bartosz Bednarczyk, Stéphane Demri, Alessio Mansutti: A Framework for Reasoning about Dynamic Axioms in Description Logics. IJCAI 2020: 1681-1687.
  • Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti: Modal Logics with Composition on Finite Forests: Expressivity and Complexity. LICS 2020: 167-180.
  • Stéphane Demri, Raul Fervari: The power of modal separation logics. J. Log. Comput. 29(8): 1139-1184 (2019).
  • Stéphane Demri, Raul Fervari, Alessio Mansutti: Axiomatising Logics with Separating Conjunction and Modalities. JELIA 2019: 692-708.
  • Sylvain Schmitz: The Parametric Complexity of Lossy Counter Machines. ICALP 2019: 129:1-129:15
  • Petr Jancar, Sylvain Schmitz: Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete. LICS 2019: 1-12
  • Jérome Leroux, Sylvain Schmitz: Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. LICS 2019: 1-13
  • Sylvain Schmitz, Georg Zetzsche: Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets. RP 2019: 193-201
  • Roman Kuznets, Lutz Strassburger: Maehara-style modal nested calculi. Arch. Math. Log. 58(3-4): 359-385 (2019).
  • Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni: The Machinery of Interaction. PPDP 2020: 4:1-4:15
  • Vitor Machado, Mario Benevides: Populational Announcement Logic (PPAL). LSFA 2020: 105-123.
  • Leandro Gomes, Alexandre Madeira, Mario Benevides: Logics for Petri Nets with Propagating Failures. FSEN 2019: 145-157.
  • Valentin Cassano, Raul Fervari, Guillaume Hoffmann, Carlos Areces, Pablo Castro: A Tableaux Calculus for Default Intuitionistic Logic. CADE 2019: 161-177.
  • Valentin Cassano, Raul Fervari, Carlos Areces, Pablo Castro: Interpolation and Beth Definability in Default Logics. JELIA 2019: 675-691.
  • Pablo Castro, Valentin Cassano, Raul Fervari, Carlos Areces: An Algebraic Approach for Action Based Default Reasoning. TARK 2019: 91-105.
  • Pablo Castro, Valentin Cassano, Raul Fervari, Carlos Areces: Default Modal Systems as Algebraic Updates. DaLI 2020.
  • Pablo Castro, Valentin Cassano, Raul Fervari and Carlos Areces: Deontic Action Logics via Algebra. DEON2020/2021.
  • Raul Fervari, Francisco Trucco, Beta Ziliani: Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq. DaLi 2019: 3-18