Infinite tree automaton とは

コンピュータサイエンスと数学論理では、無限木オートマトンは無限木構造を扱う状態機械です。これは、有限木構造を受け入れる有限木オートマトンからの拡張として見ることができる。また、BüchiオートマトンやMullerオートマトンなど、いくつかの無限語オートマットの拡張として見ることもできます。
有限オートマトンは、モナド二次論理の決定可能性を証明するためにRabinによって最初に使用されました。木オートマトンと論理理論は密接に結びついており、論理の決定問題をオートマトンの決定問題に還元することができることがさらに観察されている。