| Abstract: |
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. Here, we provide a
classification result for predicate liftings which leads to an easy
criterion for the existence of such separating sets, and we 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. We then move on to polyadic modal logic, where modal operators
may take more than one argument formula. We show that every accessible
functor admits an expressive polyadic modal logic. Moreover, expressive
polyadic modal logics are, unlike unary modal logics, compositional.
|
