While DCTLib's answer provides some insight in the general ideas, I think it is useful to give a more concrete example that has some use in practice.
One kind of 'infinite state system' is a labelled transition system $L$, where we describe a finite number of groups of states and transitions, but give each state a 'free' parameter from some domain, typically the natural numbers $\mathbb{N}$, and define transitions based on that parameter. We can ask whether certain proposition $P$ in the modal $\mu$-calculus hold (these include, but are not limited to CTL* and thus can encode many questions about the process the state machine represents, such as whether the process will always halt).
If we restrict these transitions such that they are 'linear process equations', we can (relatively efficiently) transform the pair $(L,P)$ into a Parameterised Boolean Equation System (PBES) $E$, such that some state $s$ is true in the solution for this system if and only if the proposition $P$ on $L$ holds on $s$.
Although we cannot always solve this system $E$, there are approaches that work reasonably well and tools that implement them. One such tool is mCRL2. This tool uses various techniques to try to solve PBES's, but most generally boil down to attempt to construct an equivalent Boolean Equation System (BES), which is the 'finite version' of the PBES and can therefore be solved using Gaussian elimination.
The method of proof graphs might also be instructive:
The idea is to pick only a finite number of states as vertices in a graph, with an explicit parameter, e.g. $X(1)$, $Y(7)$, $X(3)$. Then, we take a labelling on the vertices and a (directed) edge relation on them that models the 'dependency' between these states. If a certain property over all finite prefixes of all infinite paths on this graph holds, we call this graph a proof graph (the general structure without this property is called a dependency graph).
The nice part is that we have that a certain variable ($\approx$state) $s$ is true in the PBES if and only if there exists a proof graph containing that state!
So, we have transformed a question of potentially infinite paths (CTL^*) over an infinite system to a question of potentially infinite paths over a finite system. As all infinite paths on a finite system must eventually cycle, we can actually show that a graph is a proof graph automatically (Determining whether the proof graph exist may not be so easy, however. There is no panacea here!)