MSO

Deciding ω-Regular Properties on Linear Recurrence Sequences

We consider the problem of deciding ω-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. …

Extensions of ω-Regular Languages

We consider extensions of monadic second-order logic over ω-words, which are obtained by adding one language that is not ω-regular. We show that if the added language L has a neutral letter, then the resulting logic is necessarily undecidable. A …

MSO+∇ is undecidable

This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying “almost surely a branch π ∈ {0,1} ω satisfies a formula φ(π)”, This logic was introduced by Michalewski and Mio; we call it MSO+∇ …

Emptiness of Zero Automata Is Decidable

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of mso, called tmso + zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero …