\documentclass{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amssymb}
\newcounter{probcnt}
\newenvironment{problem}{\stepcounter{probcnt}{\bf Problem \arabic{probcnt}}.}{}
\newcounter{pracprobcnt}
\newenvironment{pracproblem}{\stepcounter{pracprobcnt}{\bf Practice Problem \arabic{pracprobcnt}}.}{}
\setlength{\parskip}{.4cm}
\setlength{\baselineskip}{15pt}
\setlength{\parindent}{0cm}
\newcommand{\s}[1] {\mathsf{#1}}
\newcommand{\compl}[1] {\overline{#1}}
\newcommand{\meanl} {[\![}
\newcommand{\meanr} {]\!]}
\newcommand{\means}[1] {\meanl #1 \meanr}
\newcommand{\propsem}[2] {#1\means{#2}}
\newcommand{\logprf} {\vdash}
\newcommand{\logcnsq} {\models}
\newcommand{\emptystr} {\varepsilon}
\newcommand{\foth}[1] {\mbox{Th}(#1)}
\newcommand{\nat} {{\mathbb N}}
\newcommand{\pshdelta} {\delta_{\s{push}}}
\newcommand{\popdelta} {\delta_{\s{pop}}}
\newcommand{\nodelta} {\delta_{\s{nochg}}}
\author{}
\date{}
\begin{document}
\hrule
\begin{center}
{\LARGE \sc $\underline{\mbox{Homework 5}}$} \\
{\Large \sc CS 498 MV: Logic in Computer Science}\\
\ \\
\begin{tabular}{ll}
Assigned: November 29, 2018 & Due on: December 7, 2018
\end{tabular}
\end{center}
\hrule
{\bf Instructions:} Solutions to the homework problems should be
turned in as a PDF file on Gradescope. See instructions on Piazza.
{\bf Recommended Reading:} Lectures 17 through 22: LTL, tree automata,
finite model theory, descriptive complexity, and series-parallel
graphs.
$\underline{\mbox{\bf Homework Problems}}$
\begin{problem}
Recall that in class we showed that connectivity is not expressible
in ordered graphs using Gurevich's result about orders. In this
problem you are required to show that it is not expressible in
(unordered) graphs directly. Let $G_\ell$ denote a cycle of length
$\ell + 1$. That is, $G_\ell$ has vertices $V = \{0,1,\ldots \ell\}$
and edges $E = \{(i,i+1)\: |\: 0 \leq i < \ell\} \cup \{(i+1,i)\: |\:
0 \leq i < \ell\} \cup \{(0,\ell),(\ell,0)\}$. Let $G_k + G_\ell$
denote the graph obtained by taking the disjoint union of $G_k$ and
$G_\ell$, i.e., $G_k + G_\ell$ has two cycles of length $k+1$ and
$\ell+1$ over disjoint set of vertices. Show that the Duplicator has a
winning strategy in ${\cal G}_m(G_\ell, G_k + G_\ell)$, when $k,\ell
\geq 2^m$.
\end{problem}
\begin{problem}
A {\em pushdown automaton} $P$ (without inputs and final states) is a
tuple $(Q,q_0,\Gamma, \bot, \delta)$, where $Q$ is a finite set of
states, $q_0 \in Q$ is the initial state, $\Gamma$ is the finite stack
alphabet, $\bot \not\in \Gamma$ is the initial stack symbol, and $\delta
= \pshdelta \cup \popdelta \cup \nodelta$ is the transition
relation. $\pshdelta \subseteq Q \times \Gamma \times Q$ are the push
transitions: $(q_1,\gamma,q_2) \in \pshdelta$ means that the automaton
can go from $q_1$ to $q_2$ by pushing $\gamma$ onto the stack
(independent of what is on top of the stack). $\popdelta \subseteq Q
\times \Gamma \times Q$ are the pop transitions: $(q_1,\gamma,q_2) \in
\popdelta$ means that the automaton can go from $q_1$ to $q_2$ if
$\gamma$ is on top of the stack, and the result of taking the
transition is to pop $\gamma$ from the stack. $\nodelta \subseteq Q
\times Q$ are the no stack change transitions: $(q_1,q_2) \in
\nodelta$ means that the automaton can go from $q_1$ to $q_2$ without
changing the stack (independent of what is on top of the stack).
The {\em graph of a pushdown automaton} $P$, is the (infinite) graph
$G(P) = (V,E)$, where $V = \bot\Gamma^*Q$ and $E$ is defined as
follows. $(\bot\gamma^1_1\gamma^1_2\cdots\gamma^1_nq_1,
\bot\gamma^2_1\gamma^2_2\cdots\gamma^2_mq_2) \in E$ if one of the
following 3 condtions hold. Either $(q_1,\gamma,q_2) \in \pshdelta$
and $m = n+1$, with $\gamma^2_m = \gamma$ and $\gamma^2_i =
\gamma^1_i$ for $i \leq n$. Or $(q_1,\gamma,q_2) \in \popdelta$ and $m
= n-1$, with $\gamma^1_n = \gamma$ and $\gamma^2_i = \gamma^1_i$ for
$i \leq n-1$. Or $(q_1,q_2) \in \nodelta$ and $m = n$, with
$\gamma^2_i = \gamma^1_i$ for $i \leq n$.
The {\em infinite $n$-ary tree} ${\cal T}$ is the infinite tree where
every node has exactly $n$ children. It can be viewed as a first order
structure over the signature $\tau_n = \{S_1,S_2,\ldots S_n\}$, where
$S_i$ is the $i$th child relation. In other words, as a first order
structure ${\cal T} = (T, \{S_i^{{\cal T}}\}_{i=1}^n)$, where $T$ is
the set of nodes, and $(u,v) \in S_i^{{\cal T}}$ iff $v$ is the $i$th
child of $u$.
Consider a pushdown automaton $P$ with $\Gamma = \{1,2,\ldots k\}$ and
$Q = \{k+1,k+2,\ldots n\}$. Prove that for every MSO sentence
$\varphi$ (over signature $\tau_G = \{E\}$) there is an MSO sentence
$\varphi^*$ (over signature $\tau_n$) such that
\[
G(P) \models \varphi \qquad \mbox{iff} \qquad {\cal T} \models \varphi^*
\]
{\em Hint:} Use the idea of interpretations. For a vertex $v =
\bot\gamma_1\gamma_2\cdots\gamma_mq$ of $G(P)$ let $t(v)$ be the node
of ${\cal T}$ reached by following the path
$\gamma_1\gamma_2\cdots\gamma_mq$ from the root. And for a set of
vertices $U$ of $G(P)$, let $t(U) = \{t(v)\: |\: v \in U\}$. The
translation to $\varphi^*$ can be done inductively, maintaining the
following invariant
\[
G(P) \models
\psi(x_1,\ldots, x_s, X_1, \ldots X_t)[x_i \mapsto v_i, X_i \mapsto U_i]
\mbox{ iff }
{\cal T} \models
\psi^*(x_1,\ldots, x_s, X_1, \ldots, X_t)[x_i \mapsto t(v_i), X_i \mapsto t(U_i)]
\]
In doing this construction, it might be useful to first define a
formula ${\rm Vert}(x)$ such that for a node $n_1$ of ${\cal T}$ ${\rm
Vert}(n_1)$ holds iff $n_1 = t(v)$ for some $v$ of $G(P)$, i.e.,
$n_1$ is reached by following a path of the form
$\gamma_1\cdots\gamma_mq$, where $\gamma_i \in \{1,\ldots k\}$ and $q
\in \{k+1,\ldots n\}$.
\end{problem}
\end{document}