ETA: wait that doesn't make sense because it's equivalent to computing the busy beaver number for the program under consideration. What am I missing?
[1] I'm aware there's no unique BB sequence, I don't know that the rigorous phrasing is.
Yes. There's even a practical way to check if a finite deterministic machine has repeated a previous state. Run two of them in parallel, in lockstep so that one takes two steps while the other takes one. If they ever have identical state, they're in a loop. This takes 1.5x the compute power plus 2x as much memory, so it's far cheaper than storing all previous states.
(Some early mainframe era educational interpreter supposedly did this, to stop simple student infinite loops quickly in a batch system.)
Here's a paper on the busy beaver problem which discusses upper bounds.[1] The key here is that the upper bound on states is not computable. However, if you force an upper bound by limiting memory, it becomes computable. But really hard. That paper discusses how very rapidly the number of states grows for that problem.
[1] https://homepages.hass.rpi.edu/heuveb/Teaching/Logic/CompLog...
This is useful. Verifiers which work by symbolic execution examine large numbers of cases they work through the control flow. Each case can contain a large number of states; you only need one case for each control flow pattern. Now, some programs run into combinatorial explosion when you do that. The number of cases to be examined grows rapidly. That means halting detection is NP-hard, not impossible. There's a difference.
The Microsoft Static Driver Verifier operates on the assumption that if symbolic execution doesn't terminate after a reasonable amount of automatic analysis, your driver doesn't get to run in the kernel. This is a good, practical solution.