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:

1. $L$ is rational, i.e. $L\in\operatorname{RAT}(M)$.
2. $L$ is accepted by a nondeterministic finite $M$-automaton.
3. $L$ is accepted by a "spelling" nondeterministic finite $M$-automaton with a single initial state.
4. $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).

• The text then cites: Theorem 7.17 (McKnight). A monoid $M$ is finitely generated if and only if $\operatorname{REC}(M)\subset\operatorname{RAT}(M)$. For this it gives the reference "J.D. McKnight: Kleene quotiont theorem. Pacific Journal of Mathematics, S. 1343-1352, 1964." For the analogous characterization of recognizable sets $\operatorname{REC}(M)$ over $M$ by deterministic $M$-automata, the text gives the reference "A. Nerode: Linear Automaton Transformations. Proceedings of the American Mathematical Society, 9(4):pp. 541-544, 1958." May 12 '15 at 7:56
• See also the lecture notes Automata and Formal Languages by Manfred Kufleitner. And there is now also an English edition of the mentioned book Mar 6 '17 at 22:28

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.