Recent content by alma359

Linear temporal logic

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...