Modal Logic and Separation: the Surprising Difference Between Binary and Ternary Trees

Speaker(s)

Jędrzej Kołodziejski

Affiliation

University of Warsaw

Language of the talk

English

Date

Nov. 19, 2025, 2:15 p.m.

Room

room 5440

Title in Polish

Modal Logic and Separation: the Surprising Difference Between Binary and Ternary Trees

Seminar

Seminar Automata Theory

---

Assume logical formulae φ,φ' which are mutually exclusive in the sense that φ entails ¬φ'. A separator is a formula ψ such that φ entails ψ and ψ entails ¬φ'. We will look at separation in the context of modal logic ML interpreted over binary trees and ternary (or higher arity) trees.

Over binary trees ML has the Craig interpolation property: every mutually exclusive φ,φ' are separated by some ψ which only uses common symbols of φ,φ'. On the contrary, over ternary trees deciding existence of such a ψ for given φ,φ' is coNEXPTIME-complete.  If time permits,  we will also discuss µ-ML, the extension of ML with fixpoints. One can ask if given φ,φ' in µ-ML are separated by some ψ in ML. This problem is EXPTIME-complete over binary trees, but 2-EXPTIME-complete over ternary ones.

This is joint work with Jean Christoph Jung.

---