Response Chain Property Pattern

# Response Chain Property Pattern: 1 stimulus 2 responses

The Response Chain Property Pattern: 1 stimulus 2 responses is a special case of the Response Chain Property Pattern: 1 stimulus N responses. The temporal logical formula for the 1-2 case can be derived by selecting the first (terminating) case for the extension ($Chain$)

# Response Chain Property Pattern: 1 stimulus N responses

## Untimed version (Response Chain 1-N)

 Pattern Name and Classification Response Chain 1-N: Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response S eventually holds []. := followed by T(i)[] Pattern Intent 1 stimulus -N responses response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$. Temporal Logic Mappings Logic Scope Base Formula Extension LTL Globally: $\Box (P \;\rightarrow \; (\Diamond \; (S [\wedge ])))$ $\; := o(\Diamond \;(T_i [\wedge ] ))$ Before R: $\Diamond R \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \mathcal{U} \; (S [\wedge ]))) \mathcal{U} R$ $\; := \neg R \wedge o(\Diamond \;(T_i [\wedge ]))$ After Q: $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond \; (S [\wedge ] ))))$ $\; := o(\Diamond \;(T_i [\wedge ]))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; (\neg R\; \mathcal{U} (S \; [\wedge \; ]))) U R)$ $\; := \neg R \wedge o(\Diamond \;(T_i [\wedge ]))$ After Q until R: $\Box (Q \;\rightarrow \; (P \;\rightarrow \; ( \neg R\; \mathcal{U} (S \; [\wedge \; ]))) \mathcal{W} R )$ $\; := \neg R \wedge o(\Diamond \;(T_i [\wedge ]))$ CTL Globally: $AG(P \rightarrow AF(S [\& ]))$ $\; ::= AX(AF(T_i [\& ]))$ Before R: N/A N/A After Q: N/A N/A Between Q and R: N/A N/A After Q until R: N/A N/A Example and Known Uses Example of original version of this pattern that does not contain time-constraints can be found in [http://patterns.projects.cis.ksu.edu/]. Relationships This pattern is closely related (it is an extension) to the Response Pattern(Untimed version). Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Additional notes The Response Chain Property Pattern has been proposed by Dwyer in [1].

## Time constrained version (Response Chain 1-N)

 Pattern Name and Classification Time-constrained Response Chain 1-N: Real-time Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response [within Time(0)] S eventually holds []. := followed by T(i)[within Time(i)][] Pattern Intent 1 stimulus -N responses time-bounded response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$ within $t_0$ time units between the stimulus and the chain and within $t_1,..,t_n$ time units between the chain elements respectively. Temporal Logic Mappings Logic Scope Base Formula Extension MTL Globally: $\Box (P \;\rightarrow \; (\Diamond^{[0, t_0]} \; (S [\wedge ])))$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ] ))$ Before R: $\Diamond R \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ]))) \mathcal{U} R$ $\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ After Q: $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond^{[0, t_0]} \; (S [\wedge ] ))))$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; (\neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) U R)$ $\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ After Q until R: $\Box (Q \;\rightarrow \; (P \;\rightarrow \; ( \neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) \mathcal{W} R )$ $\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ TCTL Globally: $AG(P \rightarrow AF^{[0, t_0]}(S [\wedge ]))$ $\; ::= \wedge AX(AF^{[0, t_i]} (T_i [\wedge ]))$ Before R: N/A N/A After Q: N/A N/A Between Q and R: N/A N/A After Q until R: N/A N/A Example and Known Uses ABS system. Stimulus - When the electronic control unit (ECU) detects a wheel rotating significantly slower than the others. Responses - (1) ECU actuates the valves to reduce hydraulic pressure to the brake at the affected wheel; (2) the brake assist system is activated within 10 ms Relationships This pattern is closely related (it is an extension) to the Response Pattern(Timed version). Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Additional notes The Response Chain Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found in/as Untimed version.

## Probabilistic version (Response Chain 1-N)

 Pattern Name and Classification Probabilistic Response Chain 1-N: Probabilistic Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response [within Time(0)] S eventually holds [] with [ProbabilityBound]. := followed by T(i)[within Time(i)][] Pattern Intent 1 stimulus-N responses probabilistic time bounded constrained response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$ with a certain probability $_{\bowtie p}$ within $t_0$ time units between the stimulus and the chain and within $t_1,..,t_n$ time units between the chain elements respectively. Temporal Logic Mappings Logic Scope Base Formula Extension PLTL Globally: $[\Box (P \;\rightarrow \; (\Diamond^{[0, t_0]} \; (S [\wedge ])))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ] ))$ Before R: $[\Diamond R \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ]))) \mathcal{U} R]_{\bowtie p}$ $\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ After Q: $[\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond^{[0, t_0]} \; (S [\wedge ] ))))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ Between Q and R: $[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; (\neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) U R)]_{\bowtie p}$ $\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ After Q until R: $[\Box (Q \;\rightarrow \; (P \;\rightarrow \; ( \neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) \mathcal{W} R )]_{\bowtie p}$ $\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ CSL Globally: $\mathcal{P}_{=1} (\Box (P \rightarrow \mathcal{P}_{\bowtie p}(\Diamond^{[0, t_0]}(S [\wedge ]))))$ $\; ::= \mathcal{P}_{=1}(o(\mathcal{P}_{=1}( \Diamond^{[0, t_i]} (T_i [\wedge ]))))$ Before R: N/A N/A After Q: N/A N/A Between Q and R: N/A N/A After Q until R: N/A N/A Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Example and Known Uses ABS system. Stimulus - When the electronic control unit (ECU) detects a wheel rotating significantly slower than the others. Responses - (1) ECU actuates the valves to reduce hydraulic pressure to the brake at the affected wheel; (2) the brake assist system is activated within 10 ms in 99.8% of the cases.

# Response Chain Property Pattern: N stimuli 1 response

## Untimed version (Response Chain N-1)

 Pattern Name and Classification Response Chain N-1: Order Specification Pattern Structured English Specification Scope, if S[] [has occurred], then P eventually holds. := followed by //T(i)[] Pattern Intent N stimulus-1 responses constrained response chain: A system responds to a stimulus $S$ and a chain (of events) $T_1,T_2,.., T_n$ with a response P. Temporal Logic Mappings Logic Scope Base Formula Extension LTL Globally: $\Box (S \wedge o (\Diamond (T _1 \wedge )))$ $\; := o(\Diamond \;(T_i \wedge )) \| o(\Diamond \;(T_i \;\rightarrow \Diamond P ))$ Before R: $\Diamond R \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}\; T_1 \wedge )) \mathcal{U} R)$ $\; := o(\neg R \; \mathcal{U} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U} \;(T_i \;\rightarrow \Diamond P ))$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge o (\Diamond (T _1 \wedge ))))$ $\; := o(\Diamond \;(T_i \wedge )) \| o(\Diamond \;(T_i \;\rightarrow \Diamond P ))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}\; (T_1 \wedge ))) \mathcal{U} R))$ $\; := o(\neg R \; \mathcal{U} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U} \;(T_i \;\rightarrow \Diamond P ))$ After Q and R: $\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}\; T_1 (\wedge ))) \mathcal{W} R))$ $\; := o(\neg R \; \mathcal{U} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U} \;(T_i \;\rightarrow \Diamond P ))$ CTL Globally: N/A N/A Before R: N/A N/A After Q: N/A N/A Between Q and R: N/A N/A After Q until R: N/A N/A Example and Known Uses Example of original version of this pattern that does not contain time-constraints can be found in [http://patterns.projects.cis.ksu.edu/]. Relationships This pattern is closely related (it is an extension) to the Response Pattern(Untimed version). Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Additional notes The Response Chain Property Pattern has been proposed by Dwyer in [1].

## Time constrained version (Response Chain N-1)

 Pattern Name and Classification Time-constrained Response Chain N-1: Real-time Order Specification Pattern Structured English Specification Scope, if S[] [has occurred], then in response [within Time(0)] P eventually holds. := followed by T(i)[within Time(i)][] Pattern Intent N stimulus-1 responses time bounded constrained response chain: A system responds to a stimulus $S$ and a chain (of events) $T_1,T_2,.., T_n$ with a response P within $t_0$ time units between the stimulus including the chain and the response, and within $t_1,..,t_n$ time units between the chain elements respectively. Temporal Logic Mappings Logic Scope Base Formula Extension MTL Globally: $\Box (S \wedge o (\Diamond^{[0, t_1]} (T _1 \wedge )))$ $\; := o(\Diamond^{[0, t_i]} \;(T_i \wedge )) \| o(\Diamond^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ Before R: $\Diamond R \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}^{[0, t_1]}\; T_1 \wedge )) \mathcal{U} R)$ $\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge o (\Diamond^{[0, t_1]} (T _1 \wedge ))))$ $\; := o(\Diamond ^{[0, t_i]} \;(T_i \wedge )) \| o(\Diamond^{[0, t_i]} \;(T_i \;\rightarrow \Diamond P ))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}^{[0, t_1]}\; ( T_1 \wedge ))) \mathcal{U} R))$ $\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ After Q and R: $\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge ))) \mathcal{W} R))$ $\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ TCTL Globally: N/A N/A Before R: N/A N/A After Q: N/A N/A Between Q and R: N/A N/A After Q until R: N/A N/A Example and Known Uses …. Relationships This pattern is closely related (it is an extension) to the Response Pattern(Timed version). Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Additional notes The Response Chain Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found in/as Untimed version.

