Property Pattern Mappings for LTL
Property Pattern Mappings for LTL
This page describe mappings for property patterns in linear
temporal logic (LTL).
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
P is false :
Globally |
[](!P) |
Before R |
<>R -> (!P U R) |
After Q |
[](Q -> [](!P)) |
Between Q and R |
[]((Q & <>R) -> !P U R) |
After Q until R |
[](Q -> !P U (R | [](!P))) |
P becomes true :
Globally |
<>(P) |
Before R |
<>R -> (!R U P) |
After Q |
[](!Q) | <>(Q & <>P)) |
Between Q and R |
[]((Q & <>R) -> (!R U P)) |
After Q until R |
[](Q -> (!R U P)) |
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. To improve
the readability of these mappings we use the
weak-until operator which is defined as:
P W Q == []P | (P U Q)
transitions to P-states occur at most 2 times :
Globally |
(!P W (P W (!P W (P W []!P)))) |
Before R |
<>R -> ((!P & !R) U (R | ((P & !R) U
(R | ((!P & !R) U (R | ((P & !R) U
(R | (!P U R))))))))) |
After Q |
<>Q -> (!Q U (Q & (!P W (P W (!P W (P W []!P))))))
|
Between Q and R |
[]((Q & <>R) ->
((!P & !R) U (R | ((P & !R) U
(R | ((!P & !R) U (R | ((P & !R) U
(R | (!P U R)))))))))) |
After Q until R |
[](Q -> ((!P & !R) U (R | ((P & !R) U
(R | ((!P & !R) U (R | ((P & !R) U
(R | (!P W R) | []P))))))))) |
P is true :
Globally |
[](P) |
Before R |
<>R -> (P U R) |
After Q |
[](Q -> [](P)) |
Between Q and R |
[]((Q & <>R) -> P U R) |
After Q until R |
[](Q -> P U (R | [](P))) |
S precedes P:
Globally |
<>P -> (!P U (S & !P)) |
Before R |
<>R -> (!P U (S | R)) |
After Q |
[]!Q | <>(Q & (!P U (S | []!P))) |
Between Q and R |
[]((Q & <>R) -> (!P U (S | R))) |
After Q until R |
[](Q -> ((!P U (S | R)) | []!P)) |
S responds to P :
Globally |
[](P -> <>S) |
Before R |
(P -> (!R U S)) U (R | [](!R)) |
After Q |
[](Q -> [](P -> <>S)) |
Between Q and R |
[]((Q & <>R) -> (P -> (!R U S)) U R) |
After Q until R |
[](Q -> ((P -> (!R U S)) U R) | [](P -> (!R U S))) |
This illustrates the 2 cause-1 effect precedence chain.
S, T precedes P:
Globally |
<>P -> (!P U (S & !P & o(!P U T)))
|
Before R |
<>R -> (!P U (R | (S & !P & o(!P U T))))
|
After Q |
([]!Q) | (!Q U (Q & <>P -> (!P U (S & !P & o(!P U T))))
|
Between Q and R |
[]((Q & <>R) -> (!P U (R | (S & !P & o(!P U T)))))
|
After Q until R |
[](Q -> (<>P -> (!P U (R | (S & !P & o(!P U T))))))
|
This illustrates the 1 cause-2 effect precedence chain.
P precedes (S, T):
Globally |
(<>(S & o<>T)) -> ((!S) U P)) |
Before R |
<>R -> ((!(S & (!R) & o(!R U (T & !R)))) U (R | P))
|
After Q |
([]!Q) | ((!Q) U (Q & ((<>(S & o<>T)) -> ((!S) U P)))
|
Between Q and R |
[]((Q & <>R) -> ((!(S & (!R) & o(!R U (T & !R)))) U (R | P)))
|
After Q until R |
[](Q -> (!(S & (!R) & o(!R U (T & !R))) U (R | P) | [](!(S & o<>T))))
|
This illustrates the 2 stimulus-1 response chain.
P responds to S,T:
Globally |
[] (S & o<> T -> o(<>(T & <> P)))
|
Before R |
<>R -> (S & o(!R U T) -> o(!R U (T & <> P))) U R
|
After Q |
[] (Q -> [] (S & o<> T -> o(!T U (T & <> P))))
|
Between Q and R |
[] ((Q & <>R) -> (S & o(!R U T) -> o(!R U (T & <> P))) U R)
|
After Q until R |
[] (Q -> (S & o(!R U T) -> o(!R U (T & <> P))) U
(R | [] (S & o(!R U T) -> o(!R U (T & <> P))))) |
This illustrates the 1 stimulus-2 response chain.
S,T responds to P:
Globally |
[] (P -> <>(S & o<>T))
|
Before R |
<>R -> (P -> (!R U (S & !R & o(!R U T)))) U R
|
After Q |
[] (Q -> [] (P -> (S & o<> T)))
|
Between Q and R |
[] ((Q & <>R) -> (P -> (!R U (S & !R & o(!R U T)))) U R)
|
After Q until R |
[] (Q -> (P -> (!R U (S & !R & o(!R U T)))) U
(R | [] (P -> (S & o<> T)))) |
This is the 2-1 response chain constrained by a single proposition.
S,T without Z responds to P:
Globally |
[] (P -> <>(S & !Z & o(!Z U T)))
|
Before R |
<>R -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U R
|
After Q |
[] (Q -> [] (P -> (S & !Z & o(!Z U T))))
|
Between Q and R |
[] ((Q & <>R) -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U R)
|
After Q until R |
[] (Q -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U
(R | [] (P -> (S & !Z & o(!Z U T))))) |