The theory of successor extended by several predicates
Séverine Fratani · HAL (Le Centre pour la Communication Scientifique Directe) · 2009
We present a method to define unary relations P1 , . . . , Pn such that the Monadic Second-Order theory of the natural integers en- dowed with the successor relation and P1 , . . . , Pn is decidable. The main tool is a novel class of iterated pushdown automata whose transitions are controlled by tests on the store.