Infinite data exists extensively in computer programs and database systems.Driven by the need from the applications of formal verification and database management, formal models over infinite alphabets are becoming a research focus of theoretical computer science.The main purpose of this article is to do a relatively complete and detailed survey on this topic.The article is organized according to the different mechanisms of automata models to deal with the infinite data values.The main focus is on the decidability and complexity of the related decision problems, that is, the nonemptiness and language inclusion problem of automata, and the satisfiability problem of logics.