How to express the fact that one property occurs in one path before another property in CTL?

24 Views Asked by At

I would like to express the fact that there is a path where the "p" property occurs before the φ goal, in CTL as shown in the following figure. enter image description here For this I thought of the formula ∃(∃◇p U ∃◇φ ). Is this formula correct?

0

There are 0 best solutions below