Fixed point logics: expressive power, structure, complexity

• Applicant: Professor Dr. Erich Grädel
• Subject Area: Theoretical Computer Science
• Term: from 2011 to 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 199814663

Fixed point logics play a central role in many areas of mathematical logic and its applications in computer science. In this project we investigate fixed point logics in the context of the quest for a logic for polynomial time and the definability of algorithmic problems in (linear) algebra, in connection with bisimulation safety on transition systems and extensions of modal logics, as well as in the context of the theory of infinite games.The central challenge in finite model theory is the quest for a logic for polynomial time. The study of different kinds of fixed point logics has led to logical characterizations of more and more powerful fragments of polynomial time. On the other hand one has isolated a number of fundamental algorithmic methods that cannot be expressed in classical fixed point logics. These include algorithmic techniques from (linear) algebra, from graph theory (e.g. concerning graph isomorphism) and for parallel computation. In this project we extend fixed point logics by such algorithmic methods and investigate their complexity, expressive power, and structure.In addition we intend to give a new impulse to the field of modal logics bythe construction and analysis of modal logics that go beyond state formulae and monadic fixed points, but guarantee safety under bisimulations. We will use these and other approaches to strengthen our understanding of the connection between fixed point logics and infinite games, especially concerning the definability of winning strategies. Finally we investigate the relationship of fixed point logics with a relatively new family of logics for reasoning about dependence, independence, and imperfect information, on the basis of Hodges' team semantics.

• DFG Programme: Research Grants