# Complexity of inclusion of transfinite expressions

Transfinite expressions on an alphabet $$\Sigma$$ are generated by the grammar :

$$e,f:= a\in\Sigma\mid e\cdot f\mid e+f\mid e^*\mid e^\omega.$$

They describe languages of transfinite words, i.e. words of ordinal length.

For instance the word $$(a^\omega b)^\omega$$ is in the language of the expression $$(a^\omega+b^*)^\omega$$.

After some searching I could not find results in the literature on the complexity of inclusion checking for such expressions. The closest I found is PSPACE-completeness for satisfiability of LTL formulas on transfinite words, here.

Is it known to be in PSPACE ?