Modal Circuits

Abstract

It is well known that Boolean logic circuits are functionally equivalent to propositional logic. This thesis develops an extension of Boolean logic circuits that are functionally equivalent to modal logic with Kripke semantics. We call these circuits modal circuits. We first define how modal circuits work with a series of definitions. Then we prove that modal circuits are functionally equivalent to modal logic with Kripke semantics. Using these circuits, we also define a modal analogue of Boolean circuit satisfiability, called MCSAT. We show that the well known PSPACE-complete problem of modal satisfiability (MSAT) is polynomial time reducible to MCSAT.