Who introduced nondeterministic M-automata, and proved that the finite ones recognize the rational sets over M? Let $M$ be a monoid. The family $\operatorname{RAT}(M)$ of rational sets over $M$ is defined inductively:


If $L$ is a finite subset of $M$, then $L\in\operatorname{RAT}(M)$.
If $K,L\in\operatorname{RAT}(M)$, then $K\cup L\in\operatorname{RAT}(M)$ and $KL\in\operatorname{RAT}(M)$.
If $L\in\operatorname{RAT}(M)$, then $L^*\in\operatorname{RAT}(M)$.


A similar definition can be found in "J.-E. Pin, Mathematical Foundations of Automata Theory", and already "S. Eilenberg, Automata, Languages, and Machines" defines rational sets.

A nondeterministic $M$-automaton $\mathcal A = (Q,\delta,I,F)$ consists of a set of states $Q$, a transition relation $\delta\subset Q\times M\times Q$, a set of initial states $I\subset Q$, and a set of final states $F\subset Q$. If $\delta$ is a finte set, then we say that $\mathcal A$ is finite. A run on $\mathcal A$ is a sequence of the form $$r=q_1u_1q_2\dots u_nq_{n+1}$$ with $(q_iu_iq_{i+1})\in\delta$ for all $1\leq i\leq n$. If $q_1\in I$ and $q_{n+1}\in F$, then we say that it accepts $u=u_1\dots u_n$. The set accepted by $\mathcal A$ is defined as $$L(\mathcal A):=\{u\in M|\mathcal A \text{ has a run } r \text{ that accepts }u\}$$

I found this definition in chapter 7 Automatentheorie of the German text book "Volker Diekert, Manfred Kufleitner, Gerhard Rosenberger: Diskrete algebraische Methoden: Arithmetik, Kryptographie, Automaten und Gruppen”. There we also find the following theorem:

Theorem 7.15 Let $M$ be a monoid and $L\subset M$. Then the following are equivalent:


$L$ is rational, i.e. $L\in\operatorname{RAT}(M)$.
$L$ is accepted by a nondeterministic finite $M$-automaton.
$L$ is accepted by a "spelling" nondeterministic finite $M$-automaton with a single initial state.
$L$ is accpected by a nondeterministic finite $M$-automaton with "rational labels".


I omitted the definitions for "spelling" and "rational labels", because I only want to know who first introduced nondeterministic M-automata, and proved the equivalence of (1) and (2).
According to J. Sakarovich, Elements of Automata Theory, p. 372, 


  It seems that the result appears for the first time in [1]; hidden in a footnote of this seminal but difficult article, it was then given many statements, usually in special cases. 


[1] C. C. Elgot and J. E. Mezei, On relations defined by generalized finite automata, IBM J. Res. and Develop., vol. 9 (1965), 47–68.

A full proof was also given in S. Eilenberg, Automata, Languages and Machines, vol. A, Academic Press, 1974.