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 ?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.