Push down automaton for Language of same number of as and bs The task


  Find a pushdown automaton $M$, so that $L(M)=\{w \in \{a,b\}^*\ |\ |w|_a=|w|_b\}$, where $|w|_a$ denotes the number of $a$s in a word $w$.


My solution

I'm using the Wikipedia notation.
$$M = (Q, \Sigma, \Gamma, \delta, q_0, Z_0, \{q_0\})$$
$$Q=\{q_0\}, \Sigma = \{a,b\}, \Gamma = \{Z_0, A,B\}$$
$$\delta\text{ has the following instructions:}$$
$$(q_0, \varepsilon, Z_0, q_0, \varepsilon),$$
$$(q_0, a, Z_0, q_0, AZ_0),$$
$$(q_0, b, Z_0, q_0, BZ_0),$$
$$(q_0, a, A, q_0, AA),$$
$$(q_0, b, A, q_0, \varepsilon),$$
$$(q_0, b, B, q_0, BB)\text{ and}$$
$$(q_0, a, B, q_0, \varepsilon).$$

Questions


Is this correct? Can it be simplified?
If so, how can I argue (not neccessarily proof) its correctness?
The usual approach is to prove by induction the following kind of statement:


  The set of configurations reachable from the initial state upon reading a word $w$ is ...


Here ... depends on $w$. Having proved this kind of statement, you can deduce which words are accepted by your machine, hence proving its correctness.