Dynamic Logics (Reloaded)

Dynamic Logics (Reloaded)

CLIMAT-AmSud, STIC-AmSud and MATH-AmSud are regional scientific-technological cooperation programs in which Argentina, Bolivia, Brazil, Chile, Colombia, Ecuador, Paraguay, Peru, Uruguay, Venezuela and France participate. Their objective is to promote and strengthen collaboration and the creation of research-development networks in the field of information and communication sciences and technologies (STIC), mathematics (MATH) and climate change and climate variability (CLIMAT) through the implementation of joint projects.

The Dynamic Logics (Reloaded) project has been selected as a STIC-AmSud project for the years 2024 and 2025, as a collaboration between research teams from France, Brazil, Chile and Argentina.

Description

Dynamic logics are those that include operators that can modify the model in which a formula is 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:

  • Advance our knowledge on the model theory of dynamic logics.
  • Design suitable proof calculi.
  • Investigate complexity issues.

Members

  • Facultad de Matemática, Astronomía, Física y Computación, Universidad Nacional de Córdoba, Argentina [AR-UNC]
    • Carlos Areces, Senior Researcher & Project Coordinator.
    • Luciana Benotti, Senior Researcher.
    • Raul Fervari, Junior Researcher.
    • Guillaume Hoffmann, Junior Researcher.
    • Valentín Cassano, Junior Researcher.
    • Mallku Soldevila, Junior Researcher.
    • Juliana Putero, PhD Student.
    • Andrés R. Saravia, PhD Student.
    • Danae Dutto, PhD Student.
    • Antonio Mondejar, PhD Candidate.
  • Instituto de Computação, Universidade Federal Fluminense, Brazil [BR-UFF]
    • Mario R. F. Benevides, Senior Researcher & Project Coordinator.
    • Bruno Lopes Vieira, Junior Researcher.
    • Vitor P. Machado, Junior Researcher.
    • Uéverton dos Santos Souza, Junior Researcher.
    • Anna C. N. Oliveira, Ph.D. student.
    • Renato Reis Leme, D.Sc. Student.
    • Maurício da Silva Pires, D.Sc. Student.
    • Allan Patrick de Freitas Santanna, M.Sc. Student.
    • Matheus Guimaraes Robaina, M.Sc. Student.
    • Caio Serra de Mello, M.Sc. Student.
  • Institute for Mathematical and Computational Engineering, Universidad Católica de Chile y Millennium Institute for Foundational Research on Data [CH-PUC]
    • Pablo Barceló, Senior Researcher & Project Coordinator.
    • Domagoj Vrgoc, Senior Researcher.
    • Jocelyn Dunstan, Senior Researcher.
    • Juan Reutter, Senior Researcher.
    • Alexander Kozachinskiy, Junior Researcher.
  • Inria Saclay, France [FR-SAC]
    • Lutz Strassburger, Senior Researcher & Project Coordinator.
    • Dale Miller, Senior Researcher.
    • Noam Zeilberger, Senior Researcher.
    • Beniamino Accattoli, Junior Researcher.
    • Giti Omidvar, PhD Student.
    • Marianela Morales, PhD Student.
    • Adrienne Lancelot, PhD Student.
    • Jiu-Hsuan Wu, PhD Student.
    • Farah Al Wardani, PhD student.
  • Laboratoire Méthodes Formelles (LMF) [FR-LMF]
    • Stéphane Demri, Senior Researcher & Project Coordinator.
    • Benedikt Bollig, Senior Researcher.
    • Philippe Schnoebelen, Senior Researcher.
    • Dietmar Berwanger, Senior Researcher
    • Isa Vialard, PhD student.

Exchanges

During 2024, and given the economic and political situation in Argentina, the AR-UNC research team did not receive funds for exchanges. As a result, and to try to maximize collaboration possibilities, it was decided that exchanges would be taking place in Argentina.

The following research exchanges have been organized during 2024 in the framework of the project:

  • Jocelyn Dunstan, Senior Researcher [CH-PUC], visited [AR-UNC] from May 29th to June 2nd.
  • Lutz Strassburger, Senior Researcher and Project Coordinator [FR-SAC], visited [AR-UNC] from September 23rd to October 5th.
  • Mario R. F. Benevides, Senior Researcher and Project Coordinator [BR-UFF], visited [AR-UNC] from September 27th to October 7th.
  • Bruno Lopes Vieira, Junior Researcher [BR-UFF], visited [AR-UNC] from September 27th to October 7th.
  • Pablo Barceló Senior Researcher and Project Coordinator [CH-PUC], visited [AR-UNC] from September 29th to October 4th.
  • Alexander Kozachinskiy, Junior Researcher [CH-PUC], visited [AR-UNC] from September 29th to october 4th.
  • Juan Reutter, Senior Researcher [CH-PUC], visited [AR-UNC] from September 29th to October 4th.
  • Raul Fervari, Junior Researcher [AR-UNC], visited [FR-LMF] and [FR-SAC] from October 18th to November 3rd. This visit was possible thanks to funds from MISSION and SINFIN.
  • Noam Zeilberger, Senior Researcher [FR-SAC] visited [AR-UNC] from October 17th to November 1st.

