Generalized Modal Satisfiability

It is well known that modal satisability is PSPACE- complete (Lad77). However, the complexity may decrease if we restrict the set of propositional operators used. Note that there exist an innite number of propositional operators, since a propositional operator is sim- ply a Boolean function. We completely classify the complexity of modal satisability for every nite set of propositional operators, i.e., in con- trast to previous work, we classify an innite number of problems. We show that, depending on the set of propositional operators, modal sat- isability is PSPACE-complete, coNP-complete, or in P. We obtain this trichotomy not only for modal formulas, but also for their more succinct representation using modal circuits. We consider both the uni-modal and the multi-modal case, and study the dual problem of validity as well.