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

• [UNC-AR] Carlos Areces,
  Universidad Nacional de Córdoba, Argentina
• [UFRJ-BR] Mario Roberto Benevides,
  Universidade Federal do Rio de Janeiro, Brazil
• [LIX-FR] Lutz Strassburger,
  INRIA Saclay, France
• [LSV-FR] Stéphane Demri,
  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.

• Stéphane Demri, Raul Fervari, Alessio Mansutti. Internal Proof Calculi for Modal Logics with Separating Conjunction. Journal of Logic and Computation, Oxford University Press (OUP), 2021, 31 (3), pp.832-891.
• Stéphane Demri, Karin Quaas. Concrete domains in logics: a survey. ACM SIGLOG News, ACM, 2021, 8 (3), pp.6-29.
• Stéphane Demri, Étienne Lozes, Alessio Mansutti: Internal Calculi for Separation Logics. CSL 2020: 19:1-19:18.
• Francesco Belardinelli, Stéphane Demri. Strategic Reasoning with a Bounded Number of Resources: the Quest for Tractability. Artificial Intelligence, Elsevier, 2021, 300, pp.103557.
• 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.
• Matteo Acclavio, Davide Catta, Lutz Strassburger. Game Semantics for Constructive Modal Logic, Automated Reasoning with Analytic Tableaux and Related Methods, 12842, Springer International Publishing, pp.428-445, 2021, Lecture Notes in Computer Science.
• Lutz Strassburger, Dominic Hughes, Jui-Hsuan Wu. Combinatorial Proofs and Decomposition Theorems for First-order Logic, 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13.
• Sonia Marin, Marianela Morales, Lutz Strassburger. A fully labelled proof system for intuitionistic modal logics, Journal of Logic and Computation, Oxford University Press (OUP), 2021, 31 (3), pp.998-1022.
• Matteo Acclavio, Ross Horne, Lutz Strassburger. Logic beyond formulas: a proof system on graphs, LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.38-52,
• Marianna Girlando, Lutz Strassburger. MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description), IJCAR 2020 - 10th International Joint Conference, Jul 2020, Paris, France. pp.398-407, ⟨10.1007/978-3-030-51054-1_25⟩
• Benjamin Ralph, Lutz Strassburger. Towards a Combinatorial Proof Theory, TABLEAUX 2019 - 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2019, London, United Kingdom. pp.259-276
• Matteo Acclavio, Lutz Strassburger. On Combinatorial Proofs for Modal Logic, TABLEAUX 2019 - 28t International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2019, London, United Kingdom. pp.223-240.
• 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 Space of Interaction, LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2021, Rome, France. pp.1-13,.
• Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni: The Machinery of Interaction. PPDP 2020: 4:1-4:15.
• Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The (In)Efficiency of interaction, Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), pp.1-33.
• Mario Benevides, Alexandre Madeira, Manuel A. Martins, Graded epistemic logic with public announcement. J. Log. Algebraic Methods Program. 125: 100732 (2022).
• Mario Benevides, Alexandre Madeira, Manuel A. Martins, Adding Proof Calculi to Epistemic Logics with Structured Knowledge. FSEN 2021: 53-68
• 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.
• Carlos Areces, Hans van Ditmarsch, Raul Fervari, Bastien Maubert and Francoise Schwarzentruber. Copy and Remove as Dynamic Operators, Journal of Applied Non-Classical Logics (JANCL), volume 31, number 3-4, pages 181-220, 2021.
• Carlos Areces and Raul Fervari. Axiomatizing Hybrid XPath with Data. Logical Methods in Computer Science (LMCS), volume 17, issue 3, 2021.
• Raul Fervari, Franco Trucco and Beta. Ziliani. Verification of Dynamic Bisimulation Theorems in Coq. Journal of Logical and Algebraic Methods in Programming (JLAMP), volume 120, article 100642, 2021.
• Carlos Areces, Raul Fervari, Andres Saravia and Fernando Velázquez-Quesada. Uncertainty-Based Semantics for Multi-Agent Knowing How Logics. In Proceedings of 18th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2021), pages 23-37, EPTCS 335, 2021.
• 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.
• Raul Fervari, Fernando Velázquez-Quesada and Yanjing Wang. Bisimulations for Knowing How Logics. The Review of Symbolic Logic (RSL), 2021.
• Raul Fervari and Fernando Velázquez-Quesada. Introspection as an Action in Relational Models. Journal of Logical and Algebraic Methods in Programming (JLAMP), volume 108, pages 1-23, 2019.