–
Room P3.10, Mathematics Building
Expressivity of coalgebraic modal logic
Modal logic has a good claim to being the logic of choice for describing the reactive behaviour of systems modeled as coalgebras. Logics with modal operators obtained from so-called predicate liftings have been shown to be invariant under behavioral equivalence. Expressivity results stating that, conversely, logically indistinguishable states are behaviorally equivalent depend on the existence of separating sets of predicate liftings for the signature functor at hand. A new classification result for predicate liftings leads to an easy criterion for the existence of such separating sets, and allows one to give simple examples of functors that fail to admit expressive normal or monotone modal logics, respectively, or in fact an expressive (unary) modal logic at all. A remedy to this is to move on to polyadic modal logic, where modal operators may take more than one argument formula. Every accessible functor admits an expressive polyadic modal logic. Moreover, expressive polyadic modal logics are, unlike unary modal logics, compositional. The latter result is best understood in the terminology of syntax constructors and one-step semantics as introduced by Cirstea and Pattinson; it states essentially that polyadic modal logic is closed under the composition of syntax constructors.