Fixed point logics: expressive power, structure, complexity

点击翻译按钮获取中文摘要

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.