[logic-ml] Fwd: Kobe Colloquium on Logic, Statistics and Informatics, July 14 (Olivier Finkel)

[Joerg Brendle]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20150708/a3504bf1/attachment.html>