On the Expressiveness of State Space Models via Temporal Logics
Authors: Eric Alsmann
Lowejatan Noori
Martin Lange
Venue: ICLR 2026 Poster (2026)
Keywords: state space models
expressiveness
temporal logics
Primary area: interpretability and explainable AI

Abstract: We investigate the expressive power of state space models (SSM), which have recently emerged as a potential alternative to transformer architectures in large language models. Building on recent work, we analyse SSM expressiveness through fragments and extensions of linear temporal logic over finite traces. Our results show that the expressive capabilities of SSM vary substantially depending on the underlying gating mechanism. We further distinguish between SSM operating over fixed-width arithmetic (quantised models), whose expressive power remains within regular languages, and SSM with unbounded precision, which can capture counting properties and non-regular languages. In addition, we provide a systematic comparison between these different SSM variants and known results on transformers, thereby clarifying how the two architectures relate in terms of expressive power.

Published as a conference paper at ICLR 2026
ON THE EXPRESSIVENESS OF STATE SPACE MODELS VIA TEMPORAL LOGICS
Eric Alsmann, Lowejatan Noori & Martin Lange
Theoretical Computer Science / Formal Methods University of Kassel, Germany feric. alsmann, 1. ..noori, martin. h
ABSTRACT
We investigate the expressive power of state space models (SSM), which have re- cently emerged as potential alternative to transformer architectures in large lan- guage models. Building on recent work, we analyse SSM expressiveness through fragments and extensions of linear temporal logic over finite traces. Our results show that the expressive capabilities of SSM vary substantially depending on the underlying gating mechanism. We further distinguish between SSM operating over fxcd-width arithmetic (quantised models), whose expressive power remains within regular languages, and SSM with unbounded precision, which can cap- ture counting properties and non-regular languages. In addition, we provide a systematic comparison between these different SSM variants and known results on transformers, thereby clarifying how the two architectures relate in terms of expressive power.
INTRODUCTION
State Space Models (SSM) have emerged as a potential alternative to traditional sequence modelling architectures such as the popular transformer architecture. In this paper, we investigate the expres- sive capabilities of SSM by establishing lower bounds on their computational power. The analysis focuses on two key dimensions that influence expressiveness: the type of SSM layers used and the arithmetic precision employed in computations. We specifically examine diagonal-gated SSM like S6, cf. Gu Dao (2024), where gate matrices can depend on the input but must maintain a diagonal structure, and time-invarte inve-invariant SSM like S4, ef. Gu et al. (2022), where gate matrices remain stant regardless of input. For each model variant, we consider both fixed-width arithmetic, with a constant number of bits for all computations, and log-precision arithmetic, where precision scales logarithmically with input length.
While empirical studies drive much of the progress in sequence modelling, foundational analysis provides complementary insights by establishing what architectures can and cannot represent in principle, independent of training dynamics. Motivated by the recent success of such analyses for transformers (Strobl et al. (2024)), we investigate SSMs using the same logical and complexity- theoretic framework. This allows for a precise relative comparison: we map SSM variants to the exact same logic fragments recently used to characterise transformer variants (e.g., UHAT, AHAT).
We structure our analysis around three conceptual levels of expressiveness. The most fundamen- tal level is pattern matching (linear temporal logic / first order logic), which captures the ability to detect sequences events based on their relative order without counting. Extending this, we con- sider modular predicates, which enable the tracking of periodic positions similar to what positional embeddings in transformer architectures do. Finally, we analyse global counting, which allows for comparing quantities over the entire sequence and strictly necessitates log-precision arithmetic.
By mapping SSMs to these levels, we provide structural guarantees on which patterns are theo- retically learnalle provably impossible for given architecture. We show that diagonal-gates SSM can recognise languages defined by pure-past Linear Temporal Logic on finite traces (PLTL,) with counting capabilities, while time-in invariiit SSM capture languages expressible in fragments with unary temporal operators plus modular predicates. Furthermore, we show that global count- ing strictly requires log-precision arithmetic. The lower bounds established in this paper contribute

---

