Decision problem for a Regular Langauge I'm not sure if my logic is correct when it comes to the algorithm for decision problems. The concept is confusing me when I fail to distinguish its answer from that of a proof.

For example:

Given two finite automata $M_1, M_2$ that operate on a common alphabet, find an algorithm to show that:

$$L(M_1) \subseteq L(M_2)$$

And how I viewed it was:


Find a string $w$ from the alphabet $\Sigma$
Feed $w$ to $M_2$; if accepted then $w$ is part of $L(M_2)$
Feed $w$ to $M_1$; if accepted then $w$ is part of $L(M_1)$
If $w$ was accepted by $M_2$ and $M_1$, then $L(M_1) \subseteq L(M_2)$
Otherwise reject


Unlike proofs which require mathematical arguments, algorithms for decision problems seem more like a logical flow or sequence description. If it were a proof I would have to perhaps design a language or expression using properties and lemmas where as here I just describe the process of determining if the statement can be answered (via "yes" or "no").
Your algorithm is not really specified completely, since you don't explain how you choose the word $w$. However, even once you do specify how $w$ is chosen, your algorithm will be incorrect. The reason is that it is completely symmetric in $M_1$ and $M_2$. In other words, if the algorithm accepts on the pair $(M_1,M_2)$, then it will also accept on the pair $(M_2,M_1)$. This means that it will necessarily fail for machines satisfying $L(M_1) \subseteq L(M_2)$ but $L(M_2) \nsubseteq L(M_1)$.
Presumably in class you were shown other decision algorithms for regular languages. I suggest you try to emulate them. As an example, here is an algorithm that determines whether $L(M) \neq \emptyset$, for a DFA $M$.

Input: A DFA $M = \langle \Sigma, Q, q_0, F, \delta \rangle$.
Accept if some state in $F$ is reachable from $q_0$, and reject otherwise.

(In class you will probably need to be more verbose.)
To show that this algorithm is valid, we need to show two things:

If $L(M) \neq \emptyset$, then the algorithm accepts.
If $L(M) = \emptyset$, then the algorithm rejects.

To prove the first part, suppose that $w \in L(M)$. By definition, the state $\delta(q_0,w) \in F$ is reachable from $q_0$, so the algorithm accepts.
To prove the second part, we will prove the contrapositive: if the algorithm accepts, then $L(M) \neq \emptyset$. Suppose that some state $q \in F$ is reachable from $q_0$. This means that there is some path from $q_0$ to $q$. If $w$ is the concatenation of all symbols on this path, then $\delta(q_0,w) = q \in F$, and so $w \in L(M)$, showing that $L(M)$ is non-empty.
(Once again, in class you will probably need to be more verbose.)