Agi Kurucz

On the complexity of KxK, with and without the diagonal constant

KxK, the bimodal logic of all two-dimensional product frames, is known to be decidable. However, only nonelementary decision algorithms for KxK-satisfiability are known, and so far the best lower bound has been NEXPTIME (by Marx and Mikulas 2001). Recently, Göller, Jung, and Lohrey (LICS 2012) showed that KxK-satisfiability cannot be done in elementary time. Kikot and Kurucz 2011 showed that `KxK plus diagonal constant' is even worse, its satisfiability problem is undecidable.

The talk is about the proofs of these two recent results.