DaLí 2025: The 6th Workshop on Dynamic Logic - New Trends and Applications

Title: Towards a PDL Framework for Reasoning about Causality
ABSTRACT: Causality has long been a central topic in philosophical discourse. Recent advances by researchers such as Halpern and Pearl have introduced formal tools that use structural equations to model causal dependencies between variables. Observing the parallels between variables and propositions—as well as the inherently dynamic nature of interventions—we ask: why not use propositional dynamic logic (PDL) to study causality? To explore this idea, we propose causal propositional dynamic logic (CPDL) as a framework for representing and reasoning about dependency structures between propositions and the changes in their truth values before and after different dynamic actions. We then extend this framework to an epistemic setting to capture changes in agents’ epistemic states. By fully separating semantic content from syntax, our framework supports model-independent causal reasoning, and we establish validities that hold across all models. In addition, we provide a complete axiomatization for epistemic CPDL and prove its decidability. Furthermore, we demonstrate the flexibility of our approach by extending it to include the inverse event operator, define sufficient and actual causes, and express causal relations between complex propositions. A detailed comparison with related models is included, highlighting the distinct advantages of the PDL-based approach. This is joint work with Xiaoxuan Fu and Zhiguang Zhao.

Title: Paraconsistency and Program Logics
ABSTRACT: Program logics provide methods and tools for systematic reasoning about how a program works and to prove, in a compositional way, a number of guarantees about its behaviour. Modelling complex information systems, however, often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. To meet such a challenge, in recent joint work with Juliana Cunha and Alexandre Madeira, we have developed a variant of transition systems endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values. Such structures are called paraconsistent transition systems, the qualifier stressing a connection to paraconsistent logic, a logic that takes inconsistent information as potentially informative. This lecture reports on this research initiative, putting a specific emphasis on its potential for developing more flexible program logics.

Title: Dynamic Logics for Data Exchange
ABSTRACT: I focus on a relatively new family of logics, modelling communication acts in which whole ‘chunks’ of data are being exchanged: agents or groups can access all information stored at specific locations. The data that is being exchanged may be propositional, non-propositional (numerical, visual, etc.) or a mixture of both. For this, I look at extensions of Dynamic Epistemic Logic with dynamic modalities for interactions by which agents gain (or are given) access to information sources (thus being potentially able to 'read' all the data available at that source). Formally, these correspond to dynamic changes of a model, by which (some or all of) the epistemic relations are replaced by intersections of (some or all of) the current relations. I briefly trace the history of this line of research, then present a general setting, with motivating examples. I give complete axiomatizations and decidability results. Time-permitting, I discuss the technical challenges and innovations involved in extending these axiomatizations to operators such as common knowledge, ''epistemic superiority", or ''knowledge what" (i.e., knowing a specific piece of non-propositional data, e.g. somebody's password).