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 ?
