Hennessy-Milner Properties for (Modal) Bi-intuitionistic Logic

Abstract

Bi-intuitionistic logic is an extension of intuitionistic propositional logic with a binary operator that is residuated with respect to disjunction. Our main result is a Hennessy-Milner property for biintuitionistic logic interpreted over certain classes of Kripke models. We generalise this to obtain a corresponding result for modal bi-intuitionistic logic. Our main technical tools are a categorical duality between (modal) descriptive Kripke frames and (modal) bi-Heyting algebras, and the use of behavioural equivalence. Show more