PhD vacancy Dynamic Epistemic Logics with Separation, Nancy (France)

Dynamic epistemic logics (DEL) model change of knowledge and belief in multi-agent systems. Bunched implication logics and separation logics model composing and dividing (separating) resources or information in data structures. Relations between BBI and DEL have recently been investigated. In such works modal logics have been proposed combining update modalities, epistemic modalities, and separating conjunctions and implications.

This PhD project aims to further integrate methods and tools of dynamic epistemic logic with methods and tools of bunched implications logics with separation. Among the different research directions that we envisage are: (i) defining new epistemic logics with separation, with corresponding structures and semantics; (ii) investigating the expressivity of such logics, how they contribute to modelling concurrency, and resolving decision problems for various fragments (model checking and satisfiability); (iii) defining proof calculi, both labelled and unlabelled, and investigating their properties.

The PhD supervisors for this project will be Hans van Ditmarsch and Didier Galmiche. Hans van Ditmarsch is senior researcher at CNRS, and he is heading the CELLO research group (Computational Epistemic Logic in LOrraine) at LORIA. Didier Galmiche is professor at the University of Lorraine, and he is heading the TYPES research group (Logic, Proof Theory and Programming) at LORIA.