Remix.run Logo
yorwba 7 hours ago

Proposition 16. UHATs have polynomially bounded expansion over LTL. In particular, given an LTL formula φ, one can construct in polynomial time a UHAT T such that L(T) = L(φ).

i.e. the blowup is only exponential in one direction.

measurablefunc 6 hours ago | parent [-]

That says every LTL formula can be compiled into UHAT w/ polynomial overhead. It doesn't say that all languages recognizable w/ UHATs necessarily do not have succinct recgonizers in LTLs or RNNs.

Edit: Actually nevermind. If UHAT could be compiled into LTL w/ polynomial overhead then that would also work for the languages that have exponential overhead in LTL but since they don't there is a strict separation.