The following research exchanges have been organized during 2025 in the framework of the project:

  • Pablo Barceló Senior Researcher and Project Coordinator [CH-PUC], visited [FR-LMF] from May 18th to May 25th.
  • Lutz Strassburger, Senior Researcher and Project Coordinator [FR-SAC], visited [CH-PUC] from September 13th to September 22nd.
  • Mario Benevides, Senior Researcher and Project Coordinator [BR-UFF], visited [CH-PUC] from September 14th to September 24th.
  • Dietmar Berwanger, Senior Researcher at [FR-LMF], visited [CH-PUC] from September 12th to September 18th.
  • Raul Fervari, Junior Researcher [AR-UNC], visited [FR-LMF] from July 1st to December 31st. This visit was possible thanks to funds from the program Jean D'Alembert, Universite Paris-Saclay.
  • Danae Dutto, PhD Student [AR-UNC]; visited [CH-PUC] from September 14th to September 19th.
  • Antonio Mondejar, PhD Candidate [AR-UNC]; visited [CH-PUC] from September 14th to September 19th.

Outreach Activities

The following activities were organized in the framework of the project:

  • First Dynamic Logics Workshop [link]
    Participants: Carlos Areces [AR-UNC], Pablo Barceló [CH-PUC], Danae Dutto [AR-UNC], Alexander Kozachinskiy [CH-PUC], Raul Fervari [AR-UNC], Lutz Strassburger [FR-SAC], Mario Benevides [BR-UFF], Bruno Lopes [BR-UFF], Valentin Cassano [AR-UNC], Juan Reutter [CH-PUC].
  • Training Course Exercising Citizenship in the Age of Artificial Intelligence [link]
    Participants: Luciana Benotti [AR-UNC], Jocelyn Dunstan [CH-PUC].
  • Dagstuhl Seminar 24341 Proof Representations: From Theory to Applications [link]
    Participants: Carlos Areces [AR-UNC], Lutz Strassburger [FR-SAC].
  • BIRS Seminar 24341 Proof Representations: From Theory to Applications [link]
    Participants: Carlos Areces [AR-UNC], Lutz Strassburger [FR-SAC].
  • Second Dynamic Logics Workshop [link]
    Participants: Pablo Barceló [CH-PUC], Danae Dutto [AR-UNC], Antonio Mondejar [AR-UNC], Alexander Kozachinskiy [CH-PUC], Raul Fervari [AR-UNC], Lutz Strassburger [FR-SAC], Dietmar Berwanger [FR-MLF], Mario Benevides [BR-UFF].

Publications

