|Universiteit Faculteit FNWI English version||5 december 2007, e-mail|
Woensdag 12 december 2007
AbstractModal fixpoint logics constitute a research field of considerable interest, not only because of their many applications in computer science, but also because of their rich logical/mathematical theory, which features connections with fields as diverse as lattice theory, automata theory, and universal coalgebra. In this talk the perspective will be algebraic.
The Knaster-Tarski Theorem states that every order preserving function on a complete lattices has a least and a greatest fixpoint, both of which can be obtained as limits of a transfinite approximation process. In our specific application area we are dealing with Kripke algebras that algebraically model some process as a full power set algebra, endowed with additional operations (modalities), together with some maps that are defined using fixpoints.
After providing the basic definitions and some examples, I will discuss two questions that naturally arise in this setting. First I will address the issue, which fixpoints are constructive, that is, approximated in omega many rounds. Then I will go on to the question of axiomatizing flat modal fixpoint logics. Algebraically the challenge is to find (equational) axioms that guarantee the representability of an abstract modal fixpoint algebra as a concrete Kripke algebra.
The talk is largely based on joint work with Gaelle Fontaine and with Luigi Santocanale.