The Coalgebraic mu-Calculus
Dirk Pattinson ( Imperial College )
- 14:00 29th May 2009 ( week 5, Trinity Term 2009 )Lecture Theatre B
Applications of modal logics are abundant in computer science, and a large number of structurally different modal logics have been successfully employed in a diverse spectrum of application contexts: knowledge representation, reasoning about distributed and multi-agent systems and the verification of distributed systems. Coalgebraic semantics provides a uniform and encompassing view on the large variety of specific logics used in particular domains. The coalgebraic approach is generic and compositional: tools and techniques simultaneously apply to a large class of application areas and can moreover be combined in a modular way.
We summarise the coalgebraic framework, along with some recent developments, and then introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus, and for an extension of coalition logic with fixpoints.
We summarise the coalgebraic framework, along with some recent developments, and then introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus, and for an extension of coalition logic with fixpoints.
Share this:
