Presenting Functors by Operations and Equations

We take the point of view that, if transition systems are coalgebras for a functor T, then an adequate logic for these transition systems should arise from the `Stone dual' L of T. We show that such a functor always gives rise to an `abstract' adequate logic for T-coalgebras and investigate under which circumstances it gives rise to a `concrete' such logic, that is, a logic with an inductively defined syntax and proof system. We obtain a result that allows us to prove adequateness of logics uniformly for a large number of different types of transition systems and give some examples of its usefulness.

• Type: Conference
• Year: 2006
• Where: FOSSACS
• Authors: Marcello M. Bonsangue, Alexander Kurz
• Keywords: Adequate Logic, FOSSACS 2006, Functor T, Software Engineering, Transition Systems