A Does this computation satisfy LTL formulas?

[alma359]

I have two LTL formulas.

The first one is (p U q) U r
The second one is p U (q U r)

I know the computation {r}ᵂ satisfies both formulas, computation {p}{q}{p}{q}{r}ᵂ satisfies only the first formula, computation {p}{r}ᵂ satisfies only the second one and computations {p}ᵂ or ∅ᵂ don't satisfy any of them.

Currently I'm learning LTL and I tried using AI tools to find more computations that satisfy the formulas, but I got confused because of mixed results. For example the computation {p}{q}{r}ᵂ. According to AI tools it satisfies both formulas but I believe it only satisfies the first formula, and does not satisfy the second formula, because p is not satisfied at all times before r (p is satisfied at t = 0 but not at t = 1).

If someone could confirm if I am right or wrong it would be very helpful.

 

[WWGD]

Welcome to PF!. What is LTL? This seems to deal with Sentence Logic.

 

[alma359]

Linear temporal logic

 

[berkeman]

Currently I'm learning LTL and I tried using AI tools to find more computations that satisfy the formulas, but I got confused because of mixed results. For example the computation {p}{q}{r}ᵂ. According to AI tools it satisfies both formulas but I believe it only satisfies the first formula, and does not satisfy the second formula, because p is not satisfied at all times before r (p is satisfied at t = 0 but not at t = 1).

Please keep in mind that we do not allow AI as a reference in the technical forums here. That is expressly against the PF rules at this time.