Fixed point logics: expressive power, structure, complexity

不动点逻辑在数学逻辑的许多领域及其在计算机科学中的应用中起着核心作用。在这个项目中，我们研究不动点逻辑在寻求多项式时间的逻辑和（线性）代数中算法问题的可定义性的背景下，与过渡系统的双模拟安全性和模态逻辑的扩展有关，以及在无限对策理论的背景下。有限模型理论的核心挑战是寻求多项式时间的逻辑。对各种不动点逻辑的研究使得多项式时间片段的逻辑表征越来越强大。另一方面，人们分离出了一些在经典不动点逻辑中无法表达的基本算法方法。这些包括来自（线性）代数、图论（例如关于图同构）和并行计算的算法技术。在这个项目中，我们用这种算法方法扩展不动点逻辑，并研究它们的复杂性、表现力和结构。此外，我们还试图通过构造和分析超越状态公式和一元不动点的模态逻辑，从而给模态逻辑领域带来新的推动力。我们将使用这些方法和其他方法来加强我们对不动点逻辑和无限博弈之间联系的理解，特别是关于获胜策略的可定义性。最后，我们在Hodges团队语义的基础上，研究了不动点逻辑与一类相对较新的逻辑在依赖、独立和不完全信息推理方面的关系。

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.