Property Pattern Mappings for CTL

Property Pattern Mappings for CTL

This page describe mappings for property patterns in computation tree logic (CTL). For other information about the patterns click on the pattern links.

Information about the entire pattern system is available at the Specification Patterns Home Page.

Pattern Mappings

Absence

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

Existence

P becomes true :
Globally AF(P)
Before R !E[!P U R]
After Q !E[!Q U (Q & EG(!P))]
Between Q and R AG(Q -> !E[!P U R])
After Q until R AG(Q -> !E[!P U R] & !EG(!P & !R))

Bounded Existence

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))]))]))])

Universality

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

Precedence

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

Response

S responds to P :
Globally AG(P -> AF(S) )
Before R 
!E[!R U (P & !R & E[!S U R])]
After Q 
!E[!Q U (Q & EF(P & EG(!S)))]
Between Q and R 
AG(Q -> !E[!R U (P & !R & E[!S U R])])
After Q until R 
AG(Q -> !E[!R U (P & !R & (E[!S U R] | EG(!S & !R)))])

Precedence Chain

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)]))])

Response Chain

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)))]))])

Constrained Chain Patterns

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))))]))])