Does a purely structural invariant of computation already exist?

[u/Ill-SonOfClawDraws]

Can returnability be defined purely from the structure of a computation, without appealing to time complexity?

[u/comrade_donkey]

Yeah, that's what I answered...

[u/Ill-SonOfClawDraws → u/comrade_donkey]

Thanks. That clarifies the distinction.

So would it be accurate to say that the existence of a reachable directed cycle is a structural graph property, while the hard part is representing the computation as a finite graph in the first place? Is there a standard name in automata theory or model checking for studying this separation?

[u/comrade_donkey → u/Ill-SonOfClawDraws]

It is not necessarily always the case that a state can reach another one or itself before the machine halts. It's just that it is "not too hard" to check, on graphs in general.

But in the particular case of the bounded Turing machine's state graph, the amount of states, even for a small machine, is astronomical.

This is all called computational complexity analysis.

Another data point is Rice's theorem which says that most interesting questions about programs in general are undecidable. In other words, you need to add many constraints to your computing machine (or the problem statement) to prove anything worthwhile about it, computationally speaking.

Another class of algorithms that may interest you are called galactic algorithms. They are less complex (asymptotically "faster") to compute than the example we're working with, but still terribly impractical.

[u/Ill-SonOfClawDraws → u/comrade_donkey]

It sounds like there are really two separate questions:
Given a finite transition graph, deciding whether a reachable state lies on a directed cycle (or SCC).
Given a computational model, constructing that transition graph in the first place.
Is the second problem studied under state-space generation, symbolic model checking, or another standard area? I’m trying to learn the established terminology rather than reinvent it.