## Probabilistic version (Response Chain N-1)

 Pattern Name and Classification Probabilistic Response Chain N-1: Probabilistic Order Specification Pattern Structured English Specification Scope, if S[] [has occurred], then in response [within Time(0)] P eventually holds with [ProbabilityBound]. := followed by T(i)[within Time(i)][] Pattern Intent N stimulus-1 responses probabilistic time bounded constrained response chain: A system responds to a stimulus $S$ and a chain (of events) $T_1,T_2,.., T_n$ with a response P with a certain probability $_{\bowtie p}$ within $t_0$ time units between the stimulus including the chain and the response, and within $t_1,..,t_n$ time units between the chain elements respectively. Temporal Logic Mappings Logic Scope Base Formula Extension PLTL Globally: $[\Box (S \wedge o (\Diamond^{[0, t_1]} (T _1 \wedge )))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_i]} \;(T_i \wedge )) \| o(\Diamond^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ Before R: $[\Diamond R \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}^{[0, t_1]}\; T_1 \wedge )) \mathcal{U} R)]_{\bowtie p}$ $\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ After Q: $[\Box (Q \;\rightarrow \; \Box (S \wedge o (\Diamond^{[0, t_1]} (T _1 \wedge ))))]_{\bowtie p}$ $\; := o(\Diamond ^{[0, t_i]} \;(T_i \wedge )) \| o(\Diamond^{[0, t_i]} \;(T_i \;\rightarrow \Diamond P ))$ Between Q and R: $[\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge ))) \mathcal{U} R))]_{\bowtie p}$ $\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ After Q and R: $[\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge ))) \mathcal{W} R))]_{\bowtie p}$ $\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg R \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \Diamond^{[0, t_0]} P ))$ CSL Globally: N/A N/A Before R: N/A N/A After Q: N/A N/A Between Q and R: N/A N/A After Q until R: N/A N/A Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Example and Known Uses …

