Model checking over infinite structures: Automatic Structures and Regular Automatic Trees

Sophie Pinchinat
Friday, 31 May, 2019 - 14:00
Solvay Room, NO-5

We introduce infinite relational structures that have a finite presentation by means of a finite tuple of finite-state automata, known as automatic structures. We first show that model checking against first-order logic is decidable over automatic structures. Second, we show how this seminal result can be adapted to attain the decidability of model-checking against chain-MSO, a second-order logic where second-order quantifiers range over subsets of branches, over a remarkable strict subclass of automatic structures, called regular automatic trees.