#### Automata Theory and Games

- H. Michalewski, A. Nagórko, J. Pawlewicz, An upper bound of 84 for Morpion Solitaire 5D. The Morpion Solitaire is a paper-and-pencil single-player game played on a square grid with initial position consisting of 36 dots. In each move the player puts a dot on an unused grid position and draws a line that consists of four consecutive segments passing through the dot. The goal is to find the longest possible sequence of moves. There are two main variants of the game: 5T and 5D. They have different restrictions on how the moves may intersect. Providing lower and upper bounds in Morpion Solitaire is a significant computational and mathematical challenge that led to a discovery of an important new algorithm. Best lower bounds for Morpion Solitaire were found in $2011$ by Rosin using a variant of the Monte Carlo method: $178$ moves for the 5T variant, $82$ moves for the 5D variant. In the Morpion 5D variant Kawamura et al. proved an upper bound of $121$ moves using a geometrical argument. We improve this bound to 84. This is done in two steps. 1) We state, using linear constraints, a geometric property that defines a class of graphs that includes all Morpion positions - finding practically solvable linear constraints is a main conceptual advance of the present paper. 2) We solve the mixed integer problems and obtain an upper bound of 84 for Morpion 5D. The same method fully solves Morpion 5D with center symmetry - the optimal sequence is 68 moves long.
- H. Michalewski, M. Mio, Measure Quantiﬁer in Monadic Second Order Logic. We study the extension of Monadic Second Order logic with the “for almost all” quantifier $\forall^{=1}$ whose meaning is, informally, that $\forall^{=1}X.\phi(X)$ holds if $\phi(X)$ holds almost surely for a randomly chosen $X$. We prove that the theory of $MSO\!+\!\forall^{=1}$ is undecidable both when interpreted on $(\omega,<)$ and the full binary tree. We then identify a fragment of $MSO\!+\!\forall^{=1}$, denoted by $MSO+\forall^{=1}_\pi$, and reduce some interesting problems in computer science and mathematical logic to the decision problem of $MSO\!+\!\forall^{=1}_\pi$. The question of whether $MSO\!+\!\forall^{=1}_\pi$ is decidable is left open.
- L.A. Kołodziejczyk, H. Michalewski How unprovable is Rabin's decidability theorem? We study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that the complementation theorem for tree automata, which forms the technical core of typical proofs of Rabin's theorem, is equivalent over the moderately strong second-order arithmetic theory $ACA_0$ to a determinacy principle implied by the positional determinacy of all parity games and implying the determinacy of all Gale-Stewart games given by boolean combinations of $\Sigma^0_2$ sets. It follows that complementation for tree automata is provable from $\Pi^1_3$- but not $\Delta^1_3$-comprehension. We then use results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld to prove that over $\Pi^1_2$-comprehension, the complementation theorem for tree automata, decidability of the MSO theory of the infinite binary tree, positional determinacy of parity games and determinacy of $Bool(\Sigma^0_2)$ Gale-Stewart games are all equivalent. Moreover, these statements are equivalent to the $\Pi^1_3$-reflection principle for $\Pi^1_2$-comprehension. It follows in particular that Rabin's decidability theorem is not provable in $\Delta^1_3$-comprehension.
- H. Michalewski, A. Nagórko, J. Pawlewicz 485 - a new upper bound for Morpion Solitaire, accepted CGW@IJCAI. In the work of E.D. Demaine, M.L. Demaine, A. Langerman and S. Langerman an upper bound of $705$ was proved on the number of moves in the 5T variant of the Morpion Solitaire game. We show a new upper bound of $485$ moves. This is achieved in the following way: we encode Morpion 5T rules as a linear program and solve approximately $130000$ instances of this program on special octagonal boards. In order to show correctness of this method we analyze rules of the game and use a concept of a potential of a given position. By solving continuous-valued relaxations of linear programs on these boards, we obtain an upper bound of $586$ moves. Further analysis of original, not relaxed, mixed-integer programs leads to an improvement of this bound to $485$ moves. However, this is achieved at a significantly higher computational cost. Source code of programs generating the linear problems.
- H. Michalewski, M. Mio, On the Problem of Computing the Probability of Regular Sets of Trees, submitted. We consider the problem of computing the probability of regular languages of infinite trees with respect to the natural coin-flipping measure. We propose an algorithm which computes the probability of languages recognizable by game automata. In particular this algorithm is applicable to all deterministic automata. We then use the algorithm to prove through examples three properties of measure: (1) there exist regular sets having irrational probability, (2) there exist regular sets which are comeager but of probability 0 and (3) the probability of game languages W i,k , from automata theory, is 0 if k is odd and is 1 otherwise.
- H. Michalewski, M. Mio, Baire Category Quantifier in Monadic Second Order Logic, accepted for presentation at ICALP 2015. We consider MSO logic of the full binary tree extended with the second-order quantifier $\forall^*$ with semantics given in terms of Baire Category and the Banach-Mazur game. We prove that the new quantifier can be eliminated ($MSO\!+\!\forall^* \!=\! MSO$). We then apply this result to prove that the finite-SAT problem for the qualitative fragment of the probabilistic temporal logic pCTL* is decidable. This extends a previous result of Brázdil, Forejt, Křetínský and Kučera valid for qualitative pCTL.
- M. Bojańczyk, T. Gogacz, H. Michalewski and M. Skrzypczak, On the decidability of MSO+U on infinite trees, ICALP 2014.
*This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in ZFC. This is because the theory is undecidable, under a set-theoretic assumption consistent with ZFC, namely that there exists of projective well-ordering of $2^\omega$ of type $\omega_1$. We use Shelah’s undecidability proof of the MSO theory of the real numbers.* - T. Gogacz, H. Michalewski, M. Mio and M. Skrzypczak, Measure properites of game languages, MFCS 2014.
*We show that $W_{i,k}$ languages are complete for the Kolmogorov hierarchy; also we consider measurability and regularity properties of measures on languages of trees defined by automata. This research was motivated by open questions left in M. Mio's doctoral dissertation which originally involved Martin Axiom.*A journal version of this paper (submitted) solves completely the problem of continuity using a method of Lusin and Sierpiński. This removes the remaining metamathematical assumptions from Mio's thesis. - H. Michalewski, M. Skrzypczak, Unambiguous Büchi is weak,
*We show, that if a given non-deterministic automaton of parity $(i,2n)$ is unambiguos, then the accepted language is in a smaller class $Comp(i+1,2n)$. This extends a theorem proved by Finkel and Simonnet stating that every unambiguous Büchi automaton recognises a Borel language.* - A. Facchini, H. Michalewski, Deciding the Borel complexity of regular tree languages, accepted for presentation at Computability in Europe (CiE 2014).
*We show that an algorithm of M. Bojańczyk and T. Place deciding if a given regular language of trees is a Boolean combination of open sets after some modifications also works in the case of ${\bf\Delta^0_2}$ sets.* - A. Arnold, H. Michalewski, D. Niwiński, On the separation question for tree languages, Theory of Computing Systems, accepted.
*We extend results from the paper presented at STACS 2012 conference, including separation property for the weak hierarchy and discussion of the reduction property.* - A. Arnold, H. Michalewski, D. Niwiński, On the separation question for tree languages, STACS 2012: 396-407.
*We prove that the seperation property fails for every class $(i,n)$ for odd $n$ and $i<n$. This extends an earlier result with Sz. Hummel.* - H. Michalewski, D. Niwiński, On Topological Completeness of Regular Tree Languages, Logic and Program Semantics 2012: 165-179.
*We show an example of a regular language of trees of index (1,3) which is complete for the class of $\Sigma^1_1$-inductive sets.* - Sz. Hummel, H. Michalewski, D. Niwinski, On the Borel Inseparability of Game Tree Languages, STACS 2009: 565-575.
*We give an example of a pair of Borel inseparable coanalytic sets and show implications of inseparability in the context of automata on trees.*

