In the context of formal verification:
PTIME: problems can be solved with time complexity polynomials to the
input sizes in bit counts;
PSPACE: problems may incur memory consumption polynomials to the
input sizes in bit counts;
NP: problems mean that we can guess a solution in time complexity polynomials to the input sizes;
NP-complete: problems are the hardest ones in NP and are in general considered untamable problems in computer sciences;
EXPTIME: problems consume CPU times exponential to the sizes of inputs in bit counts;
EXPSPACE: is the set of problems that at most consume memory capacity exponential to the input sizes in bit counts;
EXPSPACE-complete: problems are harder than EXPTIME problems;
Nonelementary complexities are like 2^2^[stack] with the heights of the exponent stacks at least proportional to the input sizes in bit counts;
Undecidable problems do not guarantee termination. In general, it is not possible to design algorithms (procedures that guarantee termination) for undecidable problems.
Copy and Paste from: Formal Verification of Timed Systems: A Survey and Perspective; Farn Wang.