Published as a conference paper at ICLR 2026
to growing body of research the theoretical foundations of neural network architectures for sequence modelling, complementing empirical observations about their practical performance. Cru- cially, the resulting impossibility proofs identify fundamental architectural bottlenecks, such as the inability of diagonal exeed-precision SSMs to represent non-monotonic patterns like (aa)", which hold independently of the training data or optimization procedure. In this sense, our foundational characterisation complements empirical benchmarks by delineating which tasks are structurally out of reach for specific SSM variants.
RELATED WORK. Recent work on the theoretical foundations of SSM has been related to circuit complexity, cf. Merrill et al. (2024), automata theory, cf. Sarrof et al. (2024), and communica- tion complexity, cf. Zubic et al. (2025). Alsmann & Lange (2025) investigated the computational complexity of verifying SSM. To the best of our knowledge, this is the first paper connecting the expressive power of SSM formal logic.
The work on the formal expressiveness of SSM started with Merrill et al. (2024) who provided upper bounds via circuit complexity. They showed that diagonal gated well as time-invariant SSM working over log-precision as well as models working over fixed-precision (e.g. floating-point) are contained in TC This is the class of functions definable with boolean circuits polynomial size, constant depth and using threshold gates. They also showed that SSM with arbitrary gates, meaning that the gate can be an arbitrary input-dependent matrix, can recognise all regular languages including NC² -complete languages. This implies a strict increase in expressiveness unless TC = NC Further work by Sarrof et al. (2024) provided a lower bound for diagonal gated SSM, proving that they can recognise all star-free languages. They also showed that under certain restrictions this lower bound is tight in the sense that these SSM recognise a regular language if and only if it is star-free. Our work significantly extends the lower bound provided by Sarrof et al. (2024). While they proved that diagonal SSMs (with a specific output function) can recognise star-free languages, Theorem 1 recovers this special case within broader hierarchy. Crucially, we extend the analysis along three new axes: (1) We characterise inne-invriant and mixed SSMs, relating them to modular predicates (PL.TL,, (MDD): (2) analyse the impact of arithmetic precision, showing that log-precision is strictly necessary for non-regular counting languages (like <"I""c"); and (3) we integrate these findings into the existing transformer landscape (UHAT/AHAT), enabling direct architectural comparison. Zubic et al. (2025) showed that SSM working over fixed-precision can only recognise regular languages.
Parallel to the work on the expressiveness of SSM there has been a lot of research on the expressive- ness of transformer architectures via connections to logics (see Strobl et al. (2024) for a survey on these results). The most important work regarding this paper are Yang et al. (2024a), who proved connections between unique hard-attention transformers and first-order logic as well as Barcelo et al. (2024) and Yang et al. (2025), who investigate the counting abilities of several transformer architectures via extensions of linear temporal logic.
2 FUNDAMENTALS
STATE SPACE MODELS. We explore SSM in a generalised setting as presented in Merrill et al. (2024). For a structured analysis of this model, will formalise its architecture following similar approaches as in Sarrof et al. (2024) and Merrill et al. (2024). An SSM layer is defined as a tuple gha, inc, Φ), where ho E Rdd The function gale is a mapping Rd Rdxd, inc is mapping Bd + Rdd and è is mapping Fd x Rd + Rd. An SSM layer transforms an input sequence of vectors 2 I ( into an output sequence 2 ... Zg E (IRd) through the following process: it computes an intermediate sequence h1 ... h4s E ( via the linear recurrence
h = gale((;) h--1 1 + inc( for 1 1suk
and subsequently generates the output via 2, = 6(h, x:).
An SSM S comprising L layers processes sequences over a finite alphabet Σ. It is expressed as a tuple S = (emb,41 ... LL. out). Each 4, refers to a layer as defined above, while emb is a function Σ- - Rd and out is function Rd + Rd. The SSM computes function Σ" IR as fol- lows: let a = .....
o E Σ' be a word. Initially, the SSM computes the embedding xf x.. of the word by setting a!! = emb(az). Subsequently, for each layer 1 I j < L compute
2

---

Published as a conference paper at ICLR 2026
2x 1) Each layer's output serves the input for the succeeding layer, 2/....2/ 1, [x] 2.
meaning ait ... xx+1 zi.... z- The SSM's final output, denoted as y1 yy.... yk. derived by applying out element-wise. y, = out")))) In the end, the output of S(o) is computed by yk- We say that S accepts a word o if S(r) 1. Otherwise it is rejected. We denote the language accepted by S as (S).
Recent work on the expressiveness of SSM, cf. Merrill et al. (2024) and Sarrof et al. (2024), distin- guishes between two main classes of SSM which differ in the allowed gate functions. The class of time-invariant SSM, cf. Mehta et al. (2023) and Orvieto et al. (2023), only allow layers with gate functions such that there is a matrix A E R with gate(æ) = A for x E R. The class of diagonal-gate -ated SSM, cf. Gu & Dao (2024), De et al. (2024) and Yang et al. (2024b), only allow layers that use gate functions such that gate(z) (z) is a diagonal matrix (with non-negative entries) but can depend on ac. Some SSM architectures like RetNet from Sun al. (2023) use diagonal time- invariant gates. We call SSM which combine diagonal as well as time-invariant layers mixed. To the best of our knowledge, mixed SSM have not been used in practice yet, but they are interesting from a theoretical point of view as upper bounds on expressiveness for those directly apply to time- invariant and diagonal SSM. We therefore include them in our investigation. Lastly, we call SSM which do not have any restriction on the gate- moch-mechanism, cf. Hasani et al. (2022), arbitrary. The global output out and the output of each layer é which also gets the initial input modelling a residual connection is computed by non-linear function. In practice, different kinds of non-linear functions are used. In this paper we assume them to be represented by Feedforward Neural Network (FNN) with ReLU activations.
ARITHMETICS. In our expressiveness analysis, we consider two distinct settings for the arithmetic precision of SSM computations. First, we examine fixed-precsiion arithmetic, where all values and computations use constant number of bits b (like floating-poin regardless of the input length. We say that an SSM works over fxxed-rrcisioo arithmetic if all values and computations are carried out using only these b bits. We additionally assume that the fixed-precision arithmetic is saturated, meaning that if an overflow occurs, the result is capped at the maximum representable value (resp. the minimum representable value for underflows) and that arithmetic operations are monotonic with respect to rounding. This is standard behaviour in, e.g., floating-point arithmetic, cf. 876 (2019). Second, we study log-precision arithmetic, where the precision grows logarithmically with the input length- eength-seccificllly specifically, using O n) bits for inputs of length n. This setting was studied with regards to expressiveness both for SSM by Merrill et al. (2024) and for transformer architectures by Merrill & Sabharwal (2023) and Hao et al. (2022), as it is both practically reasonable and theoretically significant: it provides sufficient precision to accurately count occurrences or compute sums that grow linearly with input size, while avoiding the unrealistic assumption of unbounded precision. This balanced approach is particularly interesting because offers middle ground between the restrictive ixee-precision model and the impractical unbounded precision model.
fixed-point representations),
LINEAR TEMPORAL LOGIC OVER FINITE TRACES, We use linear temporal logic over finite traces (LTL,) as introduced by De Giacomo & Vardi (2013) to analyse the expressiveness of SSM. extends propositional logic with temporal operators, enabling the expression of properties that involve the ordering and timing of events. We consider the pure-past fragment PLTL, of LTL, as studied by De Giacomo et al. (2021), which uses the temporal operators yesterday Y ("at the previ- ous position"), previously ("at some point in the past") and since S ("since some event occured, another event occured continuously"). Let P be a finite set of atomic propositions. The syntax of PLTL is defined as follows:
:==-
p
up
40 A xp Y
3

---

Published as a conference paper at ICLR 2026
Formulas of PLTL, are interpreted over finite words the alphabet Σ 2P. Given word
0 01 10..0000 on E Σ and i E {l...., n), the semantics of PLTLy is inductively defined as follows:
o, = p
peo,
0,1 F 7p
- o, +
0,1 F AA V
0, F p and o, 0,i v
0,1 YYp
- i> and a, 1,i-1F
0, PP
0,1 = 4
= 3iskgi:o. v and f.a & <jSiio,jt
We say that a is model of iff an F p (or simply a F () Furthermore, we denote the language of formula as L(Ø) fo Ex l0 = 9) We typical abbreviations tt (always evaluates to true), (always evaluates to false) and H = - (p holds on all past positions). Furthermore, call the unary fragment of PLTL,, which only uses yesterday and previously, UN-PLTLf.
COUNTING EXTENSIONS. Yang & Chiang (2024) and Barcelo et al. (2024) analysed the expres- sive power of several transformer architectures, regarding the ability to do counting, by extending LTL, with counting operator. PLTL s # extends PLTL, syntactically by one additional .4 are PLTL, # formulas, ai ai, ai,bi,, ..,b,,,.b, 2, c E and
case: ".....,,, 1,,,
~E {<, 2. then
Σa Pi + Σ bj 2 ~c
is also PLTL, #1 formula. When evaluating formula word and position i, # yp counts the number of positions j S i such that o, F and # does so analogously for positions j 2 i.
By p we denote the logic in which every counting subformula has by for all j. The use of # (and not # is tied the nature of SSMs: unlike transformers with full sequence attention, SSMs only have access the prefix of the input at each step.
MODULAR PREDICATES. We introduce third variant of PLTL, which adds modular predicates. The syntax of ,LTL, [MOD] is extended by additional atomic formulas MOD." for m > and S r < m. The semantics the same in PLTL,. For the new operator it is extended by
+= MOD." - iir
(mod m)
Crucially, allowing these modular predicates strictly increases the expressive power beyond star-free languages (which correspond standard PLTL,). It enables the definition of periodic properties, such as recognising the language (aa)", which necessitates distinguishing even from odd positions. Formally, this extension lifts the expressiveness to the class of all regular languages definable in AC (Straubing, 1994). This complexity class serves key reference point in later analysis, as we will show that it aligns with the capabilities mixed SSMs and transformers equipped with positional encodings.
RESULTS
Our analysis establishes lower bounds SSM expressiveness across different architectural variants and precision settings. The results reveal an interesting hierarchy where expressiveness varies sig- nificantly based on gating mechanisms and arithmetic precision. An overview of these findings illustrated in Figure 1. It also shows how our fragments of PLTL, relate to circuit complexity and first-order logic. detailed explanation of these connections can be found in Appendix A.I.
DIAGONAL SSM. Theorem demonstrates that diagonal SSM with fixed-width arithmetic can recognise the languages definable in PLTLy, which corresponds to the class of first-order definable frrefree regular languages. This result constructive: show how to systematically translate any FLTL, formula into an equivalent diagonal SSM by decomposing the formula according to its nesting depth and implementing each temporal operator through appropriate gate mechanisms.
4

---

Published as a conference paper at ICLR 2026
The key insight underlying this construction is that while temporal operators like and can be im- plemented using simple gating patterns, the since-operator requires input- nepu-deepnndent diagonal gates due to its recursive definition (p v & V (p y(p v)). This dependency current input evaluation necessitates the diagonal structure of the gates.
We complement this lower bound with matching non-expressibility result. Theorem 3 proves that diagonal SSM with fixed precision cannot recognise the simple non-star-free language (aa)". This limitation arises from a fundamental monotonicity property (Lemma 2): when diagonal SSM repeatedly processes the same input symbol, its output must eventually stabilise.
When diagonal SSM are equipped with logarithmic precision arithmetic, their expressiveness pands considerably. Theorem 4 shows that these models can recognise all languages definable in pLTL [ pure-past LTL extended with backward-looking counting operators. Barcelo et al. (2024); Yang & Chiang (2024) also used this logic to investigate the expressiveness of transformer architectures. The extension by counting formulas enables the recognition of non-regular (and even non context-free) languages, such as {a"b"c" n 2 0}, which can be expressed by
= H ((a -((b (Plb)c)) (b -Pc) ^ ( a $ b- (#H # b =
SSM. While we conjecture that time-invariant SSM cannot express the tem- poral dependencies captured by the since-operator (Conjecture 1). they possess another capabil- ity: the computation of modular predicates about sequence positions. Lemma 6 demonstrates how time-invariant SSM can maintain counters modulo m using cyclic permutation matrices, enabling recognition of languages like (aa)* that are beyond the reach of diagonal SSM with fixed precision.
This leads to the characterisation in Theorem 7: time-invariant SSM with fixed precision recognise all languages definable in UN-PLTL, MMOD], the unary fragment of pure-past LTL extended with modular predicates. With logarithmic precision, they can additionally handle counting operators, recognising languages in UN-PLTL, (OD, #1.
MIXED AND ARBITRARY GATES. Our hierarchy is completed by considering SSM that combine multiple gating mechanisms. Corollary 8 establishes that mixed SSM (combining both diagonal and time-invariant layers) with fixed precision recognise all regular languages in AC effectively capturing the union of capabilities from both individual architectures. SSM with arbitrary gates achieve even greater expressiveness, recognising all regular languages as established in prior work by Merrill et al. (2024).
EXPRESSIVE POWER OF DIAGONAL SSM
We show that diagonal SSM least as expressive as PLTL,, which expressively equivalent to the set of star-free languages. This follows the lines of Sarrof et al. (2024) but we use it as the base for further constructions regarding extensions and restrictions of PLTL,,
In order to evaluate PLTL, formula at position i of a word a, one can evaluate the subformulas of op a bottom-up manner. We order the subformulas such way that every subformula evaluated after its own subformulas. Independent subformulas can be evaluated in parallel (in single SSM layer). This means that the number of layers needed for all our constructions corresponds to the depth of the syntax tree of formula ş2, here called nesting depth for brevity.
Definition 1. The nesting-depth nd(ss) of PLTL, formula is defined inductively: nd(p) (MOD O, nd(ip opin v) max(nd( (5)), (d)) + 1. nd((an sp) = nd(p) + 1 and nd E #
H ~c) max(nd((p,) S j < k} with Obin E (A,S} and cun
Y-,P.Y).
This allows us order the subformulas of y in the way described above. For each subformula v of ip, we construct a diagonal SSM layer lg which computes for each position whether a, í F db The SSM S.P for the whole formula oo then computes whether ar, n += s. A similar idea has already been used by Alsmann & Lange (2025) to show that the satisfiability problem for diagonal SSM over fixed-precision is PSPACF-cooplete.
5

---

Published as a conference paper at ICLR 2026
SSM with arbitrary gates
REG (Merill (2024)
SSM with mixed layers
TC (Merrill at. (2024))
Corr, 8
PLTL [OD] = FO|K, KOD] = REG n AC
(itt prec.)
Dog. prec.
SSM with diagonal gates
SSM with time-invariant gates
Thm.
2 PLTL, FO[<]
Thm.
2 UN-PLTL, [MDD] s ro* MOD]
(fin. prec.
(fin prec.)
Thm
2 PLTL
(log, prac. 2 UN-PLTL, (#, MOD]
Thm.
(log. prec.
SSM with diagonal time-invariant gates Cor
UN-PLTL, [F+
dlgg. prec.
Cur
UN-PLTL,
Figure I: Expressiveness hierarchy of SSM architectures mapped to logical fragments and complex- ity classes. We establish lower bounds for Diagonal, Time-Invariant, and Mixed SSMs, distinguish- ing between txed-precision and log-precision (enabling counting operators #). Dashed arrows indicate provably strict inclusions (Theorem 3). The gray box delineates the TC upper bound from prior work (Merrill et al., 2024).
Theorem 1. Diagonal SSM with Exeed-peecsioon recognise all languages definable in PLTL,.
Proof sketch. The detailed proof can be found in Appendix A.2. Each subformula corresponds to one dimension of the SSM's hidden states. The increment function of each layer together with the position-wise FNN add information about subformulas evaluated in previous layers and take care of the non-temporal subformulas such as conjunctions, negations and comparisons. After each layer, each hidden state is a boolean vector, indicating which subformulas are satisfied at each position. The temporal operators Y and can be implemented by diagonal and time-invariant gates, because they do not require any conjunctions with the current input. consistently references the imme- diately preceding position, and accumulates occurrences up to the current point. In contrast, the since-operator is inherently recursive, defined by y S & (p A y(pp v)). thus combining previous and current states through conjunction. Evaluating this operator inherently depends on the current input evaluation of yo, necessitating an input-dependent gate.
Li
Next, show that this characterisation is tight in the sense that diagonal SSM working over fixed- precision cannot recognise (aa)*, which is not definable in PLTTL,, This non-expressiveness result based on monotonicity property of diagonal SSM working over fixed-precision Any diagonal SSM working over fixed-precision after repeatedly seeing that same input must eventually become constant.
Lemma 2. Let S be diagonal SSM over alphabet E. For E, let :N - Fd be the function defined by fo (n) Yn. where yn is the last vector of the output sequence of S after the last layer on the word σ². Then there exists number N M such that for all > N: fo(n) = (N)...
Proof. The key insight is that since the gate matrices are diagonal, each dimension of the hid- den state evolves independently. For the first layer this means that for each dimension i, (h+); gate (ate(emb(r)))- (h:-1); + ine( inc(emb(a)); Because the gate is non-negative, this sequence must be monotonic. Given the fixed-precision arithmetic, each dimension can only take on a finite number of distinct values. Therefore, as t increases, each dimension must eventually stabilize to constant value. This implies that there exists some such that for all n 2 N, the output of the first layer remains constant. The same argument applies inductively to each subsequent layer, leading to the conclusion that the entire SSM's output stabilises after a finite number of repetitions the input symbol.

---

Published as a conference paper at ICLR 2026
The following is direct consequence of Lemma 2 and the fact that (aa)* is not monotonic in the sense that there are words in the language that can be extended to a word not belonging to the language and vice-versa.
Theorem 3. No diagonal SSM with -xeed-preiision can recognise (aa)".
Proof. Assume that there exists diagonal SSM S recognising (aa)". By Lemma 2, there exists number N such that for all n 2 N: fa(n) = (N). This means that S either accepts or rejects all words of the form a" with n N. contradicting the assumption.
Lemma 2 showed that diagonal SSM behave montonically for each input symbol. With diagonal SSM, even though they have monotonic behaviour for each input symbol, they can still "reset" the hidden state when seeing a different symbols and thus evaluate the since-operator.
Having characterised the expressiveness of diagonal SSM working over fixed-precisio, we now turn to diagonal SSM working over log-precision. In this setting, diagonal SSM can also recognise non-regular and even non-context-free languages. This was already observed by Sarrof et al. (2024). Also, Alsmaan & Lange (2025) showed that the satisfiability problem for this class of SSM is undecidable. We show that diagonal SSM working over log pre-ciiciinn can recognise all languages definable in FLTL, extended by the backward-looke looking counting operator #
Theorem 4. Diagonal SSM with log-precision recognise all languages definable in PLTL,
Proof sketch. The detailed proof can be found in Appendix A.2. The proof is an extension of the proof of Theorem 1. Given a counting subformula Σ Oj # fj ~ c, we add one layer to the SSM which counts the occurrences of each ;i in the hidden state using the increment function. The position- wise FNN then checks whether their linear combination satisfies the comparison with and writes the result into the corresponding dimension of the hidden state. The rest the construction remains unchanged. As this construction does not require any non-diagonal gates, it also works for time-invariant diagonal SSM.
5 EXPRESSIVE POWER OF TIME-INVARIANT SSM
As established in the previous section, diagonal SSM can evaluate all formulas in PLTL,. However, the since-operator inherently requires input-dependent gates. This raises the question of whether time-invariant SSM, which have constant gates, can evaluate the since-operator. We conjecture that they cannot, and thus cannot recognise all languages definable in PLTTL.3
Conjecture 1. No time-invariant SSM with fixed-rrecision can recognise I. (aSb) over = {a,b, c)..
The intuition behind this conjecture is that the since-operator requires combining information from the current imput with information from previous positions way that depends on the current input. While time-invariant SSM can "reset" the hidden state when seeing a different symbol, time- invariant cannot adapt their gate based on the current input symbol. Due to this limitation, the only difference between seeing a b or e in a word, lies within the additive ine-part of the SSM. Our suspicion that time-invariant SSM trying to recognise a b will eventually reach point, where they loose track of whether the last non-a symbol was a b or this happens are a = az (ca"ba") and a' a² (ba"ca") ym for large n1 m. A formal proof this conjecture however is difficult for two reasons. First, the behaviour of time-invarian SSM is more complex than that of diagonal SSM, as the dimensions of the hidden state can interact with each other. Second, due saturation effects in fixed-precision arithmetic and the fact the fixed-precision arithmetic is not associative, the behaviour of time-invariant SSM is difficult to analyse.
Good candidates for words where
As the since-operator is the only temporal operator which needs input-dependent diagonal gate we get the following immediately for the case in which the SSM layers are both diagonal and time- invariant. Without the since-operator, diagonal and time-invariant SSM can recognise languages in the unary fragment of PLTL,--
Corollary 5. SSM with layers that are both diagonal and timeinvariant can recognise all languages definable in UN-PLTL, fixed-width arithmetic.
[ under org-iiiciioon arithmetic, and those definable in UN-PLTL, under
7

---

Published as a conference paper at ICLR 2026
While being possibly less expressive than diagonal SSM, time-invariany and non-diagonal SSM can still recognise languages which are not definable in pLTL,. We demonstrate this by showing that time-invann invariant SSM can compute modular predicates about sequence positions. For any position in a sequence, modular predicates determine whether has a specific remainder when divided by some modulus m. This ability originates from the possibility of time-invariant SSM maintain counter modulo m in their hidden state using cyclic permutation matrix as the gate.
Lemma 6. For any integer m 2 2, there exists a time-invariant SSM layer INOp that outputs e, Rd position if and only if (mod m).
Proof. We construct the SSM layer IMOD follows. The initial state ho e1, the first standard basis vector. The gate matrix P is the cyclic permutation matrix that maps e; to ei+1 for I,..., m-1 and em e1. Specifically, all of P's entries zero except for ones the subdiagonal and in position (1,m):
0
0
0
0
1
0
0
0
P
0
1
0
0
0
The increment matrix B is set to zero, since the predicate depends only on the position and not on the input. The key insight is that the hidden state evolves as h, Ph P' P'e Since is cyclic permutation of order we have pm = I, and thus Plei E(t mod m)+1- This means that, at each position I, the hidden state is exactly the standard basis vector whose index encodes the remainder of modulo m. At position t, the state he has in position (t mod m. + and O's elsewhere. D
Example 1. To illustrate the concept of modular predicates, consider MOD?. which determines whether a position is odd. Here m 2, so the permutation matrix is (i d) and the initial state hg = (1,0)T. The state sequence alternates between e; (0. 1)" at odd positions and Co = (1, 0) at even positions.
The eyclic permutation effectively maintains a counter modulo m in the hidden state, enabling the computation of any modular predicate with a single time-invariant SSM layer. This especially allows non-star-free languages to be defined, e.g. T(Ha A MOD (aa)", " which are not definable in PLTL,, cf. Straubing (1994). In this sense diagonal and time-invariant SSM are incomparable in expressiveness, diagonal SSM cannot recognise (aa)* and time-invariant SSM seem to be unable to recognise L(a S b).
Theorem 7. Fine-invarian SSM with fixed-precision recognise all languages definable in UN-PLTL, [MOD] and time-invariant SSM with log oog-precision recognise all languages definable in UN-PLTL, MOD, #1.
Proof sketch. The detailed proof can be found in Appendix A.3. It is similar to the proof of Theorem 1. The main difference is that need to add layer for each modular predicate MOD." appearing in the formula. This layer constructed as described in Lemma 6. The rest of the construction remains unchanged. As this construction does not require any non-diagonal gates, it also works for time-invariant diagonal SSM.
Having established lower bounds for diagonal and for inverinvariant SSM, it seems natural to con- sider SSM that are either diagonal or inme-invariant in each layer. Mixed SSM can evaluate both the since-operator and modular predicates. This allows us to show that mixed SSM with fixed-precision can recognise all languages in (LTLLy(MOD) which are exactly the regular languages AC ef. Straubing (1994), the class of languages recognised by constant-depth polynomial-size circuits with unbounded fan-in. This class contains all star-free languages as well as languages like (aa)". The
same holds for mixed SSM with log- precision and PLTL, MMDD #1.
Corollary 8. Mixed SSM with fixed-precision recognise all regular languages in AC With log- precision they recognise all regular languages in PL.TL, (#, (H, MOD].
8

---

Published as a conference paper at ICLR 2026
FO|<, MOD] X mixed SSM (Omn.
UHAT' PE (hong ctal (2024a1)
FO
UN-PI.TI. [MDD]
S diagonal SSM conn
time-invariant SSM (then.
UIAAT (Yegge (2044
UN-PLTL, < diagonal lime-invariant SSM (Cun.
Figure 2: Detailed comparison of fixed-precision SSM variants with Unique Hard-Attention Trans- formers (UHAT) Yang et al. (2024a). The diagram illustrates structural alignment: Diagonal SSMs capture star-free languages (FO[<], matching the capabilities of UHAT without positional encod- ings. Time-invariant layers introduce modular predicates, providing an expressive lift analogous to adding Positional Encodings to transformers. Consequently, mixed SSMs capture the full class FO[<, MOD] (regular languages in AC
COMPARISON TO TRANSFORMER ARCHITECTURES
In this section we will discuss how the results on the expressiveness of SSM fit into the broader landscape of recent results on SSM expressiveness and the comparative expressivity of various trans- former architectures.
Transformer architectures studied in the formal expressiveness communities can be classified into two main categories: those with hard attention mechanisms and those with soft attention mecha- nisms. Hard attention transformers, e.g. unique hard-attention (UHAT) and average hard-attention (AHAT), use a discrete attention mechanism that allows them to focus on specific parts the in- put sequence. In contrast, soft attention transformers (SAT), like the original transformer model by Vaswani et al. (2017) and its variants, employ a continuous attention mechanism that computes weighted averages
the entire input sequence. While unique hard-attention transformers can only attend to one position in the sequence, average hard-attention and soft-attention transformers attend to multiple positions, allowing them to count occurrences of certain properties. This dif- ference corresponds to the difference between fixed-precision and log-precision arithmetic in SSM.
Additionally due to the nature of the attention mechanism, transformers cannot distinguish between different positions in a sequence without additional positional encodings. These encodings provide the model with information about the order and position of elements in the sequence. In contrast, SSM inherently encode positional information through their recurrent structure. But as observed in Section allowing time-ivarriant SSM layers increases expressivity because the model can also maintain counter modulo m in its hidden state, enabling them to compute modular predicates about sequence positions. Just as allowing time-invariant SSM layers, adding positional encodings to transformers also allows them to compute modular predicates, cf. Yang al. (2024a) and Barcelo et al. (2024).
Yang et al. (2024a) established that unique hard-attention transformers (UHAT) can recognise all languages definable in first-order logic with the order predicate (FO(<) and that adding positional encodings (UHAT+PE) allows them to recognise all languages definable in FO[K, MOD]. This aligns with our results on diagonal and time-invariant SSM working on exeedppecissoo, as can be seen in Figure 2. Analogously, Barcelo et al. (2024) showed that average hard-attention transformers
(AHAT) can recognise all languages definable in PLTL, H # .MDD]. This aligns with our results on mixed SSM working on precisicin The increase in power of AHAT is due the transformers' ability to attend to all positions in the input sequence. Yang & Chiang (2024) investigated the counting abilities of soft-attention transfommers (SAT) by analysing logic called C-RASP and its extension C-RASP[MOD). C-RASP corresponds to a strict subset of UN-PLTL, [+), which we show in Appendix A.4. Figure 3 shows how our results embed into the existing literature.

---

Published as a conference paper at ICLR 2026
PLTL, S AHAT
PF: (havekee OENN
PLTL,
PLTL, MCD mixed
S diagonal SSM me.
UN-PLTL, diagonal
UN-PLTL MOD
invariant
C-RASP < SAT 2324
C-RASPIMOD]
S SAT PE Vew
Figure 3: Comparative hierarchy under log preciisii.on. enabling counting capabilities. The diagram positions SSM variants relative soft-attention (SAT) (Yang & Chiang, 2024) and average hard- attention transformers (AHAT) (Barcelo et al., 2024). While SSMs strictly subsume the logic of SAT (C-RASP) due to superior local temporal processing (e.g., the Yesterday operator), they remain strictly less expressive than AHAT+PE. This separation arises from causality: SSMs are limited to lockkadd counting (#) whereas the global attention of AHAT allows for forward-looking counting (#)
7 OUTLOOK
We established lower bounds the expressiveness of various SSM architectures by demonstrating their ability to recognise languages defined by different fragments temporal logie. The results, as visualised in Figure 1, provide a comprehensive picture of the expressiveness hierarchy among resulting implications
SSM variants. While our analysis relies on explicit weight constructions, robust training methodology. Specifically, our separation results establish hard architectural limits: for instance, the monotonicity lemma implies that a diagonal fixed- exxed-reccssio SSM cannot be trained to recognise non-star-free free languages like (aa)*. regardless of the optimizer or dataset size. Furthermore, they reveal an interesting gap between the lower bounds established here and the known upper bound of TC established by Merrill et al. (2024). The language classes that are shown here to be recognisable by various restricted SSM architectures with fixed-width arithmetic lie within AC proper subset of TC This suggests two possibilities: either the TC upper bound can be tightened to AC for these SSM architectures, or these SSM can actually recognise languages outside of AC such as parity. The first possibility seems more plausible, as we have not identified any mechanism in these SSM architectures that would enable counting modulo some constant-a capability required for recognising parity and other languages outside of AC Sarrof et al. (2024) even proved that diagonal SSM cannot express parity, but only for specific choice of non-linear layer output functions. If this is indeed the case, would align SSM with unique hard-attention transformers which have also been shown to be limited to AC cf. Hao et al. (2022).
Moreover, investigating potential expressiveness hierarchies based on formula nesting depth could provide finer- finer-grained complexity classifications. Similar expressiveness hierarchies have been proved for unique hard-attention, cf. Yang et al. (2024a), and soft-attention transformers, cf. Yang al. (2025).
REFERENCES
IEEE standard for floatingppoin arithmetic. IEEE Sid 754-2019 (Revision of IEFE 754-2008), pp- 1-84, 2019, doi: 10.110//FFFSSTD2221999766
Eric Alsmann and Martin Lange. The Computational Complexity of Satisfiability in State Space Models. In ECAI 2025, pp. 1768-1775. IOS Press, 2025. doi: 10.3233FFAA2251006.
10

---

Published as a conference paper at ICLR 2026
Raman Arora, Amitabh Basu, Poorya Mianjy, and Anirbit Mukherjee. Understanding Deep Neural Networks with Rectified Linear Units. In International Conference on Learning Representations, February 2018.
Pablo Barcelo, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. Logical languages accepted by transformer encoders with hard attention. The Twelfth International Conference on Learning Representations, 2024.
Soham De, Samuel L. Smith, Anushan Feraand,, Aleksandar Botev, George Cristian-Muraru, Al- bert Gu, Ruba Haroun, Leonard Berrada, Yutian Chen, Srivatsan Srinivasan, Guillaume Des- jardins, Arnaud Doucet, David Budden, Yee Whye Teh, Razvan Pascanu, Nando De Freitas, and Caglar Gulcehre. Griffin: Mixing Gated Linear Recurrences with Local Attention for Efficient Language Models, February 2024.
Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI '13, pp. 854-86 860, Beijing, China, August 2013. AAAI Press. ISBN 978-1- 57735-633-2.
Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti, and Sasha Rubin. Pure-past linear temporal and dynamic logic on finite traces. In Proceedings of the Twenty-Nint International Joint Conference on Artificial Intelligence, IJCAI'20, pp. 4959 4965, Yokohama, Yokohama, Japan, January 2021. ISBN 978-0- 101-009999211----9
Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279-29) 2002. ISSN 0890-5401. doi: 1.006//nco.200..299.
Michael Fisher, Dov M. Gabbay, and Vila (eds.). Handbook of Temporal Reasoning in Artificial Intelligence. Number 1 in Foundations of Artificial Intelligence. Elsevier, Amsterdam Boston, 1st ed edition, 2005. ISBN
978-0-444-51493-6
Merrick Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hi- erarchy. Mathematical systems theory, 17(1):13-27, December 1984. ISSN 1433-0490. doi: 10.1007/BF01744431.
Albert Gu and Tri Dao. Mamba: Linear- Time Sequence Modeling with Selective State Spaces. In First Conference on Language Modeling, August 2024.
Albert Gu, Karan Goel, and Christopher Re. Efficiently Modeling Long Sequences with Structured State Spaces. In International Conference on Learning Representations, 2022.
Yiding Hao, Dana Angluin, and Robert Frank. Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity. Transactions of the Association for Com- putational Linguistics, Lingussie, 10:800-810, July 2022. ISSN 2307-387X. doi: 10.11120aac.a.00499.
Ramin Hasani, Mathias Lechner, Tsun-Hsuan Wang, Makram Chahine, Alexander Amini, and Daniela Rus. Liquid Structural State-Space Models. In The Eleventh International Conference on Learning Representations, September 2022.
Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. University California, 1968.
Harsh Mehta, Ankit Gupta, Ashok Cutkosky, and Behnam Neyshabur. Long range language model- ing via gated state spaces. In The Eleventh International Conference on Learning Representationss 2023.
William Merrill and Ashish Sabharwal. The Parallelism Tradeoff: Limitations of fog-Precision Transformers. Transactions of the Association for Computational Linguistics, 11:531-545, June 2023. ISSN 2307-387X. doi: 10.1 162/tacl 00562.
William Merrill, Jackson Petty, and Ashish Sabharwal. The illusion of state in state-space models. In Proceedings of the 41st International Conference on Machine Learning, volume 235 JCML'22 24, pp. 35492-35506. Vienna, Austria, July 2024. JMI.R.org.
11

---

Published as a conference paper at ICLR 2026
Antonio Orvieto, Samuel L Smith, Albert Gu, Anushan Fernando, Caglar Gulcehre, Razvan Pas- canu, and Soham De. Resurrecting recurrent neural networks for long sequences. In Proceedings of the 40th International Conference on Machine Learning, ICML'23, M2,,, Honolulu, Hawaii, USA, 2023. JMLR.org.
Yash Sarrof, Yana Veitsman, and Michael Hahn. The Expressive Capacity of State Space Models: A Formal Language Perspective. In The eighth Annual Conference on Neural Information Processing Systems, November 2024.
Howard Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, Boston, MA, 1994. ISBN 978- 1-4612--665-2 978- 1-4612-0289-9 9. doi: 10.1007/978-14462-00333 1-4612-0289-9
Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. What Formal Lan- guages Can Transformers Express? A Survey, Transactions of the Association for Computational Linguistics, 12:543-561, May 2024. ISSN 2307-387X. doi: 20.116//aclaaa00066
Yutao Sun, Li Dong, Shaohan Huang, Shuming Ma, Yuqing Xia, Jilong Xue, Jianyong Wang, and Furu Wei. Retentive Network: Successor to Transformer for Large Language Models, August 2023.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Proceedings of the 31 Inter- national Conference on Neural Information Processing Systems, NIPS' 17, pp. 6000-6010, Red Hook, NY, USA, December 2017. Curran Associates Inc. ISBN 978- 5108-1096-44
Andy Yang and David Chiang. Counting like transformers: Compiling temporal counting logic into softmax transformers. In First Conference on Language Modeling, 2024.
Andy Yang, David Chiang, and Dana Angluin. Masked hard-attention transformers recognize ex- actly the star-free languages. In The Thirty-Fighth Annual Conference Neural Information Processing Systems, 2024a.
Andy Yang, Michaël Cadilhac, and David Chiang. Knee-deep in c-RASP: A transformer depth hierarchy. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025.
Songlin Yang, Bailin Wang, Yikang Shen, Rameswar Panda, and Yoon Kim. Gated linear attention transformers with hardware-efficient training. In Proceedings of the 4 International Conference Machine Learning, (CML''24, Vienna, Austria, 2024b. JMLR.org.
Nikola Zubic, Federico Soldà, Aurelio Sulser, and Davide Scaramuzza. Limits of deep learning: Sequence modeling through the lens of complexity theory. In The Thirteenth International Con- ference on Learning Representations, 2025.
A APPENDIX
A.1 EXPRESSIVE POWER OF PLTL, AND ITS EXTENSIONS/FRAGMENTT
Kamp's theorem Kamp (1968), in conjunction with results from De Giacomo & Vardi (2013); De Gi- acomo al. (2021), establishes that PLTL, is equally expressive to first-order logic over words FO[<], which in turn corresponds precisely to the class of star-free expressions. Similarly, the logic PLTL, [MOD] is expressively equivalent first-order logic with modular predicates MOD], char- acterising exactly the regular languages contained in AC Straubing (1994). The unary fragment UN-PI.TL.f constitutes a subset of languages definable in the two-variable fragment of first-order logic FOR Etessami et al. (2002). While UN-PLTL, is restricted to the unary temporal operators yesterday and previously, FO* fully characterises languages definable in L.T., using the unary operators yesterday, préviously, next, and sometimes in the future. One can show that UN-PLTLL must be a proper subset of FO² [<] as the standard construction for separating temporal formulas into past and future components Fisher et al. (2005) relies on the since operator. This relationship extends to the modular predicate extensions, with UN-PL.TL, MMDD] forming proper subset of FO MOD].
12

---

Published as a conference paper at ICLR 2026
Regarding the counting extension to fLTL,, observe that restricting to counting subformulas with exclusively positive weights does not enhance expressiveness. However, incorporating neg- ative weights enables the representation of non-regular languages that may lie outside AC For instance, consider the language {w {a,6)* Iw]a- ] consisting of strings with equal occur- rences of and b. This language falls outside AC Furst et al. (1984), yet can be concisely expressed even in P [#]
with the straightforward formula #
# O.
A.2 PROOFS OF SECTION 4
FEEDFORWARD NEURAL NETWORKS. An (FNN- is a function V: R R with v(x)
relu(E; C,2, + b). where l is the input dimension, the C E R are called weights, b E R is the biay and relu IE + R with relu(x) max(0, x)) is the activation function of v. An (FNN-)layer I is tuple of some n nodes (U1...., Un) where each node has the same input dimension m. computes the function (: IT + R" via ((x) the output dimension of I. A Feedforward Neural Network (FNN) N consists of k layers ......, lu. where 1 has input dimension m. the output dimension of 1 is equal to the input dimension of 4,41 for < and the output dimension of 4 is n. The FNN N computes a function from Ih' to R by N (xx) lx (1 (z:)...))
E.....,.,(.)). (z)).) We call the input and
For lower bound constructions we sometimes need to make use of FNN checking specific properties. for instance: is some vector entry equal specific value? For easier notation we will define FNN gadgets for specific properties we will need later.
Lemma 9, Let n, R1, ... nk. m, b E Z. There are FNN
Nob s.t. (n)(n)= = if n- ~ b and (n) otherwise, for all =,,,,
Nmin(0,a) s.t. Nminno..) (n) = min(0. z))
-2 2- 2-luuurr - b)), Noc be the FNN computing Nzs(x) = relu (relu(b + 1 x) relu(b x)). N2b be the FNN com- puting N N2)(2) = relu (relu(x - (b 1)) relu( - b)) and Nmin(1.x) be the FNN computing Nmin(1.2) (x) = relu(x) ) - relu(-x)
Proof. Let N be the FNN computing N=o(x)= = retu (relu(x - (b (b- 1)) 1))
relu(x (x - 1). Since we only work over integers, we can rewrite & < b to x < b - and > b to 2 b + 1. It is straightforward to see that the given FNN compute the required functions.
We will sometimes need combine FNN. Let Ni and N₂ be FNN computing functions R R
for i E 21. The composition of N2 and N2 is defined as follows. When n22 = m.. the FNN Ni N2 computes the function RT - R"1 with N1 N2(2) = Ni (N2(z)). Syntactically, composition simply concatenates the output layer of N2 and the input layer of N₁ setting all weights 1.
To simplify notation, we define the gate and increment functions of diagonal SSM layers using linear projections. For fixed matrices A, B, let gate(x;)) = diag(Ar,) and inc(x;) = Bæg, This reduces the diagonal SSM layer recurrence to
h = (Axx)) o h4-1 + Ba,,
where a denotes element-wiss multiplication. We leverage the sequential decomposition of PLTL, formulas to construct an SSM evaluating subformulas layer-wise according to increasing nesting depth.
Definition 2 (Sequential Decomposition). Let & be an LTL, formula with nd((p) n. The se-
quential decomposition of & is the unique sequence of sets Mo..., M.,,...,, with M, = {vC E Sub((p) nd(w) (b) i).
First, we construct the translation for each temporal operator individually, then provide the complete construction by induction over nesting depth. Given a PLTL, formula o over propositions P = ((1a................. ... ...,a),, J. fix an injective function P U Sub((p) (1) + {1...., |P| + (i + 1), assigning each proposition p = a; to index i. The assignment for remaining subformulas is arbitrary. This ordering assigns each subformula fixed index within vectors computed by the resulting SSM,
13

---

Published as a conference paper at ICLR 2026
which has dimension d = | |gl + + The final dimension in each vector is set to the constant 1. For case of defining linear projections, we introduce the copy matrix ((++-)) e Idddd defined by C(i+-) = e,e,, for indices < j I d. Multiplying vector z E IR by C(i+s) yields a vector whose j-th component IG, with zeros elsewhere.
Theorem and Theorem 4 are direct consequences of the following more general result. Which we will prove the end of this section.
Theorem 10. Let up be a , (##) formula over propositions P. Then there exists an SSM S over alphabet E =P of dimension d = [P] + lypl 1 with exactly nd((p) layers, satisfying the following: For every word a E Ex with o = n, if y ... is the outpul produced by Sp after the final layer on impul o, then (yt)u(e) if and only if of F v,, and (Wr)aw) otherwise, for all Sub(yp).
positions 1 S t S and subformulas
To prove this theorem, we first require some intermediate results. Specifically, evaluating formulas involving the yesterday-operator necessitates a suitable encoding of prior-step information into the current hidden state via the gate mechanism. This encoding was originally introduced by Sarrof et al. (2024); we provide a self-contained proof adapted to our context.
Lemma 11 (Sarrof et al. (2024)). Let a be a binary sequence o 01a2...-00 On E 13". For every 1 S t S n. we define the number h4 E R recursively by ho = 0 and h4 = 1 h2-1 + ag There exists an FNN Npr which outputs the value a; at position for all & 2 2, and outputs at position 1.
Proof. The hidden state evolves according to h, = { h/-11-11 + a, for t 2 1. Expanding this recurrence, we obtain he = + - 16 0- 64 0- +... The key insight is that when E {0, 1}. the value he has the binary representation at 0a;-1 00:-0002200000 012- This encoding places the current input 0 in the integer part, while previous inputs -; - occupy alternating binary digits in the fractional part, separated by zeros.
To understand why this leads to disjoint intervals, observe that the contribution of all bits from position and earlier bounded: the infinite series 15 4- 64 0t-3 + ... can be at most 1-1/4 12 when all a, 1, and at least 0 when all a, O. Therefore, the contribution of the "tail" is bounded by the interval [0, 1.2.
1 + 256 +... 1/16
16
Given this bound, we can analyze the four cases based on (at, a;-1):
For (ar, ax-1) 1) = (0, 0): We have lo2 0 + 0 tail, so h₁ E [0, +/2
For (at, 1)- = (0, 1): We have h; = + 1 + tail, so h1 E 1 1 + 1/2 [
For (at, Gt-1) 0): We have h; + 0+ tail, so E [1,1+ + = [1,
* For (a,, a1-1) (1, 1): We have h, 1 + 1/2 + tail, so h4 E 12 1 = [9.
These intervals are clearly disjoint. For practical implementation under finite precision arithmetic, we can use slightly tighter intervals with exact binary representations. Since all houndaries can be represented exactly with at most 3 bits after the decimal point, we can safely use: (0, 0) + [0, dl. 1) + 14 1) (1,0) + [1, 3. and 11 + 1 3 These refined intervals maintain the non- overlapping property while providing additional safety margins against rounding errors.
Nprev extracts 6t-1 by mapping the intervals containing (at, at-1) E (),, to output O, and the intervals containing (a,, 1)-1) E (0, 1). (1, (1, 1)} to output 1. This piecewise- function can be exactly represented by an FNN with ReLU activations using standard techniques for imple- menting step functions (Arora et al. (2018)). For t = 1, we have b an and (ap) construction. For t. 2 2, the interval containing h; uniquely determines a which is correctly extracted by Nprev The factor (rather than 2) is crucial as provides sufficient spacing between encoded bits to prevent numerical errors under finite precision arithmetic.
by
Having shown how we can recover information from previous positions in order to evaluate yester- day formulas, we will now show how construct layers evaluating PL.TL, [#] formulas in general.
14

---

Published as a conference paper at ICLR 2026
Lemma 12. Let -n...-n E"
be a word, ,1,,,., 4p be PLTL s formulas and æ1 Bn
be a sequence with the property (xt))(())) =1 + a,t F for all 1 - t S n and 1 < i S k.
Then there are diagonal gated SSM layers for all tà E {-p1, 41 A 42, P1 S (22, Y (1, P pp. -, "g
# Pj ~ c} such that for the layer output ... Zn we have (zi)((0) = (zr)s = - for all j + c(x)) and 1 S t S n..
t - Vb and
Proof. We will show how to construct the layers for each formula individually. For all layers we set hg = O. When defining an FNN which only affects single dimension in the input, we always assume that all other inputs remain unchanged.
Case 1: -I. Notice that in order to evaluate the negation, we do not need to transfer any informa- tion from previous positions via the gate. The formula can evaluated statically at each position using the increment function. We define
A = 0 and B I C(((P))) ((((-11)=)(9)))
After computation of the linear recurrence defined in Eq. 1 we get sequence h1 ... hn with (he)at = 1- (dr))(())) As this already satisfies the claim, we can set the non-linear activation á of this layer be the identity ((x, h) h.
Case 2: 1p A 422 Let
= 0 and B = 1 + (((()))))))d)))) + (((( (((()))2))-(1))
After computation of the linear recurrence as defined in Eq. 1 we get sequence h1 ... hn with (he) Appa) (z)))(())> + (æ)))((2)) - {-1,0, 13. The non-linear layer output now maps this sequence 21 ... Zn. such that (Z))((p)))2)) ((a(())))))) This yields the wanted property.
Case 3: PyI In this case we need positions at which fi is satisfied at, to the current position.
gate in order transfer information about previous
A = (" and B = 1 + C (((()))))(())))
Notice that the gate is actually time-invariant and diagonal, as the transfer does not depend on the current input. The gate just propagates the previous value, hence
(he)(pe)) (hI-1) (x)))(()))
> (a))
Therefore, (h)-1)d(p holds the number of times P P1p1 was true at previous positions. The non- linear layer output & now maps this sequence 21 Zn, such that (21).(P)1) N (he)))))
Case 4: E; # 93 c. For more compact notation we denote the formula by tb. This case is basically an extension of the previously case. Instead of only testing if the number of positions at which a formula held is at least one, we compute a weighted sum on the number of occurences and compare it to a specific value.
A = ((1))))11)) and B = Σ aj (((())))0))))
As in the previous case this gate is also time-invariant and diagonal as only propagates the value of specific dimension independently of æt, We get
(he) = (he- ()(0)) +
Σ aj (o))((e))
aj (xi)
Σ aj
c (a)))ee))))
1=1
The non-linear layer output now maps this sequence to 2. Zn. such that (2))(()
N.w (hh)))()))
15

