Bahareh Afshari: Nested sequents for fixed point modal logic

Abstract: Modal logic provides an effective language for expressing properties of state-based systems. When equipped with operators that can test for infinite behaviour like looping and reachability, the logic becomes a powerful tool for specifying correctness of nonterminating reactive processes such as communication protocols and control systems. An elegant example of such a logic is the modal mu-calculus which extends basic modal logic by two quantifiers for defining inductive and co-inductive operators. 

In this talk I will introduce the modal mu-calculus and present a complete proof system for it based on nested sequents. We will see how the proof system can be used to obtain a constructive proof of the finite model property and, time permitting, I will also explain how the framework lends itself to a sound and complete axiomatisation for the extension of mu-calculus with backward modalities.