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$

example 1

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:

example 3

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.

  • 1
    $\begingroup$ 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. $\endgroup$
    – DCTLib
    Commented Jun 2, 2023 at 13:33
  • $\begingroup$ Please ask only one question per post. If you have multiple questions, you can ask them separately. $\endgroup$
    – D.W.
    Commented Jun 3, 2023 at 20:56
  • $\begingroup$ 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. $\endgroup$
    – D.W.
    Commented Jun 3, 2023 at 20:56


Your Answer

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