---

Published as a conference paper at ICLR 2026
Case 5: (9 S22. We use the temporal unfolding of the since- S P2. At closer look one can see that the unfolding has a similar structure as the linear recurrence in SSM layers. The current evaluation of (oi gets multiplied with the previous evaluation of y S y22 and additionally the evaluation of y22 is added in order to restart the recurrence in case of a new occurence of 422- We define
A = C((((1893) and B I + ((((11))))-1(9)))
This leads to (ht) = (Iz))((p))
We see that in this case the gate not ine-innariantt actually depends on the value of (Z)))()))) Obviously y2 S ip2 is satisfied at some position if (he))((11822) O. The non-linear layer output ø now maps this sequence to Z1. En. such that (zt)((p18pa) x1) ((e)) ((2)))
+ (222)))))) (((11)(()1802))
Case 6: y We use the encoding trick from Lemma 11. Let
A c((8))))))))) and B c((lre)))s()))
We get (1)) = (h: + (#)))((e)) Let Nprew be the FNN defined in Lemma 11. The non-linear layer output & now maps this sequence to 21 En. such that (z)) = (hew((())((rr))))) This recovers the previous value y from position t I and yields the wanted property.
We are now ready to prove Theorem 10. The proof shows that we do not need a single layer for each subformula of y., but is possible to evaluate all subformulas of the same nesting-depth simultaneously. We therefore need decomposition of every pLTL, formula, by its nesting-depth.
Proof of Thm. 10. Let y be a ,LTL, decomposition. We show the claim via an induction over the sequential decomposition and nesting depth k of yp
[1 formula with nd(pp) and Mo. My be its sequential
Case k 0: Mo contains only atomic formulas. Let emb Σ - Rd with emb(a) = 2; with (z.)a(1) = 1 and (z)
if p E a and otherwise for all p P. All other dimensions are set to zero. Let a E" be some word and #y ...... Lx, emb(o), then obviously (are).(p) o,t F p for all p E P and < t < |o).
Case k > 0: Using the induction hypothesis we assume that the claim holds for all formulas in MA-1. Hence, we can apply Lemma 12 to each v E MR. Let (Ag. B the gate and ine tuples gained from Lemma 12 for each vi E Mr- We now define layer 4 with A = EvEM, Ay and B = EvEN, By. Recall that Lemma 12 shows that each Ag and Bg. only affects the dimension of w. leaving all other dimensions unchanged. This enables us to simply accumulate the effect of all gates and inc, resulting the non-lineat outputs. We argued that for each v. the layer output dg only affects the dimension of vh. Hence, we can compose all FNN without affecting the wanted output. Therefore, let = OvEM, 6s, where O denotes the repeated composition of FNNs. Using these arguments together with Lemma 12 we get that for every word E Σ", the output 2 ... -/1,/ of S.p after layer L, has the property (z))a(0)
layer which simultaneously evaluates all & MM.. The same holds for
= w. t - 2b for all vb E Mn and 1 < t < |o].
Proof of Thm. 1. Let = =1 after the last layer of S.p as constructed in Theorem 10. We have (z))uw)) = + w, = zù for all
Σ' be word and 21 ... 2n be the vector sequence produced
v E Sub(y) and S S n. Therefore, a L(y) = o,n F = (zn)(()) = 1. We define the final output FNN of Spp such that ye = (=)((z)))))) We get I(g) O So = O
It is important to note that the expressiveness of SSM evaluating PLTL # formulas with counting subformulas depends crucially on the arithmetic model used for computation. When operating over fixed-width arithmetic with a constant number of bits, SSM can only evaluate counting subformulas
Σj=1 aj- # P0 ~ c in which all coefficients a, are positive (i.e., formulas in pLTL,[#]* {)). This re- striction arises because the accumulation can only increase when coefficients are solely positive, and
16