#### Set Theory and Topology

- M. Kojman, H. Michalewski, Borel Extensions of Baire Measures in ZFC, Fund. Math. 211 (2011), 197-223.
*We prove that every Baire measure on the Kojman-Shelah Dowker space admits a Borel extension. If the continuum is not a real-valued measurable cardinal then every Baire measure on the M.E. Rudin Dowker space admits a Borel extension.* - A. Komisarski, H. Michalewski, P. Milewski, Functions Equivalent to Borel Measurable Ones, Bull. Pol. Acad. Sci. 58 (2010), 55-64.
*Using a recent result of J. Saint Raymond we gave some conditions on a given function $f:R→R$ ($R$ stands for the real line), which are necessary and sufficient for existence of a Borel-measurable function equivalent, in a sense defined by Ryll-Nardzewski and Morayne, to the function $f$.* - A. Krawczyk, W. Marciszewski, H. Michalewski, Remarks on the set of $G_\delta$-points in Eberlein and Corson Compact Spaces, Topology and its Applications 156 (2009), 1746-1748.
*We show that, for every scattered Eberlein compact space K, the set of points with countable base of neighborhoods in K is a $G_\delta$-set in K. We also give an example of a scattered Eberlein compactum with non-metrizable set of points with countable base of neighborhoods in K. Moreover, we give an example of a Corson compact space K such that the set f points with countable base of neighborhoods in K does not contain any dense $G_\delta$ subset of K.* - W. Kubis, H. Michalewski, Small Valdivia compact spaces, Topology and its Applications 153 (2006), 2560–2573.
*Under certain conditions we show that retractions and open images of Valdivia compact spaces remain Valdivia. In general, as was proved by Kubis and Uspeinski, open image of a Valdivia compact space may be not Valdivia.* - H. Michalewski, Condensations Of Projective Sets Onto Compacta, Proc. Amer. Math. Soc. 131 (2003) no. 11, pp.3601-3606.
*I proved that every coanalytic-complete, separable, metrizable space might be bijectively, continuously mapped onto the Hilbert cube. As a corollary I noticed that the space $C_p(A)$ admits a weaker compact topology if $A$ is an analytic, separable, metrizable space. For sigma-compact $A$ this result was proved earlier by Arkhangelskii.* - A. Krawczyk, H. Michalewski, Linear metric spaces close to being sigma-compact, preprint of the Institute of Mathematics of the University of Warsaw.
*We shown, under an additional set theorethical assumption implied by MA, an example of two o-bounded, metrizable, separable topological groups, such that their product is not o-bounded. This construction appeals to the affinity between the o-bounded property and Menger property of a given topological group.* - A. Krawczyk, H. Michalewski An example of a topological group, Topology and its Applications 127 (2003), pp.325-330.
*We consider notions of o-boundedness and strong o-boundedness, introduced by Tkachenko and Okunev, which generalize the notion of $\sigma$-compactness in the class of topological groups. We gave an example of a topological group which is a Lindelof P-space, but which is not strongly o-bounded.* - H. Michalewski, An answer to a question of Arkhangelskii, Comment. Math. Univ. Carolinae 42 (2001).
*I gave two examples of a space with the property that the spaces $C_p(X)$ and $C_p(X\times\omega)$ are linear homeomorphic, but the spaces $C_p(X)$ and $C_p(X\times(\omega+1))$ are not linear homeomorphic, where $\omega$ and $\omega+1$ are countable ordinals equiped with ordinal topology. One of the examples is a metrizable space (it is so called the Stone space).* - H. Michalewski, Homogeneity of K(Q), Tsukuba Journ. of Math. 24 (2000), 297–302.
*I proved that all separable, metrizable, zero–dimensional spaces which are of the first category in itself and which are locally coanalytic complete, are homeomorphic. As a corollory I proved that the space of all compact subspaces of rationals, endowed with Hausdorff metric, is a topological group.* - H. Michalewski, Game-Theoretic Approach to the Hereditary Baire Property of $C_p(N_F)$, Bull. Pol. Acad. Sci. 46 (1998), 135-140.
*I gave a characterization in terms of topological games of these countable spaces $X$ with one non–isolated point, such that the function space $C_p(X)$ is a hereditary Baire space (every closed subset satisfies the Baire Category Theorem). It is a part of my master degree thesis.* - H. Michalewski, R. Pol, On a Hurewicz-Type Theorem and a Selection Theorem of Michael, Bull. Pol. Acad. Sci. 43 (1996), 273-275.
*We proved a generalization of Kechris-Louveau-Woodin theorem via an application of a theorem of Michael on selections.*

#### Theses

- MA Thesis (1998), Przestrzenie funkcji ciaglych i przestrzenie dziedzicznie Baire'a (in Polish; Function spaces and hereditary Baire spaces). Supervised by Witold Marciszewski.

- PhD Thesis (2002) Przestrzenie funkcyjne z topologia zbieznosci punktowej (in Polish; Function spaces with topology of pointwise convergence). Supervised by Witold Marciszewski.

- (2014/2015) Habilitation autoreferat in English, habilitation autoreferat in Polish; ``autoreferat'' stands for summary of professional accomplishments.

#### Selected seminar talks

- Morpion Solitaire @ "Co jest grane?" workshop, April 2016, Warsaw; Morpion 5T version online; code@github (running these experiments requires Gurobi solver).