Dependence and Independence, Quantitative Aspects and Counting Constructs in Logic and Games

数理逻辑、自动机理论和无限对策理论的结合是反应系统综合与验证的成功方法论的基础。本研究项目的主要目标是通过一些相关的组成部分来扩展这种方法论，并加强逻辑与对策在这类应用中的联系。我们集中在两个主要方面进行这种扩展，以及它们的结合。一方面，我们要发展和加强定量方面的逻辑和相关的博弈论模型，特别强调计数的各种形式的结构。另一方面，我们调查的逻辑形式主义和博弈论方法的依赖性和独立性，基于Hodges介绍的团队语义和逻辑系统，发起Väänänen，其中依赖性和独立性的概念被视为原子语句。与这种逻辑相关的博弈模型一方面是不完全信息博弈，另一方面是我们在工作中介绍的二阶可达性博弈。最后，我们将联合收割机结合这两个方面，并将数量运算符和计数结构集成到逻辑中的依赖性和独立性，并集成到一般的团队语义中，以及相关的博弈模型中。

The combination of mathematical logic, automata theory and the theoryof infinite games is the basis of a successful methodology for the synthesisand verification of reactive systems.The main goal of this research project is to extend this methodologyby some relevant components and to strengthen the connections between logics and games with regard to such applications.We focus on two main aspects for such extensions, and on theircombination. On the one hand, we want to develop and strengthenquantitative aspects in logics and the associated game-theoretical models,emphasizing in particular counting constructs of various forms. On the other hand, we investigate logical formalisms and game-theoretical methodsfor dependence and independence, based on the team semantics introduced by Hodges and the logicals systems, initiated by Väänänen, in which notions of dependence and independence are treated as atomic statements. The game models relevant for such logics are, on the one hand, games with imperfect information, and on the other hand, the second-order reachability games that we introduced in our work.Finally, we shall combine these two aspects and integrate quantitative operators and counting constructs in logics for dependence and independence, and into team semantics in general, as well as into the associated game models.