As far as I know, the answer is no. We don't have an argument not based (directly or indirectly) on digonalization for even proving there is a language outside Dec (The set of Turing decidable languages).
Characterizing a class means having criteria for showing when a language is in the class and when a language is not. The second part would give us tools to prove lowerbounds on such classes.
For very small classes like $AC^0$ and $AC^0[p]$ there are combinatorial arguments (also for monotone-$AC^0$ circuits), but the current state of knowledge is consistent with $AC^0[6] = NP$. The Razbarov-Rudich (RR) Natural Proofs theorem is related to why the previous combinatorial arguments haven't been successful in separating larger classes. In simple terms, there is no "natural proof" for separating the larger classes unless there is no pseudo-random number generators (many believe they do exists), and all previous proofs were natural. Tim Gowers wrote a number of interesting blog posts on the topic:
http://gowers.wordpress.com/2009/09/22/a-conversation-about-complexity-lower-bounds/
The reason that we have pumping lemmas for $Reg$ (regular languages) and $CFL$ (context-free languages) is that the machine models for them are very specific which gives the strings accepted by them special combinatorial structure. For classes defined by Turing machines this is not the case. If a complexity class contains some basic functions (say $AC^0$) and is closed under composition, proving lowerbounds for it becomes a rather difficult task. Note that $Reg$ does not contain $AC^0$ ($\{0^n1^n: n \in \omega \}$ is in $AC^0$ but not in $Reg$.)
EDIT:Comments
part 1.
I don't have a theoretical justification right now, but the history of complexity theory shows that the structure of much smaller complexity classes are at least very difficult to understand. Many experts "believe" that there are pseudo-random number generators (PRNG), so RR's Natural Proof theorem applies and there is no "natural" property of sets/functions that can be used to prove a lowerbound for the complexity classes satisfying the condition of the RR theorem. I think a person accepting the existing of PRNGs can at least claim that there are no simple combinatorial structures for these complexity classes.
part 2. You are looking for a combinatorial property of sets of strings in a complexity class. The computational complexity of checking a property is a good measure. Any property stated in the first order logic (on a finite structure) is $AC^0$. The RR theorem applies to properties which are in $P$, i.e. can be checked in polynomial time given the truth table of the functions (characteristic functions of sets restricted to inputs of size n). Encoding Turing Machines (TM) is not difficult, and I think it can be done if one goes a little above $AC^0$, e.g. $TC^0$ is probably capable of checking if a string encodes a TM. You are looking for a property that holds for all functions in a class, but not for those outside it. The negation of it would be a property of the kind considered in RR's theorem. By these considerations, I think there are no properties of the kind you are looking for unless there are no PRNGs.
definitions:
$AC^0$ is class of sets of strings accepted by (uniform) circuits of polynomial size and bounded depth, i.e. there is a constant $d$ and a polynomial $p(n)$ and a sequence of circuits $\{C_n\}_{n \in \omega}$ using unbounded fan-in $\land$,$\lor$,$\lnot$ gates and of depth $d$ and size $p(n)$ that accepts them.
$AC^0[n]$ is the same as $AC^0$ but allows $mod_n$ gates. $p$ is a prime number.
$TC^0$ is the same as $AC^0$ but allows majority/threshold gates.
A property $Q$ is natural if it is:
useful: i.e. does not hold for simple functions (functions of low complexity) but holds for some function in the larger class,
constructive: i.e. can be checked in polytime from the truth table of the functions,
large: i.e. for some k and all large enough n, the property holds for at least $\frac{1}{n^k}$ of the functions.
Jean-Camille Birget answered my question. These are called universally halting Turing machines.
The oldest reference is:
Martin Davis (1956). A note on universal Turing machines. In Shannon,
C. E., McCarthy, J., eds, Automata Studies, pp. 167-175. Princeton
University Press.
Birget proved a complexity version of this:
Every deterministic Turing machine with time complexity $T(n)$ is equivalent to a deterministic Turing machine which halts after $O(T(n))$ steps, no matter what configuration of size $n$ this machine starts in [J.C. Birget, Infinite String Rewrite Systems and Complexity, J. Symbolic Computation (1998) 25, 759-793.]
Update Friedrich Otto sent the following two more references:
Herman, G.T.,
Strong computability and variants of the uniform
halting problem,
Zeitschrift fuer mathematische Logik und
Grundlagen der Mathematik,
17,
1971,
115--131
Shepherdson, J.C.,
Machine configuration and word problems of given
degree of unsolvability,
Zeitschrift fuer mathematische Logik und
Grundlagen der Mathematik,
11,
1965,
149--175
Best Answer
Yes, the class NP $\cap$ coNP is closed under symmetric difference. To see this, suppose that $A$ and $B$ are both in NP $\cap$ coNP. This means that the truth of $a\in A$ can be verified in polynomial time with a suitable witness, and also $a\notin A$ can be verified in polynomial time with a suitable witness, and the same for $B$. Let $A\triangle B=(A-B)\cup (B-A)$ be the symmetric difference (the same as what you call $A\oplus B$), and argue as follows:
$A\mathrel{\triangle} B$ is in NP. This is because we can verify whether $a\in A\mathrel{\triangle} B$ by verifying either that $a\in A$ and $a\notin B$ or that $a\notin A$ and $a\in B$. That is, the objects $a$ in the symmetric difference $A\mathrel{\triangle} B$ are verified by a pair of witnesses, which either verify membership in $A$ and not in $B$ or in $B$ but not in $A$.
$A\mathrel{\triangle} B$ is in coNP. This is because we can verfiy whether $a\notin A\mathrel{\triangle} B$ by verifying either that $a\in A$ and $a\in B$ or that $a\notin A$ and $a\notin B$.
So the symmetric difference is in NP $\cap$ coNP, as desired.
(Meanwhile, your proposed algorithm, if interpreted as a nondeterminisitic algorithm, is not correct, since failure to verify membership nondeterministically is not the same thing as a verfication of non-membership. In short, your algorithm can be fooled in the following way: suppose $x$ is in both languages, but in step 2 of your algorithm, $M_1$ happens to choose a branch of computation that doesn't verify membership---an inadequate witness, so it doesn't accept on that branch---but then $M_2$ does accept $x$ in step 4. In this case, you will accept $x$ when you shouldn't.)