Monadic Second Order (MSO) logic on graphs Given a conflict graph $G = (V, E)$, a man has to transport a set $V$ of items/vertices across the river. Two items are connected by an edge in $E$, if they are conflicting and thus cannot be left alone together without human supervision. The available boat has capacity $b\geq 1$, and thus can carry the man together with any subset of at most $b$ items. A feasible schedule is a finite sequence of triples $(L_1, B_1, R_1),\dots, (L_s, B_s, R_s)$ of subsets of the item set V that satisfies the following conditions (FS1)–(FS3). The odd integer $s$ is called the length of the schedule.
(FS1) For every $k$, the sets $L_k, B_k, R_k$ form a partition of V . The sets $L_k$ and $R_k$ form stable sets in $G$. The set $B_k$ contains at most $b$ elements.
(FS2) The sequence starts with $L_1 \cup B_1 = V$ and $R_1 = \emptyset$, and the sequence ends with $L_s = \emptyset$ and $B_s\cup R_s = V$.
(FS3) For even $k \geq 2$, we have $B_k\cup R_k = B_{k-1} \cup R_{k-1}$ and $L_k = L_{k-1}$. For odd $k \geq3$, we have $L_k\cup B_k= L_{k-1}\cup B_{k-1}$ and $R_k = R_{k-1}$.
Known Result: $VertexCover(G) \geq b \geq VertexCover(G)+1$.
Please help formulate this problem in MSO. 
 A: Maybe there is a solution. But, for that I assume there is an upper bound in the number of rounds needed, say n, and that the value b is fixed upfront. Then, there is the following EMSO formula,
$\exists L_{1} \exists B_{1} \exists R_{1} ... \exists L_{n} \exists B_{n} \exists R_{n} \phi(L_{1},B_{1},R_{1} ...,L_{n},B_{n},R_{n})$  
where $\phi = Seq_{1} \wedge Seq_{2} ...\wedge Seq_{n}$ 
$Seq_{1}$=$\forall x (XOR(x\in L_{1},x \in B_{1})) \wedge empty(R_{1}) \wedge$ $lessthanb(B_1) \wedge IndSet(L_{1})$
If i is even :
$Seq_{i} = empty(L_{i-1}) \vee (equals(L_{i-1},L_{i})\wedge 
\forall x ((x \in B_{k-1} \vee x \in R_{k-1})$
$ \Rightarrow XOR(x \in B_{k},x \in R_{k})))
\wedge lessthanb(B_i) \wedge IndSet(L_{i}) \wedge IndSet(R_{i})$ 
If i is odd (i $\geq$ 3): 
$Seq_{i}$ = $empty(L_{i-1}) \vee (equals(R_{i-1},R_{i})\wedge \forall x ((x \in B_{k-1} \vee x \in L_{k-1})$
$ \Rightarrow XOR(x \in L_{k},x \in B_{k}))) \wedge lessthanb(B_i) \wedge IndSet(L_{i}) \wedge IndSet(R_{i})$ 
$Seq_{n} = empty(L_{n-1})$
So if we can prove that if there is a solution then there is a solution of maximum n rounds which is dependent on the size of the graph then I think we have a solution.
empty(X) = $\forall x \neg(x\in X)$
lessthanb(X) = $\exists x_{1} ... \exists x_{b} (\wedge_{i \neq j}\neg(x_{i} = x_{j})) \forall x (x \in X) \rightarrow (x=x_{1} \vee... \vee x=x_{b})$
IndSet(X) = $\forall x,y \in X \neg(R(x,y))$
A: I am not sure whether it is definitely expressible in MSO or not. 
A: You can find papers on the graph theoretic problem by searching for "Alcuin number graph".
A reference to a clear definition of Monadic Second-Order Logic (and especially, some examples of what it can typically express) would be helpful for answering the question.
A: In MSOL as I know it one could not express this for the boring reason that you can't say in MSOL "set B_i contains at most b elements" (parametrically in b). Maybe you should say precisely what language you want this expressed in? (And what exactly you want expressed: that a given solution is feasible?)
