Return to Answer

I think it is PSpace-complete, here is a proof scheme.

We can go back to the proof scheme for PSpace-completeness of regular expression universality, e.g. described in this answer.

There we can see that the reduction uses a disjunction of expressions $e_0, e_1,e_2,\dots,e_k$, where most expressions $e_i$ are of the form $\Sigma^* f_i \Sigma^*$, where $f_i$ describes a fixed-sized infix, that is a forbidden pattern in a run of the PSpace machine $M$. The exceptions to this are the expressions stating that the prefix does not describe an initial configuration, and about the suffix not describing a final configuration, assume these are $e_0$ and $e_k$.

Let us take $L=f_1+f_2+\dots+f_{k-1}$, and $K$ the language stating that the word starts with an initial configuration and ends with a final one.

We have $K\subseteq \Sigma^*L\Sigma^*$ if and only if the PSpace machine $M$ does not halt. Indeed this inclusion expresses the fact that any word describing a run that starts with an initial configuration and ends with a final one must "cheat" somewhere.

The only thing that remains to be carefully verified is that the monoids of $L$ and $K$ are of polynomial size, but it seems to be the case.

Notice that for some expressions, you can either put them in $L$ or put their complement in $K$, for instance the constraint that in any run you must have exactly one state between any two $\$$. It can either be formulated as a polynomial forbidden pattern everywhere (for $L$), or by a language that you can describe with a small monoid (for $K$).

Bottomline, the intuition is that the main source of nondeterminism that causes the PSpace-hardness of regular expression universality, is the one encoded by expressions of the form $\Sigma^*f\Sigma^*$, i.e. the ability to search for a pattern anywhere in the word.

Added from the comments: more precisions on why we can obtain a polynomial-sized monoid for $L$:

The typical job of the syntactic monoid of $L$ will be to recognize a union of languages of the form $p_1\Sigma^*p_2$, where $p_1$ and $p_2$ are small patterns (say of $3$ letters). It is doable with a polynomial size monoid, which just remembers the length of the word and the $3$-letter words on the sides.

You could even restrict even more the variation in $L$, by choosing for $M$ a universal Turing machine $M_u$ (with polynomial simulation overhead). This way, the number of forbidden local patterns will be a constant, as it will only depend on the transition table of $M_u$, and the only variation in $L$ will be the length $n$ of configurations. The arbitrary PSpace problem will be fully encoded in the initial configuration of the tape, itself encoded in $K$.

I think it is PSpace-complete, here is a proof scheme.

We can go back to the proof scheme for PSpace-completeness of regular expression universality, e.g. described in this answer.

There we can see that the reduction uses a disjunction of expressions $e_0, e_1,e_2,\dots,e_k$, where most expressions $e_i$ are of the form $\Sigma^* f_i \Sigma^*$, where $f_i$ describes a fixed-sized infix, that is a forbidden pattern in a run of the PSpace machine $M$. The exceptions to this are the expressions stating that the prefix does not describe an initial configuration, and about the suffix not describing a final configuration, assume these are $e_0$ and $e_k$.

Let us take $L=f_1+f_2+\dots+f_{k-1}$, and $K$ the language stating that the word starts with an initial configuration and ends with a final one.

We have $K\subseteq \Sigma^*L\Sigma^*$ if and only if the PSpace machine $M$ does not halt. Indeed this inclusion expresses the fact that any word describing a run that starts with an initial configuration and ends with a final one must "cheat" somewhere.

The only thing that remains to be carefully verified is that the monoids of $L$ and $K$ are of polynomial size, but it seems to be the case.

Notice that for some expressions, you can either put them in $L$ or put their complement in $K$, for instance the constraint that in any run you must have exactly one state between any two $\$$. It can either be formulated as a polynomial forbidden pattern everywhere (for $L$), or by a language that you can describe with a small monoid (for $K$).

Bottomline, the intuition is that the main source of nondeterminism that causes the PSpace-hardness of regular expression universality, is the one encoded by expressions of the form $\Sigma^*f\Sigma^*$, i.e. the ability to search for a pattern anywhere in the word.

Added from the comments: more precisions on why we can obtain a polynomial-sized monoid for $L$:

The typical job of the syntactic monoid of $L$ will be to recognize a union of languages of the form $p_1\Sigma^*p_2$, where $p_1$ and $p_2$ are small patterns (say of $3$ letters). It is doable with a polynomial size monoid, which just remembers the length of the word and the $3$-letter words on the sides.

You could restrict a lot of the variation in $L$, by choosing for $M$ a universal Turing machine $M_u$ (with polynomial simulation overhead). This way, the number of forbidden local patterns will be a constant, as it will only depend on the transition table of $M_u$, and the only variation in $L$ will be the length $n$ of configurations. The arbitrary PSpace problem will be fully encoded in the initial configuration of the tape, itself encoded in $K$.

I think it is PSpace-complete, here is a proof scheme.

We can go back to the proof scheme for PSpace-completeness of regular expression universality, e.g. described in this answer.

There we can see that the reduction uses a disjunction of expressions $e_0, e_1,e_2,\dots,e_k$, where most expressions $e_i$ are of the form $\Sigma^* f_i \Sigma^*$, where $f_i$ describes a fixed-sized infix, that is a forbidden pattern in a run of the PSpace machine $M$. The exceptions to this are the expressions stating that the prefix does not describe an initial configuration, and about the suffix not describing a final configuration, assume these are $e_0$ and $e_k$.

Let us take $L=f_1+f_2+\dots+f_{k-1}$, and $K$ the language stating that the word starts with an initial configuration and ends with a final one.

We have $K\subseteq \Sigma^*L\Sigma^*$ if and only if the PSpace machine $M$ does not halt. Indeed this inclusion expresses the fact that any word describing a run that starts with an initial configuration and ends with a final one must "cheat" somewhere.

The only thing that remains to be carefully verified is that the monoids of $L$ and $K$ are of polynomial size, but it seems to be the case.

Notice that for some expressions, you can either put them in $L$ or put their complement in $K$, for instance the constraint that in any run you must have exactly one state between any two $\$$. It can either be formulated as a polynomial forbidden pattern everywhere (for $L$), or by a language that you can describe with a small monoid (for $K$).

Bottomline, the intuition is that the main source of nondeterminism that causes the PSpace-hardness of regular expression universality, is the one encoded by expressions of the form $\Sigma^*f\Sigma^*$, i.e. the ability to search for a pattern anywhere in the word.

I think it is PSpace-complete, here is a proof scheme.

We can go back to the proof scheme for PSpace-completeness of regular expression universality, e.g. described in this answer.

There we can see that the reduction uses a disjunction of expressions $e_0, e_1,e_2,\dots,e_k$, where most expressions $e_i$ are of the form $\Sigma^* f_i \Sigma^*$, where $f_i$ describes a fixed-sized infix, that is a forbidden pattern in a run of the PSpace machine $M$. The exceptions to this are the expressions stating that the prefix does not describe an initial configuration, and about the suffix not describing a final configuration, assume these are $e_0$ and $e_k$.

Let us take $L=f_1+f_2+\dots+f_{k-1}$, and $K$ the language stating that the word starts with an initial configuration and ends with a final one.

We have $K\subseteq \Sigma^*L\Sigma^*$ if and only if the PSpace machine $M$ does not halt. Indeed this inclusion expresses the fact that any word describing a run that starts with an initial configuration and ends with a final one must "cheat" somewhere.

The only thing that remains to be carefully verified is that the monoids of $L$ and $K$ are of polynomial size, but it seems to be the case.

Notice that for some expressions, you can either put them in $L$ or put their complement in $K$, for instance the constraint that in any run you must have exactly one state between any two $\$$. It can either be formulated as a polynomial forbidden pattern everywhere (for $L$), or by a language that you can describe with a small monoid (for $K$).

Bottomline, the intuition is that the main source of nondeterminism that causes the PSpace-hardness of regular expression universality, is the one encoded by expressions of the form $\Sigma^*f\Sigma^*$, i.e. the ability to search for a pattern anywhere in the word.

Added from the comments: more precisions on why we can obtain a polynomial-sized monoid for $L$:

The typical job of the syntactic monoid of $L$ will be to recognize a union of languages of the form $p_1\Sigma^*p_2$, where $p_1$ and $p_2$ are small patterns (say of $3$ letters). It is doable with a polynomial size monoid, which just remembers the length of the word and the $3$-letter words on the sides.

You could even restrict even more the variation in $L$, by choosing for $M$ a universal Turing machine $M_u$ (with polynomial simulation overhead). This way, the number of forbidden local patterns will be a constant, as it will only depend on the transition table of $M_u$, and the only variation in $L$ will be the length $n$ of configurations. The arbitrary PSpace problem will be fully encoded in the initial configuration of the tape, itself encoded in $K$.

I think it is PSpace-complete, here is a proof scheme.

We can go back to the proof scheme for PSpace-completeness of regular expression universality, e.g. described in this answer.

There we can see that the reduction uses a disjunction of expressions $e_0, e_1,e_2,\dots,e_k$, where most expressions $e_i$ are of the form $\Sigma^* f_i \Sigma^*$, where $f_i$ describes a fixed-sized infix, that is a forbidden pattern in a run of the PSpace machine $M$. The exceptions to this are the expressions stating that the prefix does not describe an initial configuration, and about the suffix not describing a final configuration, assume these are $e_0$ and $e_k$.

Let us take $L=f_1+f_2+\dots+f_{k-1}$, and $K$ the language stating that the word starts with an initial configuration and ends with a final one.

We have $K\subseteq \Sigma^*L\Sigma^*$ if and only if the PSpace machine $M$ does not halt. Indeed this inclusion expresses the fact that any word describing a run that starts with an initial configuration and ends with a final one must "cheat" somewhere.

The only thing that remains to be carefully verified is that the monoids of $L$ and $K$ are of polynomial size, but it seems to be the case.

Notice that for some expressions, you can either put them in $L$ or put their complement in $K$, for instance the constraint that in any run you must have exactly one state between any two $\$$. It can either be formulated as a polynomial forbidden pattern everywhere (for $L$), or by a language that you can describe with a small monoid (for $K$).

Bottomline, the intuition is that the main source of nondeterminism that causes the PSpace-hardness of regular expression universality, is the one encoded by expressions of the form $\Sigma^*f\Sigma^*$, i.e. the ability to search for a pattern anywhere in the word.

As a bonus, this proof scheme allows to see that one-sided versions of your problem, where the other side is a well-chosen constant language, are still PSPACE-complete.

First, we can always assume that the PSpace TM $M$ starts and ends with empty configuration, so we can assume that $K$ is always the same. Thus, there is a fixed $K$ such that the inevitability problem is PSpace-complete, with $M_L$ as only input.

On the other hand, if we consider that $M$ is a universal machine $M_u$ with polynomial overhead for the simulation, then any PSpace problem can be encoded in the input configuration. Thus, $L$ will be a fixed language, asserting that there is a violation of the transition table of $M_u$. We obtain a fixed language $L$ such that the inevitability problem with only input $K$, asking whether $K\subseteq \Sigma^*L\Sigma^*$, is PSpace-complete.

Notice that if it turns out that the monoid $M_L$ is in general exponential in the size of the machine $M$, this last version fixes the problem, as $M_L$ becomes a constant.

I think it is PSpace-complete, here is a proof scheme.

We can go back to the proof scheme for PSpace-completeness of regular expression universality, e.g. described in this answer.

There we can see that the reduction uses a disjunction of expressions $e_0, e_1,e_2,\dots,e_k$, where most expressions $e_i$ are of the form $\Sigma^* f_i \Sigma^*$, where $f_i$ describes a fixed-sized infix, that is a forbidden pattern in a run of the PSpace machine $M$. The exceptions to this are the expressions stating that the prefix does not describe an initial configuration, and about the suffix not describing a final configuration, assume these are $e_0$ and $e_k$.

Let us take $L=f_1+f_2+\dots+f_{k-1}$, and $K$ the language stating that the word starts with an initial configuration and ends with a final one.

We have $K\subseteq \Sigma^*L\Sigma^*$ if and only if the PSpace machine $M$ does not halt. Indeed this inclusion expresses the fact that any word describing a run that starts with an initial configuration and ends with a final one must "cheat" somewhere.

The only thing that remains to be carefully verified is that the monoids of $L$ and $K$ are of polynomial size, but it seems to be the case.

Notice that for some expressions, you can either put them in $L$ or put their complement in $K$, for instance the constraint that in any run you must have exactly one state between any two $\$$. It can either be formulated as a polynomial forbidden pattern everywhere (for $L$), or by a language that you can describe with a small monoid (for $K$).

Bottomline, the intuition is that the main source of nondeterminism that causes the PSpace-hardness of regular expression universality, is the one encoded by expressions of the form $\Sigma^*f\Sigma^*$, i.e. the ability to search for a pattern anywhere in the word.