线性有界自动机 (LBA) 是图灵机的受限形式，其中输入磁带是有限的。
例子
证明 LBA ⊂ PSPACE
PSPACE 是上下文相关语言集的超集。
现在证明 LBA=PSPACE，
我们使用磁带缩减空间压缩定理，它指出，
对于每一个 k 带S(n)空间有界离线图灵机 M 和常数 c>0，存在一个单带cS(n)空间有界离线图灵机 N 使得L(M)= L(N)。
以下身份适用于 -
DSPACE( S(n))=DSPACE(O( S(n)))
和 NSPACE( S(n))=NSPACE(O( S(n)))
由于 LBA 是单带 n 空间有界图灵机，因此它遵循 -
LBA= NSPACE(n)---------------------(1)
现在根据萨维奇定理，如果 S 是完全空间可构造的并且S(n)>log(n)那么
NSPACE( S(n)) ⊆DSPACE(S^{2}(n)) -------------(2)
最终证明
LBA= NSPACE(n)......by(1)
⊆DSPACE(n^{2})........by(2)
⊂DSPACE(n^{3})........根据空间层次定理
⊆PSPACE
Space Hierarchy 然后需要S(n)它是完全可以空间构建的。