---

Published as a conference paper at ICLR 2026
the comparison against the threshold cremains stable under A decision procedure simply needs to determine whether the accumulated sum exceeds, equals, or falls below the constant c, which can be achieved with fixed precision. In contrast, when the arith- metic precision grows logarithmically with the input length, SSM can evaluate general counting formulas in PLTL, [ including those with negative coefficients aj. This is the case because logarithmic precision provides enough bits to exactly count occurrences of subformulas in words of length maintaining the precise difference between positive and negative terms. For instance, b) A (# a # = 0) re- quires tracking the exact difference between occurrences of a and b, which necessitates unbounded precision as n grows, since any fixed-precision arithmetic would eventually lead to overflow or rounding errors when processing sufficiently long inputs.
approximations.
recognising the language fa"b" n 2 0} expressed by formula H(a + -Y
A.3 PROOFS OF SECTION 5
For time-invariant SSM, the gate of each layer is a constant matrix, independent of the input. For the construction carried out here we assume, as in the previous section, that the increment function is simply computed by linear projection. This means we can represent the recurrence of time- invariant SSM layer as
h Ah + Bx:
For easier construction show that effectively only need to maintain single counter, when several modular predicates occur in a formula.
Lemma 13. For every yp E UN-PLTL ## MOD] using modular predicates with divisors di.... dx there is formula v' E UN-PLTL MOD]. which only uses modular predicates with the same divisor d'.
Proof. Take the least common multiple d' = lcm(d1, .. predicate MOD by MODE" MOD r+d, V MOD V....
,. ,d)). Then construct sp' by replacing each
We will now show that every language recognised by a UN-PLTL, MOD] formula can also be recognised by a time-invariant SSM. We will show this by extending the proof of Theorem 10. Let E UN-PLTL, # MOD] be formula over modular predicates all having single divisor m. The resulting SSM will have
dimensions. We refine the function PU MMOD Th 0 < < m) U Sub({p) (p) U (1) + {1, d} which has the same properties as in Section The only difference that we have additional dimensions for every possible modular predicate MOD,". For simplicity, memory, with (MOD,")) = ((MOD"' + for all 0 S < m, forming a contiguous interval of indices. We are then ready prove that time-invariant SSM can recognise all languages definable in UN-PLTL, MOD).
[PI + |p) + m
a function
ensure that the indices of modular predicates are adjacent in
Theorem 14. Let yp be a UN-PLTL, # MOD] MMD) formula over P. using only modular predicates with divisor m. There an SSM Sip over the alphabet = 2 with dimension = | + m + |4p| + and nd((p) + layers, such that for all words E Σ* with |o| after the last layer on input o, then (yt))ty) = 1 if and only if w. t - ?) and otherwise 0, for all 1 st t S n and 1) E Sub(yp).
If y1 Yn the oulput of S
The proof follows the exact same lines as Theorem 10. The only difference that we need an additional layer right after the embbedding in order to evaluate the modular predicates. Let E and 2; ... Fr be the vector sequence following the embedding. We add an additional layer hoDD as described in Lemma 6. For this layer, we extend the permutation matrix P from Lemma to the full dimension d by embedding in a larger matrix. Specifically, we construct a matrix where the cyclic permutation P is applied only to the dimensions ((MOD?") for 0 < m, which form a contiguous block of indices as established earlier. All other entries are set to zero. Let A be this matrix. We set the increment B to be the matrix which looks like the identity matrix, but with zeros on the diagonal for all dimensions (MOD)") for 0 < r < m. Therefore we get (h+) (he) < = (mod d) and (h+); (æ:);; for all other dimensions i. Therefore, all
Proof.
17

---

Published as a conference paper at ICLR 2026
atomic formulas evaluated after the first layer. The remaining layers defined as in Theorem 10.
Theorem now follows directly from the previous theorem.
It is important to note that the considerations regarding fixed-width arithmetic for time-invariant SSM mirror those discussed for diagonal SSM in Appendix A.2. When operating over -xxdhwidth arithmetic with a constant number of bits, time-invarian SSM can only reliably evaluate counting
subformulas with positive coefficients (i.e., formulas in UN-PLTL, only increases and comparisons against thresholds remain stable under bounded- bounded-precision approxi- mations. The ability to evaluate formulas with negative coefficients requires arithmetic precision that grows logarithmically with input length. The addition of modular predicates does not affect this fun- damental limitation, as the modular counter component operates independently from the counting mechanisms. Thus, when restricted to fixed-width arithmetic, the expressiveness of time-invariant SSM seems to remain limited to UN-PLTL, MMDD), which corresponds to a fragment of FO |<, MOD].
MOD]+), as the accumulation
A.4 PROOFS OF SECTION 6
C-RASP was first introduced by Yang & Chiang (2024) as logic called K2 The syntax of C-RASP is very similar to (N-PLTL,[#] with the only difference being that C-RASP has
yesterday and no previously operator. The only temporal operator is the # operator in counting formulas.
We show that C-RASP is strictly less expressive than UN-PLTL, [# The proof is based on the fact that while C-RASP can simulate the previoushy-operator, it cannot simulate yesterday.
Lemma 15. C-RASP UN-PLTL, #1 without the yesterday-operator
Proof. The inclusion of C-RASP in UN-PLTI., is trivial, as all operators of C-RASP are also in UN-PLTL, [#]. For the other direction, let be a UN-PLTL, [#] formula without the yesterday- operator. We only need replace all previously subformulas y by the counting formula $4 1. This yields a C-RASP formula which obviously equivalent to
To see that C-RASP is strictly less expressive than UN-PLTL f # consider the language {w {a, b)* contains aa). which is definable by the UN-PLTL #1 formula P(a A Y Ya), but as noticed by Yang & Chiang (2024) cannot be defined in C-RASP.
18


Reviews:
[{"review_id": "HncarDEzy0", "reviewer": "Reviewer_FusE", "summary": "The paper investigates the expressive power of State Space Models (SSMs) in recognizing formal languages through Propositional Linear Temporal Logic (PLTL).\nDiagonal SSM (with fixed-precision) can recognize PLTL_f, which is equivalent to star-free regular languages (FO[<]), but they cannot\nrecognize non-star-free languages like (aa)*.\nDiagonal SSM with log-precision can use a backward counting operator, so they can handle UN-PLTL_f.\nTime-Invariant SSM (fixed-precision) can recognize UN-PLTL_f[MOD] by using cyclic permutation matrices to maintain modulo counters and so they can recognize languages like (aa)* which are not star-free.\nTime-Invariant with log-precision also handle backward counting.\n\nMixed SSM\n   - Fixed-precision: Recognize all regular languages in AC0 (which is PLTL_f[MOD]).\n   - Log-precision: Recognize PLTL_f.\n\nComparison to Transformers: \n- Diagonal fixed-precision SSMs are comparable to UHAT without positional encodings (FO[<]). \n- Time-invariant fixed-precision SSMs are similar to UHAT with positional encodings (FO[<,MOD]).\n- Mixed log-precision SSM align with AHAT in expressiveness.", "questions": "Could you provide preliminary experiments demonstrating mixed SSM’s ability/failure on synthetic languages under finite precision? If not, is such validation planned for the final version?", "limitations": "", "rating": 8, "confidence": 2, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "- The proofs builds on top of the  temporal logic theory and circuit complexity (AC⁰/TC⁰) using established formal frameworks from transformer expressiveness research.  \n- Bounds are tight: Diagonal SSMs’ impossibility to recognize `(aa)*` is proven via star-free language separation.  \n- Gate constructions are explicit and computable.  \n- Language recognition capabilities are formally verified, not empirically approximated.  \n- Limitations (e.g., TC⁹ upper bound not yet reduced to AC⁰ for SSMs) are presented.", "weaknesses": "- Empirical validation of depth hierarchies suggested but not explored.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "YQvufTmrVK", "reviewer": "Reviewer_hFRJ", "summary": "The paper studies variants of state space models (SSMs) from a theoretical perspective and seeks to establish lower bounds on their expressivity. It builds upon prior work that provided upper bounds via circuit complexity. It uses fragments and extensions of (pure-past) linear temporal logic on finite traces (pLTLf) to capture the lower bounds.\n\nThe paper begins by presenting a formal model of SSMs and the lower bounds on the expressivity are established through the explicit construction of SSM layers that encode different logical operators. The two types of SSMs considered are SSMs with diagonal and time-invariant gates. Their results establish that SSMs with diagonal gates can capture pLTLf and the time-invariant version can capture the unary operator fragment un-pLTLf, along with modular counting. Additionally, log-precision arithmetic that scales precision logarithmically with input length can allow the models to perform counting.", "questions": "Please comment on the weaknesses mentioned above.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "The work builds upon an established literature that studies the limits of expressivity of different ML architectures from a theoretical lens. The paper studies the full breadth of different SSM variants and a clear expressivity hierarchy is established. Counterexamples have also been provided where possible to show that the lower bounds are \"tight\" at least from the temporal logic perspective.", "weaknesses": "The primary weakness is that these results do not suggest any ways to improve ML techniques and are far removed from practice.\n\nThere is a lot of room for improving the presentation. The abstract conveys the main message well but the introduction is severely lacking in details and a reader unfamiliar with formal logic/complexity theory would find it hard to comprehend. Many aspects are not provided with an explanation. For example, the introduction never discusses what it means to recognize a language or what LTL fundamentally is because the general ML community would not be familiar with temporal logics or formal languages. The presentation would be greatly improved with an extended introduction that puts more effort in explaining the results intuitively. This is challenging considering the amount of formalisms required but it is necessary.\n\nComments about notation:\n- There are a few times when a layer is referred to by an $\\ell$ instead of $l$.\n- FNN abbreviation is used in line 84 before the expanded form is mentioned.\n- The operators tt, ff, and H would be obvious to a person familiar with formal logic but not to everyone. They need to be provided with an intuitive explanation.\n- ex. is used instead of $\\exists$ or just exists which is non-standard.\n- First-order logic is used but never defined.\n- Circuit complexity classes are also used several times but never mentioned what they mean.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "R8J0tqDPdg", "reviewer": "Reviewer_M8MD", "summary": "The paper investigates the expressive power of state space models (SSMs), an alternative to transformers, exploiting formal methods. Various fragments and extensions of Linear Temporal Logic (LTL) over finite traces (LTL$_f$) are used to proxy the SSM expressiveness. It investigates two aspects: the SSM gating mechanism (diagonal, depending on the input, vs time-invariant, remaining constant) and the arithmetic precision (fixed-width vs log-precision). Each setting combination recognizes different languages (e.g., SSM with time-invariant gates recognizes the past fragment of LTL$_f$ with unary past operators and the MOD operator with fixed-precision, while it recognizes the extended version of the same language with a past-counting operator with log-precision). All the results are formally proved, and I appreciate this a lot. The paper also positions and discusses its results with respect to relevant transformer architectures, adding value to the overall contribution. The paper is excellent and presents its results very clearly. I will recommend acceptance.", "questions": "(Q1) Can you please add an additional figure to improve the accessibility to readers to navigate the results? \n\n(Q2) I would use different aesthetics for Figures 1, 2, and 3. For example, the \"dashed\" versus \"non-dashed\" inclusions could have symbols on the edges (e.g., $\\subset$). Also, Figure 1 uses $\\ge$, while Figures 2 and 3 use $\\subseteq$; indeed, Figure 1 says \"SSM with diagonal gates $\\ge$ pLTL$_f$ with past-counting operator ($\\log$-precision) (Thm. 4)\", while Figure 2 says \"pLTL$_f$ with past-counting operator $\\subseteq$ diagonal SSM (Thm. 4)\". The captions could be improved as well. These inconsistencies detract from the overall readability. Can you please improve all these aspects?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "(S1) The paper is exquisite with a clean presentation. The mathematics is there, and the authors know what they are doing. \n\n(S2) The paper's expressiveness study is impactful as it sets new grounds for what SSMs can express or not.\n\n(S3) The work bridges the gap between symbolic and neural AI. For me, this kind of investigation allows us to see temporal, formal logic through a new lens. \n\n(S4) Conjecture 1 makes sense. I don't have a formal argument, but I think the provided argument is sound.\n\n(S5) Even if the study addresses only SSMs, the contextualization of the results with respect to other transformer architectures adds value. It closes the circle elegantly.", "weaknesses": "(W1) I really enjoyed the mathematical framework and arguments (with all the proofs), but I think the paper could benefit from an additional figure showcasing how such results are related (e.g., which Lemma(s) lead to which Theorem(s)). I expect this to improve the navigation of the paper's results.\n\n(W2) The layout/presentation of Figures 1, 2, and 3 should be standardized. These figures could benefit from a more descriptive caption. \n\n(W3) Some minor inconsistencies that I've identified:\n\n- line 84: FNN is not defined (it is, however, defined at line 104)\n- lines 148--156: pLTL$_f$ with both past- and future-counting operators seems counterintuitive. Since \"p\" stands for past, I would have presented it differently; for example, \"LTL$_f$ with both past- and future-counting operators extends LTL$_f$ $\\ldots$\" and then (at line 157) I would have said that \"By pLTL$_f$ with past-counting operator we denote the logic in which every counting subformula has $b_j = 0$ for all $j$, a fragment of LTL$_f$ with both past- and future-counting operators.\" Moreover, I would rather use $\\sigma$ instead of $w$ to denote the words (as in the semantics at lines 134--140).\n- line 252: missing closing period\n- line 353: $\\ell$ should be $l$ (see line 350)\n- line 631: since $N_1 : \\mathbb R^{m_1} \\to \\mathbb R^{n_1}$ and  $N_2 : \\mathbb R^{m_2} \\to \\mathbb R^{n_2}$, then $N_1 \\circ N_2 : \\mathbb R^{m_2} \\to \\mathbb R^{n_1}$ if $n_2 = m_1$; thus, $\\mathbb R^{m_1} \\to \\mathbb R^{n-2}$ is wrong. In any case, I would rather use $N_2 \\circ N_1 : \\mathbb R^{m_1} \\to \\mathbb R^{n_2}$ with $n_1 = m_2$; it is just simpler to read.\n- lines 635 & 638: $\\text{diag}(A \\mathbf x_t)$ vs $(A \\mathbf x_t)$\n- line 707: it should be $\\varphi_1 S \\varphi_2$ instead of $\\varphi S \\varphi_2$ \n- Proofs of Lemma 12 & Theorem 10: for the cases, please use either bold or emphasize, but not both.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "InWnGYHXYm", "reviewer": "Reviewer_FYk9", "summary": "This paper presents a theoretical analysis of the expressive power of State Space Models (SSMs), establishing a formal hierarchy of their capabilities based on gating mechanisms (diagonal vs. time-invariant) and arithmetic precision (fixed vs. logarithmic). The core contribution is a set of lower bounds linking different SSM variants to specific fragments of temporal logic (PLTLf and its extensions), thereby characterizing which classes of formal languages each variant can recognize.\n\nThe work is purely theoretical, focusing on abstract computational expressiveness rather than practical performance or model design. It provides no empirical validation, engineering insights, or direct applications to real-world tasks. The motivation stems from a foundational interest in comparing SSMs to transformers within a formal logic framework, continuing a line of theoretical research in deep learning. While it clarifies the theoretical landscape, the paper's findings have no immediate or clear practical application for practitioners designing or training SSMs.", "questions": "The paper introduces several extensions of PLTLf (e.g., PLTLf[#↓], PLTLf[MOD]) without a clear, upfront motivation. Could the authors explicitly justify why these specific logical fragments are the most relevant or natural for analyzing SSMs? For instance, what is the intrinsic property of SSMs that makes the pure-past, backward-looking counting operator #↓ a better fit than a future-looking one?\n\nSeveral key symbols are used before being defined or are used inconsistently (e.g., Σ at line 84, P at line 132, w at line 184, H φ). For a paper aiming for precision, this hinders readability. Could the authors add a \"Preliminaries\" section or a notation table to ensure every symbol is formally defined upon first use?\n\nThe paper states that its results \"subsume\" the lower bounds of Sarrof et al. (2024). Could the authors provide a more detailed discussion, perhaps with a concrete example, of exactly what new expressiveness their construction captures that the prior work did not?\n\nThe constructive proofs show that an SSM exists which can recognize a given language. However, it relies on hand-crafted, precise weights. What is the authors' intuition or any theoretical insight on whether such configurations can be discovered via gradient-based learning, or are they likely to be in regions of the parameter space that are hard to reach?\n\nThe constructions, especially for fixed-precision arithmetic, seem to depend on exact numerical values to avoid state collisions. How robust are these constructions to the inevitable noise and approximation errors that occur during stochastic training? Would a small perturbation to the gate weights cause the SSM to fail on the languages it is supposed to recognize?\n\nThe entire analysis is framed around formal language recognition. How do the authors envision these theoretical results informing the design of SSMs for core practical tasks like next-token prediction (a function computation problem) or sequence-to-sequence translation? For example, does the inability of a fixed-precision diagonal SSM to recognize (aa)* imply a fundamental limitation on its ability to model certain syntactic or semantic structures in natural language?\n\nThe paper maps SSMs to a known hierarchy of circuit complexity and logic. However, for a practitioner, the key question is: \"Which SSM variant should I use for my problem?\" Could the authors speculate on what their expressiveness hierarchy implies for real-world performance? For instance, does the ability to express modular predicates (like in time-invariant SSMs) suggest an advantage for tasks requiring periodicity or hierarchical structure?\n\nWhile a purely theoretical paper need not include large-scale experiments, could the authors propose a minimal, synthetic experiment that could falsify or corroborate their theoretical predictions? For example, training different SSM variants on a synthetic dataset for (aa)* or $a^n b^n$ and observing if the results align with the theoretical capabilities (e.g., diagonal SSMs failing to learn (aa)*).\n\nThe heavy reliance on temporal logic and circuit complexity can limit the paper's impact. Have the authors considered adding a more extensive, intuitive overview in the introduction that explains the \"story\" and the practical implications of the different logic fragments (e.g., \"PLTLf corresponds to pattern X, while adding counting allows for pattern Y\") before diving into the formal details? A summary figure comparing the practical capabilities (e.g., \"can detect repeated patterns,\" \"can count events\") of each SSM variant would be immensely helpful.\n\nThe sentence “We use this restriction, because in contrast to transformers, where the attention mechanism is usually able to attend to all positions, SSM can only see information from previous positions.” at lines 157-159 is unclear. Please clarify its meaning and why this sentence is important; similarly, for the other sentence at lines 166-167, whose role in the paper is not known.", "limitations": "", "rating": 2, "confidence": 2, "soundness": 2, "presentation": 1, "contribution": 2, "strengths": "The paper's primary strength is its “systematic” and “rigorous” approach. It aims to establish “precise”, “formal” connections between SSM variants and both well-understood and less well-known fragments of temporal logic (PLTLf), not adequately justified.\n\nThe work establishes a hierarchy of expressiveness. It differentiates the capabilities of diagonal-gated, time-invariant, and mixed SSMs, and further shows the critical impact of arithmetic precision (fixed vs. logarithmic). \n\nIt provides constructive proof sketches (proofs are in the appendix) showing how to translate a temporal logic formula into a corresponding SSM architecture. This offers some insight into the mechanisms (e.g., gates, recurrence) that enable specific computational behaviors.\n\nThe paper provides a formal comparison between the two competing architectural paradigms. It shows how the recurrent, state-based nature of SSMs leads to a different expressive profile compared to the attention-based transformers.", "weaknesses": "This is a purely theoretical work, and as such it expected to be rigorous. However, many terms are not explained (e.g. $\\Sigma$ at line 84, $\\mathcal{P}$ at line 132, $H \\varphi$, $w$ at line 184). Not clear why the different logics where introduced, they appear out of the blue and it is not clear their practical importance. Why the considered extensions of pLTLf have been introduced?\n\nIts most significant weakness from a practical standpoint is the absence of any empirical evidence. The results are \"in vitro\" – they show what is possible in a formal model, but not what is practically efficient, learnable, or scalable with gradient descent on real data.\n\nThe analysis is decoupled from the practical motivations that drive SSM development (e.g., training speed, long-context handling, inference efficiency). It remains unclear how these theoretical expressiveness limits correlate with the models' performance on real-world tasks like language modeling or reasoning. A practitioner would not know if reaching for a more expressive (theoretically) SSM variant would yield any tangible benefits.\n\nThe paper focuses exclusively on language recognition, a very specific and limited task. It does not address the expressive power of SSMs for sequence-to-sequence tasks, generation, or their ability to compute functions over sequences, which are more relevant to their practical use.\n\nThe constructions rely on idealized components, such as hand-crafted weight matrices and specific non-linear functions. It does not address whether these precise configurations can be discovered through standard training procedures or if they are stable under stochastic gradient descent.\n\nThe heavy reliance on formal logic, circuit complexity, and automata theory makes the work largely inaccessible to a broad machine learning audience, limiting its immediate impact outside a specialized theoretical community.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)