Errors in examples of Vardi's paper "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces"

The paper Linear Temporal Logic and Linear Dynamic Logic on Finite Traces has the following examples on page 4:

Q1. (Update to Q1: solved. See the comment by DCTLib.) The first example says that the REf (reg-expr over fin words) $$\varphi^* \equiv$$$$\phi$$

I disagree: the LTLf formula ☐$$\phi$$ says that in every moment of the trace the formula $$\phi$$ holds while the REf $$\varphi^*$$ says there exists $$n$$ such that $$\varphi;\varphi;...\varphi$$ n times matches the whole word. Example: take the word $$abab$$ and $$\varphi = (a;b)$$, then $$abab \models (a;b)^*$$ whereas $$abab \not\models$$$$(a;b)$$. Agreed?

Q2. Another example:

Let me first note that the very first part $$true^*$$ already corresponds to ◇(...) and not to ☐, hence it cannot have the form ☐(...). Now, I assume the operator priorities are such that we have $$true^*;(\neg \psi + (true^*; \varphi))$$. This corresponds to ◇(Last ∧ (𝜓 → 𝜑)). So it is not what they claim. Agreed?

Many thanks.

• The first example seems to contain a typo by mixing "\varphi" and "\phi". Phi was a bit earlier defined to be a propositional formula, and then this example appears to be fine. Commented Jun 2, 2023 at 13:33
• Please ask only one question per post. If you have multiple questions, you can ask them separately.
– D.W.
Commented Jun 3, 2023 at 20:56
• Don't use images as main content of your post. This makes your question impossible to search and inaccessible to the visually impaired; we don't like that. Please transcribe text and mathematics. You can use LaTeX.
– D.W.
Commented Jun 3, 2023 at 20:56