# Response Chain Property Pattern: 2 stimuli 1 response

## Untimed version (Response Chain 2-1)

 Pattern Name and Classification Response Chain 2-1: Order Specification Pattern Structured English Specification Scope, if S followed by T [has occurred], then in response P eventually holds. Pattern Intent 2 stimuli -1 response response chain: A system responds to a stimulus chain (of events) $S, T$ with $P$. Temporal Logic Mappings Logic Scope Logical Formula LTL Globally: $\Box (S \wedge o (\Diamond T) \;\rightarrow \; o( \Diamond(T \wedge (\Diamond P))))$ Before R: $\Diamond R \;\rightarrow \; (S \wedge o(\neg R \mathcal{U} T ) \;\rightarrow \; o(\neg R \mathcal{U} (T \wedge (\Diamond P)))) \mathcal{U} R$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge o(\Diamond T) \;\rightarrow \; o(\Diamond T \wedge (\Diamond P)))))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge o(\neg R \mathcal{U} T ) \;\rightarrow \; o(\neg R \mathcal{U} (T \wedge (\Diamond P)))) \mathcal{U} R)$ After Q until R: $\Box (Q \;\rightarrow \; (S \wedge o(\neg R \mathcal{U} T ) \;\rightarrow \; o(\neg R \mathcal{U} (T \wedge (\Diamond P)))) \mathcal{U} (R \vee \Box (S \wedge o(\neg R \mathcal{U} T ) \;\rightarrow \; o(\neg R \; \mathcal{U} (T \wedge (\Diamond P))))))$ CTL Globally: N/A Before R: N/A After Q: N/A Between Q and R: N/A After Q until R: N/A Example and Known Uses Example of original version of this pattern that does not contain time-constraints can be found in [http://patterns.projects.cis.ksu.edu/]. Relationships This pattern is closely related (it is an extension) to the Response Pattern(Timed version). Additional notes A generic formulation of the N-1 Response Chain similar to the 1-N Response Chain would require a simultaneous substitution of the extensions  since in the N-1 Response Chain formula fragment are repeated multiple times.

## Time constrained version (Response Chain 2-1)

 Pattern Name and Classification Time-constrained Response Chain 2-1: Real-time Order Specification Pattern Structured English Specification Scope, if S followed by T [has occurred] [within Time(1)], then in response P eventually holds [within Time(0)]. Pattern Intent 2 stimuli -1 responses time-bounded response chain: A system responds to a stimulus chain (of events) $S, T$ with $P$ with a within $t_0$ time units between the chain and the response and within $t_1$ time units between the chain elements respectively. Temporal Logic Mappings Logic Scope Logical Formula MTL Globally: $\Box (S \wedge o (\Diamond^{[0, t_0]} T) \;\rightarrow \; o( \Diamond^{[0, t_1]}(T \wedge (\Diamond^{[0, t_0]} P))))$ Before R: $\Diamond R \;\rightarrow \; (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P)))) \mathcal{U} R$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge o(\Diamond^{[0, t_1]} T) \;\rightarrow \; o(\Diamond^{[0, t_1]} T \wedge (\Diamond^{[0, t_0]} P)))))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P)))) \mathcal{U} R)$ After Q until R: $\Box (Q \;\rightarrow \; (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P)))) \mathcal{U} (R \vee \Box (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \; \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P))))))$ TCTL Globally: N/A Before R: N/A After Q: N/A Between Q and R: N/A After Q until R: N/A Example and Known Uses House Smoke Detector: Stimuli - (1) the optical smoke detector raises a smoke alarm and then (2) the ionization detector raises a smoke alarm; Response- all lights in the house will blink to alert occupants within 10 ms Relationships This pattern is closely related (it is an extension) to the Response Pattern(Timed version).

