I have to admit my knowledge of complexity theory doesn’t extend too far, but isn’t the solution to LBAs just.. brute forcing? Also, is it even decidable a priori whether a program is LBA vs requiring a tape that is not only linear function of its input?
The worst case solution is just brute forcing, yes.
An LBA is effectively "just" a Turing machine that has a finite tape.
A typical current computer is an LBA only if you disallow all IO of any sort or bound that IO and include it as part of the system you analyse and so fix the values which will be provided as IO, which of course is a very unusual situation, and so that constraint does not really make the halting problem more tractable in situations we usually care about.
The naive way of deciding it it halts is executing it and keep track of all state between steps. If the machine halts, you're done, if it repeats a state, it's looping.
If you can represent a program with an LBA, it is by definition a context sensitive language and decidable. You could also show it by making a equivalent gramma for the language, that accepts the same input as the program. This gramma must be constructed in a certain way, and then you know it is a context sensitive language.