The following publications have been developed in the framework of this project

  • B. Icard, R. Fervari: Beyond the Spell: A Dynamic Logic Analysis of Misdirection. CoRR abs/2401.14516 (2024)
  • C. Areces, V. Cassano, R. Fervari: Data-Aware Hybrid Tableaux. CoRR abs/2406.12090 (2024)
  • B. Bednarczyk, S. Demri, R. Fervari, A. Mansutti: On Composing Finite Forests with Modal Logics. ACM Trans. Comput. Log. 24(2): 12:1-12:46 (2023)
  • S. Demri, R. Fervari: Model-Checking for Ability-Based Logics with Constrained Plans. AAAI 2023: 6305-6312
  • V. Cassano, R. Fervari, C. Areces, P. Castro: Algebraic tools for default modal systems. J. Log. Comput. 33(6): 1301-1325 (2023)
  • C. Areces, V. Cassano, D. Dutto, R. Fervari: Data Graphs with Incomplete Information (and a Way to Complete Them). JELIA 2023: 729-744
  • P. Barceló, A. Kozachinskiy, A. Widjaja Lin, V. Podolskii: Logical Languages Accepted by Transformer Encoders with Hard Attention. ICLR 2024
  • M. Lanzinger, P. Barceló: On the Power of the Weisfeiler-Leman Test for Graph Motif Parameters. ICLR 2024
  • P. Barceló, D. Figueira, R. Morvan: Separating Automatic Relations. MFCS 2023: 17:1-17:15
  • M. Girlando, R. Kuznets, S. Marin, M. Morales, L. Strassburger: A Simple Loopcheck for Intuitionistic K. WoLLIC 2024: 47-63
  • W. Ouedraogo, G. Scherer, L. Strassburger: Coqlex: Generating Formally Verified Lexers. Art Sci. Eng. Program. 8(1) (2024)
  • M. Sadrzadeh, L. Strasburger: Lambek Calculus with Banged Atoms for Parasitic Gaps. WoLLIC 2024: 193-209
  • A. Das, E. Pimentel, L. Strasburger, R. Martinot: Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341). Dagstuhl Reports 14(8): 1-23 (2024)
  • M. Girlando, R. Kuznets, S. Marin, M. Morales, L. Strassburger: Intuitionistic S4 is decidable. LICS 2023: 1-13
  • S. Demri, P. Andrzej Walega: Computational Complexity of Standpoint LTL. CoRR abs/2408.08557 (2024)
  • H. Maina, L. Alonso Alemany, G. Ivetta, M. Rajngewerc, B. Busaniche, L. Benotti: Exploring Stereotypes and Biases in Language Technologies in Latin America. Commun. ACM 67(8): 54-56 (2024)
  • C. Areces, L. Benotti, F. Bulgarelli, E. Echeveste, N. Finzi: Leveraging Language Models and Automatic Summarization in Online Programming Learning Environments. Commun. ACM 67(8): 86-87 (2024)
  • J. Eisenschlos, H. Maina, G. Ivetta, L. Benotti: Selectively Answering Visual Questions. ACL (Findings) 2024: 4219-4229
  • D. Arroyuelo, A. Hogan, G. Navarro, J. Reutter, D. Vrgoc: Tackling Challenges in Implementing Large-Scale Graph Databases. Commun. ACM 67(8): 40-44 (2024)
  • D. Arroyuelo, B. Bustos, A. Gómez-Brandón, A. Hogan, G. Navarro, J. Reutter: Worst-Case-Optimal Similarity Joins on Graph Databases. Proc. ACM Manag. Data 2(1): 39:1-39:26 (2024)
  • R. Fervari and B. Icard. Arbitrary Radical Upgrades. International Workshop on Reconfigurable Transition Systems: Semantics, Logics and Applications (ReacTS’24), SEFM 2024 Collocated Workshops, vol 15551 of LNCS, pages 36-49. Springer (2024).
  • C. Areces, R. Fervari, A. Saravia and F. Velázquez-Quesada. Uncertainty-Based Knowing How Logic. Journal of Logic and Computation (JLC), volume 35, issue 1, pages 1-35, (2025).
  • S. Demri and R. Fervari. On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025), (2025).
  • P. F. Castro, P. R. D’Argenio and R. Fervari. How Lucky Are You to Know Your Way? A Probabilistic Approach to Knowing How Logics. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025), (2025).
  • R. Fervari, D. Figueiredo and M. Martins. Graded Relation Updates in Modal Logic. In Logic, Language, Information and Computation (WoLLIC), volume 15942 of LNCS, pages 278–292. Springer (2025).
  • S. Demri, L. Doyen and R. Fervari. Knowing-How Reasoning with Budgets Recasted: Universal Reachability Problem on VASS. In 19th International Conference on Reachability Problems (RP 2025), (2025).
  • C. Areces, V. Cassano, D. Dutto and R. Fervari. Sequent Calculi for Data-Aware Modal Logics. In 20th International Symposium on Logical and Semantic Frameworks, with Applications (LSFA 2025), (2025).
  • V. Prabhakaran, S. Dev, L. Benotti, D. Hershcovich, Y. Cao, et al. Proceedings of the 3rd Workshop on Cross-Cultural Considerations in NLP (C3NLP 2025). ACL, (2025)
  • M. Gómez, J. Dabbah, L. Benotti. A workshop on artificial intelligence biases and its effect on high school students' perceptions. International Journal of Child-Computer Interaction, Vol. 43, 2025)
  • M. Arenas, P. Barceló, A. Kozachinskiy, M. Romero, B. Subercaseaux. On Computing Probabilistic Explanations for Decision Trees. J. Artif. Intell. Res. 83 (2025)
  • P. Barceló, A. Kozachinskiy, M. Romero, B. Subercaseaux, J. Verschae. Explaining k-Nearest Neighbors: Abductive and Counterfactual Explanations. Proc. ACM Manag. Data 3(2): 97:1-97:26 (2025)
  • X. Huang, M. Romero Orth, P. Barceló, M. Bronstein, I. Ceylan: Link Prediction with Relational Hypergraphs. Trans. Mach. Learn. Res. 2025 (2025)
  • V. Belle, P. Barceló: A Uniform Language for Safety, Robustness and Explainability. JELIA (1) 2025: 3-12
  • S. Demri, K. Quaas: Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures. Log. Methods Comput. Sci. 21(2) (2025)

Funding

The project received the following funds during 2024:

  • From MEAE (France): 2500 euros.
  • From INRIA (France): 5000 euros.
  • From CAPES (Brazil): 6000 euros.
  • From ANID (Chile): 5500 euros.
  • From MinCyT (Argentina): 0 euros.

The project received the following funds during 2025:

  • From MEAE (France): 2000 euros.
  • From INRIA (France): 5000 euros.
  • From CAPES (Brazil): 6000 euros.
  • From ANID (Chile): 6000 euros.
  • From SiCYT (Argentina): 5000 euros.