## Probabilistic version (Response Chain 2-1)

 Pattern Name and Classification Probabilistic Response Chain N-1: Probabilistic Order Specification Pattern Structured English Specification Scope, if S followed by T [has occurred] [within Time(1)], then in response P eventually holds [within Time(0)] with [ProbabilityBound] Pattern Intent N stimuli-1 response probabilistic time bounded response chain: A system responds to a stimulus chain (of events) $S, T_1,T_2,.., T_n$ with $P$ with a certain probability $_{\bowtie p}$ within $t_0$ time units between the chain and the response and within $t_1,..,t_n$ time units between the chain elements respectively. Logic Scope Logical Formula PLTL Globally: $[\Box (S \wedge o (\Diamond^{[0, t_0]} T) \;\rightarrow \; o( \Diamond^{[0, t_1]}(T \wedge (\Diamond^{[0, t_0]} P))))]_{\bowtie p}$ Before R: $[\Diamond R \;\rightarrow \; (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P)))) \mathcal{U} R]_{\bowtie p}$ After Q: $[\Box (Q \;\rightarrow \; \Box (S \wedge o(\Diamond^{[0, t_1]} T) \;\rightarrow \; o(\Diamond^{[0, t_1]} T \wedge (\Diamond^{[0, t_0]} P)))))]_{\bowtie p}$ Between Q and R: $[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P)))) \mathcal{U} R)]_{\bowtie p}$ After Q until R: $[\Box (Q \;\rightarrow \; (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P)))) \mathcal{U} (R \vee \Box (S \wedge o(\neg R \mathcal{U}^{[0, t_1]} T ) \;\rightarrow \; o(\neg R \mathcal{U}^{[0, t_1]} (T \wedge (\Diamond^{[0, t_0]} P))))))]_{\bowtie p}$ CSL Globally: N/A Before R: N/A After Q: N/A Between Q and R: N/A After Q until R: N/A Example and Known Uses House Smoke Detector: Stimuli - (1) the optical smoke detector raises a smoke alarm and then (2) the ionization detector raises a smoke alarm; Response- all lights in the house will blink to alert occupants within 10 ms in 99.9% of the cases

Bibliography
1. Matthew B. Dwyer; George S. Avrunin; James C. Corbett, Patterns in Property Specifications for Finite-State Verification. ICSE 1999. pp. 411-420.