Weak MSO with the unbounding quantifier (Q537919)

Weak monadic second-order (MSO) logic is the monadic second-order predicate logic over the set \(\mathbb N\) of natural numbers with successor function \(s(x)=x+1\) over \(\mathbb N\). Monadic predicates \(X(x)\) may be finite or infinite (i.e., may have a finite or infinite set of truth points). But second-order quantification is allowed only over finite predicates. Additionally, there is allowed the unbounding quantifier \(UX.\varphi(X)\) which says that the size of \(X\) satisfying \(\varphi(X)\) is unbounded, i.e., \(UX.\varphi(X)=\bigwedge_{n\in \mathbb N}\exists_{\text{fin}}\,X\, (\varphi(X)\land |X|\geq n\)), where the formula \(\varphi(X)\) does not use the unbounding quantifier. Fix a set of counters \(C\). Define the following operations: 1) \(c:=c+1\) (increment counter \(c\)); 2) \(c:=0\) (reset counter \(c\)); 3) \(c:=\max(d,e)\) (store in counter \(c\) the maximal value of counters \(d,e\)). For a counter valuation \(v\in\mathbb N^C\) and a finite sequence of counter operations \(\pi\), let \(v\pi\in\mathbb N^C\) be the counter valuation obtained from \(v\) by applying all the operations in \(\pi\). A max automaton is a finite automaton where each transition is labelled by a finite sequence of counter operations. A \({run}\) of the automaton is a sequence of transitions which is consistent with the input word. Fix a run \(\rho\) and let \(\pi_{i}\) be the sequence of counter operations that labels the first \(i\) transitions in \(\rho\). For an initial counter valuation \(v\in\mathbb N^C\) and a counter \(c \in C\), define a sequence \(\rho_c\in \mathbb N^\omega\), \(\rho_c=v(c),v\pi_1(c),v\pi_2(c),\dots\). The acceptance condition of a max automaton is a Boolean combination of conditions: ``the sequence \(\rho_c\) is bounded'', i.e., the acceptance condition is a Boolean combination of conditions lim sup \(\rho_{{c}} < \infty\). The main result of the paper is that the classes of \(\omega\)-regular languages represented in weak MSO logic and accepted by deterministic max automata, respectively, coincide.