# Property Pattern Mappings for CTL

This page describe mappings for property patterns in computation tree logic (CTL).

Many of the mappings use the weak until operator (W) which is related to the strong until operator (U) by the following equivalences:

```A[x W y] = !E[!y U (!x & !y)]
E[x U y] = !A[!y W (!x & !y)]
```

This operator often makes the mappings easier to understand (thanks to William Chan for suggesting this).

For information about the meaning of scopes look here.

# Pattern Mappings

P is false :

 Globally AG(!P) Before R A[(!P | AG(!R)) W R] After Q AG(Q -> AG(!P)) Between Q and R AG(Q & !R -> A[(!P | AG(!R)) W R]) After Q until R AG(Q & !R -> A[!P W R])

P becomes true :

 Globally AF(P) Before R A[!R W (P & !R)] After Q A[!Q W (Q & AF(P))] Between Q and R AG(Q & !R -> A[!R W (P & !R)]) After Q until R AG(Q & !R -> A[!R U (P & !R)])

In these mappings we illustrate one instance of the bounded existence pattern, where the bound is at most 2 designated states. Other bounds can be specified by variations on this mapping.

Transitions to P-states occur at most 2 times :

 Globally `!EF(!P & EX(P & EF(!P & EX(P & EF(!P & EX(P))))))` Before R ```!E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & !R))]))]))]``` After Q `!E[!Q U (Q & EF(!P & EX(P & EF(!P & EX(P & EF(!P & EX(P)))))))]` Between Q and R ```AG(Q -> !E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & !R & EF(R)))]))]))])``` After Q until R ```AG(Q -> !E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & E[!R U (!P & !R & EX(P & !R))]))]))])```

P is true :

 Globally AG(P) Before R A[(P | AG(!R)) W R] After Q AG(Q -> AG(P)) Between Q and R AG(Q & !R -> A[(P | AG(!R)) W R]) After Q until R AG(Q & !R -> A[P W R])

S precedes P :

 Globally `A[!P W S]` Before R `A[(!P | AG(!R)) W (S | R)]` After Q `A[!Q W (Q & A[!P W S])]` Between Q and R `AG(Q & !R -> A[(!P | AG(!R)) W (S | R)])` After Q until R `AG(Q & !R -> A[!P W (S | R)])`

S responds to P :

 Globally AG(P -> AF(S)) Before R `A[((P -> A[!R U (S & !R)]) | AG(!R)) W R]` After Q `A[!Q W (Q & AG(P -> AF(S))] ` Between Q and R `AG(Q & !R -> A[((P -> A[!R U (S & !R)]) | AG(!R)) W R])` After Q until R `AG(Q & !R -> A[(P -> A[!R U (S & !R)]) W R])`

This illustrates the 1 cause-2 effect precedence chain.

P precedes S,T:

 Globally `!E[!P U (S & !P & EX(EF(T)))]` Before R `!E[(!P & !R) U (S & !P & !R & EX(E[!R U (T & !R)]))]` After Q `!E[!Q U (Q & E[!P U (S & !P & EX(EF(T)))])]` Between Q and R ```AG(Q -> !E[(!P & !R) U (S & !P & !R & EX(E[!R U (T & !R & EF(R))]))])``` After Q until R ```AG(Q -> !E[(!P & !R) U (S & !P & !R & EX(E[!R U (T & !R)]))])```

This illustrates the 2 cause-1 effect precedence chain.

S,T precedes P:

 Globally ```!E[!S U P] & !E[!P U (S & !P & EX(E[!T U (P & !T)]))]``` Before R ```!E[(!S & !R) U (P & !R)] & !E[(!P & !R) U (S & !P & !R & EX(E[(!T & !R) U (P & !T & !R)]))]``` After Q ```!E[!Q U (Q & E[!S U P] & E[!P U (S & !P & EX(E[!T U (P & !T)]))])]``` Between Q and R ```AG(Q -> !E[(!S & !R) U (P & !R & EF(R))] & !E[(!P & !R) U (S & !P & !R & EX(E[(!T & !R) U (P & !T & !R & EF(R))]))])``` After Q until R ```AG(Q -> !E[(!S & !R) U (P & !R)] & !E[(!P & !R) U (S & !P & !R & EX(E[(!T & !R) U (P & !T & !R)]))])```

This illustrates the 1 stimulus-2 response chain.

S,T responds to P:

 Globally `AG(P -> AF(S & AX(AF(T))))` Before R ```!E[!R U (P & !R & (E[!S U R] | E[!R U (S & !R & EX(E[!T U R]))]))]``` After Q `!E[!Q U (Q & EF(P & (EG(!S) | EF(S & EX(EG(!T))))))]` Between Q and R ```AG(Q -> !E[!R U (P & !R & (E[!S U R] | E[!R U (S & !R & EX(E[!T U R]))]))])``` After Q until R ```AG(Q -> !E[!R U (P & !R & (E[!S U R] | EG(!S & !R) | E[!R U (S & !R & EX(E[!T U R] | EG(!T & !R)))]))])```

This illustrates the 2 stimulus-1 response chain.

P responds to S,T:

 Globally `!EF(S & EX(EF(T & EG(!P))))` Before R `!E[!R U (S & !R & EX(E[!R U (T & !R & E[!P U R])]))]` After Q `!E[!Q U (Q & EF(S & EX(EF(T & EG(!P)))))]` Between Q and R ```AG(Q -> !E[!R U (S & !R & EX(E[!R U (T & !R & E[!P U R])]))])``` After Q until R ```AG(Q -> !E[!R U (S & !R & EX(E[!R U (T & !R & (E[!P U R] | EG(!P & !R)))]))])```

This is a 1-2 response chain constrained by a single proposition.

S,T without Z responds to P:

 Globally `AG(P -> AF(S & !Z & AX(A[!Z U T])))` Before R ```!E[!R U (P & !R & (E[!S U R] | E[!R U (S & !R & (E[!T U Z] | EX(E[!T U R])))]))]``` After Q ```!E[!Q U (Q & EF(P & (EG(!S) | EF(S & (E[!T U Z] | EX(EG(!T)))))))]``` Between Q and R ```AG(Q -> !E[!R U (P & !R & (E[!S U R] | E[!R U (S & !R & (E[!T U Z] | EX(E[!T U R])))]))])``` After Q until R ```AG(Q -> !E[!R U (P & !R & (E[!S U R] | EG(!S & !R) | E[!R U (S & !R & (E[!T U Z] | EX(E[!T U R] | EG(!T & !R))))]))])```