An automaton approach to Kripke semantics

We study the satis ability problem over axiomatic extensions of modal logic K, with an automata-theoretic point of view. We exhibit optimal subclasses of alternating tree automata, thus providing a new framework for the satis ability problem with frame constraints. Additionally, we clarify the correspondence between runs of automata and branches of the standard tableau construction for modal logic. We are confi dent this pioneer work is a milestone in bridging philosophers, logicians and computer scientists know-hows