In the past years, extensions of monadic second-order logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.

We study definability questions for positional winning strategies in infinite games on graphs. The quest for efficient algorithmic constructions of winning regions and winning strategies in infinite games, in particular parity games, is of importance in many branches of logic and computer science. A closely related, yet different, facet of this problem concerns the definability of winning regions and winning strategies in logical systems such as monadic second-order logic, least fixed-point logic LFP, the modal μ-calculus and some of its fragments. While a number of results concerning definability issues for winning regions have been established, so far almost nothing has been known concerning the definability of winning strategies. We make the notion of logical definability of positional winning strategies precise and study systematically the possibility of translations between definitions of winning regions and definitions of winning strategies. We present explicit LFP-definitions for winning strategies in games with relatively simple objectives, such as safety, reach ability, eventual safety (Co-Büchi) and recurrent reach ability (Büchi), and then prove, based on the Stage Comparison Theorem, that winning strategies for any class of parity games with a bounded number of priorities are LFP-definable. For parity games with an unbounded number of priorities, LFP-definitions of winning strategies are provably impossible on arbitrary (finite and infinite) game graphs. On finite game graphs however, this definability problem turns out to be equivalent to the fundamental open question about the algorithmic complexity of parity games. Indeed, based on a general argument about LFP-translations we prove that LFP definable winning strategies on the class of all finite parity games exist if, and only if, parity games can be solved in polynomial time, despite the fact that LFP is, in general, strictly weaker than polynomial time.