Abstract State Machines (ASMs) provide a model of computations on structures rather than strings. Blass, Gurevich and Shelah showed that deterministic PTIME-bounded ASMs define the choiceless fragment of PTIME, but cannot capture PTIME. In this article deterministic PSPACE-bounded ASMs are introduced, and it is proven that they cannot capture PSPACE. The key for the proof is a characterisation by partial fixed-point formulae over the St\"ark/Nanchen logic for deterministic ASMs and a construction of transitive structures, in which such formulae must hold. This construction exploits that the decisive support theorem for choiceless polynomial time holds under slightly weaker assumptions.

翻译：抽象状态机（ASMs）提供了一种基于结构而非字符串的计算模型。Blass、Gurevich 和 Shelah 证明了确定性多项式时间有界 ASMs 定义了 PTIME 的无选择片段，但无法捕捉 PTIME。本文引入了确定性多项式空间有界 ASMs，并证明它们无法捕捉 PSPACE。证明的关键在于利用 Stärk/Nanchen 逻辑中确定性 ASMs 的偏不动点公式刻画，以及构造一种传递结构，使此类公式必然成立。该构造利用了无选择多项式时间中的决定性支撑定理在略微弱化的假设下依然成立这一事实。