Kobe Colloquium on Logic, Statistics and Informatics

以下の要領でコロキウムを開催します。

日時：2015年7月14日（火）13:30-15:00 講演者：Olivier Finkel （パリ第７大学） 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）

============================================================

題目： Logic, Complexity and Infinite Computations

アブストラクト： The theory of automata reading infinite words, which is closely related to infinite games, is a rich theory which is used for the specification and verification of non-terminating systems. We prove that the Wadge hierarchy of omega-languages accepted by 1-counter Büchi automata (or by 2-tape Büchi automata) is equal to the Wadge hierarchy of omega-languages accepted by Büchi Turing machines, which forms the class of effective analytic sets. Moreover the topological complexity of an omega-language accepted by a 1-counter Büchi automaton, or of an infinitary rational relation accepted by a 2-tape Büchi automaton, is not determined by the axiomatic system ZFC. In particular, there is a 1-counter Büchi automaton A (respectively, a 2-tape Büchi automaton B) and two models V1 and V2 of ZFC such that the omega-language L(A) (respectively, the infinitary rational relation L(B)) is Borel in V1 but not in V2. We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Büchi automata (or by 2-tape Büchi automata) is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automaton (respectively, a 2-tape Büchi automaton) A such that: (1) There exists a model of ZFC in which Player 1 has a winning strategy in the Gale-Stewart game G(L(A)); but the winning strategies cannot be recursive and not even hyperarithmetical. (2) There exists a model of ZFC in which the Gale-Stewart game is not determined. We also prove that the determinacy of Wadge games between two players in charge of omega-languages accepted by real-time 1-counter Büchi automata (or by 2-tape Büchi automata) is equivalent to the effective analytic determinacy, and thus is not provable in ZFC.

========================================================

交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」 行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm