Some remarks on decidability

Our result on $\mathit{ILM_0}$ does not include a decidabilty result. Some attempts have been made though. The finite model property would be sufficient for the decidability. In order to keep the model finite one should re-use worlds as was done in the completeness proof of $\mathit{ILM}$. Attention should be payed at the invariants. They must be preserved! Probably it will be necessary to also label the S_x-transitions throughout the construction.