[SOLVED] Is this CTL formula equivalent and what makes it hold?

Is this CTL formula equivalent and what makes it hold?

I'm wondering if the CTL formulas below are equivalent and if so, can you help me persuade myself that they are? A(p U ( A(q U r) )) = A(A(p U q) U r)

I can't come up with any models that contradicts it and my guts tells me the formulas are equivalent but I can't find any equivalences that supports that statement. I've tried to rewrite the equivalence A(p U q) == not(E ((not q) U not(p or q)) or EG (not q)) into something helpful but failed several times.

I've looked through my course material as well as google but I can't find anything. I did however find another question here that has the same equivalence question but with no answer, so I'm trying to make a second try.

Solution

Note: this answer might be late.

However, since the question was raised multiple times, I think it's still useful.

Question: Is A[p U A[q U r]] equivalent to A[A[p U q] U r]?

Answer: no.

To prove that the inequality stands, it is sufficient to provide a single Kripke Structure s.t. A[p U A[q U r]] is verified but A[A[p U q] U r] is not (or the converse).

Now, for simplicity, we assume to deal with a Kripke Structure in which every state has only one possible future state. Therefore, we can forget about the A modifier and consider the LTL version of the given problem: is [p U [q U r]] equivalent to [[p U q] U r]?.

Let's break down [p U [q U r]]:

[q U r] is true on paths which match the expression {q}*{r}
[p U [q U r]] is true on paths that mach {p}*{[q U r]} = {p}*{q}*{r}

What about [[p U q] U r]?

[p U q] is true on paths which match the expression {p}*{q}
[[p U q] U r] is true on paths that mach {[p U q]}*{r} = {{p}*{q}}*{r}

Now, {p}*{q}*{r} != {{p}*{q}}*{r}.

In fact, {p}*{q}*{r} matches any path in which a sequence of p is followed by r and there is no q along the way.

However, {{p}*{q}}*{r} does not. If a path contains a sequence of p, then the occurrence of q before r is mandatory.

Thus, the two formulas are not equivalent.

Hands-On Answer:

Let's encode a Kripke structure that provides the same counter-example using NuSMV

MODULE main ()
VAR
  p: boolean;
  q: boolean;
  r: boolean;

INVAR !q;

INIT
  !q & p & !r

TRANS
  r -> next(r);

TRANS
  p & !r -> next(r);

CTLSPEC A[p U A[q U r]];
CTLSPEC A[A[p U q] U r];

and check it:

~$ NuSMV -int
NuSMV > reset; read_model -i test.smv; go; check_property
-- specification A [ p U A [ q U r ]  ]   is true
-- specification A [ A [ p U q ]  U r ]   is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  p = TRUE
  q = FALSE
  r = FALSE

Indeed, one property is verified but the other is not.