Constrained Response Chain Property Pattern

# Constrained Response Chain Property Pattern: 1 stimulus 2 responses

The Constrained Response Chain Property Pattern: 1 stimulus 2 responses is a special case of the Constrained 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$)

# Constrained Response Chain Property Pattern: 1 stimulus N responses

## Untimed version (Constrained Response Chain 1-N)

 Pattern Name and Classification Constrained Response Chain 1-N: Order Specification Pattern Scope, if P [has occurred], then in response [without Constraint(0)] S eventually holds []. := followed by T(i)[without Constraint(i)][] Pattern Intent 1 stimulus -N responses constrained response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$ without $Z_S$ holding between the stimulus and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Base Formula Extension LTL Globally: $\Box (P \;\rightarrow \; (\neg Z_S \; \mathcal{U}\; (S [\wedge ])))$ $::= \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}\;(T_i [\wedge ]))$ Before R: $\Diamond R \;\rightarrow \; (P \;\rightarrow \; ((\neg R \; \wedge \; \neg Z_S) \; \mathcal{U} \; (S [\wedge ]))) U R$ $\; ::= \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge ] ))$ After Q: $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \neg Z_S \; \mathcal{U} \; (S [\wedge ]\; ))))$ $\; ::= \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge ]))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; ((\neg R\; \wedge \;\neg Z_S) \mathcal{U} (S \; [\wedge \; ] ))) U R)$ $\; ::= \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge ]))$ After Q until R: $\Box (Q \;\rightarrow \; (P \;\rightarrow \; (( \neg R\; \wedge \; \neg Z_S) \mathcal{U} (S \; [\wedge \; \;] ))) \mathcal{W} R )$ $\; ::= \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge ] ))$ CTL Globally: $AG(P \rightarrow A(!Z_S \mathcal{U}(S [\& ])))$ $\; ::= !Z_i \& AX(A(!Z_i \mathcal{U} (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 Untimed version (Response Chain 1-N) pattern. Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Additional notes The Constrained Response Chain Property Pattern has been proposed by Dwyer in [1].

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

 Pattern Name and Classification Time-constrained Constrained Response Chain 1-N: Real-time Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response [within Time(0)][without Constraint(0)] S eventually holds []. := followed by T(i)[within Time(i)][without Constraint(i)][] Pattern Intent 1 stimulus -N responses constrained 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 and without $Z_S$ holding between the stimulus and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Base Formula Extension MTL Globally: $\Box (P \;\rightarrow \; (\neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ])))$ $\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ] ))$ Before R: $\Diamond R \;\rightarrow \; (P \;\rightarrow \; ((\neg R \; \wedge \; \neg Z_S) \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ]))) U R$ $\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ After Q: $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ] ))))$ $\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; ((\neg R\; \wedge \;\neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) U R)$ $\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ After Q until R: $\Box (Q \;\rightarrow \; (P \;\rightarrow \; (( \neg R\; \wedge \; \neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) \mathcal{W} R )$ $\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ TCTL Globally: $AG(P \rightarrow A(\neg Z_S \mathcal{U}^{[0, t_0]}(S [\wedge ])))$ $\; ::= \neg Z_i \wedge AX(A( \neg Z_i \mathcal{U}^{[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 Cargo Smoke Controller: Stimulus - a cargo controller signals a smoke controller warning; Responses - (1) the air ventilation system is turned off and then (2) the compartment isolation valves are closed within 60 seconds; Constraint: recognized a false warning. Relationships This pattern is closely related (it is an extension) to the Time constrained version (Response Chain 1-N) pattern. Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension. Additional notes The Constrained 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 (Constrained Response Chain 1-N)

 Pattern Name and Classification Probabilistic Constrained Response Chain 1-N: Probabilistic Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response [within Time(0)][without Constraint(0)] S eventually holds [] with [ProbabilityBound]. := followed by T(i)[within Time(i)][without Constraint(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 and without $Z_S$ holding between the stimulus and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Base Formula Extension PLTL Globally: $[\Box (P \;\rightarrow \; (\neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ])))]_{\bowtie p}$ $\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ] ))$ Before R: $[\Diamond R \;\rightarrow \; (P \;\rightarrow \; ((\neg R \; \wedge \; \neg Z_S) \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ]))) U R]_{\bowtie p}$ $\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ After Q: $[\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge ] ))))]_{\bowtie p}$ $\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ Between Q and R: $[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; ((\neg R\; \wedge \;\neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) U R)]_{\bowtie p}$ $\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ After Q until R: $[\Box (Q \;\rightarrow \; (P \;\rightarrow \; (( \neg R\; \wedge \; \neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; ]))) \mathcal{W} R )]_{\bowtie p}$ $\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge ]))$ CSL Globally: $\mathcal{P}_{=1} (\Box (P \rightarrow \mathcal{P}_{\bowtie p}(\neg Z_S \mathcal{U}^{[0, t_0]}(S [\wedge ]))))$ $\; ::= \neg Z_i \wedge \mathcal{P}_{=1}(o(\mathcal{P}_{=1}( \neg Z_i \mathcal{U}^{[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. Relationships This pattern is closely related (it is an extension) to the Probabilistic version (Response Chain 1-N) pattern. Example and Known Uses Cargo Smoke Controller: Stimulus - a cargo controller signals a smoke controller warning; Responses - (1) the air ventilation system is turned off and then (2) the compartment isolation valves are closed within 60 seconds with a probability of 99.99%; Constraint: recognized a false warning.

# Constrained Response Chain Property Pattern: N stimuli 1 response

## Untimed version (Constrained Response Chain N-1)

 Pattern Name and Classification Constrained Response Chain N-1: Order Specification Pattern Structured English Specification Scope, if S[] [has occurred], then P eventually holds and without $Z_P$ holding between the stimulus and the chain := followed by //T(i)[] without $Z_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 without $Z_P$ holding between the stimulus including the chain and the response, and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Base Formula Extension LTL Globally: $\Box (S \wedge o (\neg Z_1 \; \mathcal{U} (T _1 \wedge )))$ $\; := o(\neg Z_i \; \mathcal{U} \;(T_i \wedge )) \| o(\neg Z_i \; \mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ Before R: $\Diamond R \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}\; T_1 \wedge )) \mathcal{U} R)$ $\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge o (\neg Z_1 \; \mathcal{U} (T _1 \wedge ))))$ $\; := o(\neg Z_i \; \mathcal{U} \;(T_i \wedge )) \| o(\neg Z_i \; \mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}\; (T_1 \wedge ))) \mathcal{U} R))$ $\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ After Q and R: $\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1) \;\mathcal{U}\; T_1 (\wedge ))) \mathcal{W} R))$ $\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i )\;\mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} 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 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.

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

 Pattern Name and Classification Time-constrained 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 without $Z_P$ ever holding. := followed by T(i) without $Z_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 and without $Z_P$ holding between the stimulus including the chain and the response, and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Base Formula Extension MTL Globally: $\Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge )))$ $\; := o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ Before R: $\Diamond R \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; T_1 \wedge )) \mathcal{U} R)$ $\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge ))))$ $\; := o(\neg Z_1 \; \mathcal{U} ^{[0, t_i]} \;(T_i \wedge )) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; ( T_1 \wedge ))) \mathcal{U} R))$ $\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i)\;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ After Q and R: $\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge ))) \mathcal{W} R))$ $\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i)\;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[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 Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension.

## Probabilistic version (Constrained Response Chain N-1)

 Pattern Name and Classification Probabilistic Constrained 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 without $Z_P$ ever holding with [ProbabilityBound]. := followed by T(i) without $Z_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 and without $Z_P$ holding between the stimulus including the chain and the response, and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Base Formula Extension PLTL Globally: $[\Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge )))]_{\bowtie p}$ $\; := o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ Before R: $[\Diamond R \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; T_1 \wedge )) \mathcal{U} R)]_{\bowtie p}$ $\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ After Q: $[\Box (Q \;\rightarrow \; \Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge ))))]_{\bowtie p}$ $\; := o(\neg Z_i \; \mathcal{U} ^{[0, t_i]} \;(T_i \wedge )) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ Between Q and R: $[\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge ))) \mathcal{U} R))]_{\bowtie p}$ $\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ After Q and R: $[\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge ))) \mathcal{W} R))]_{\bowtie p}$ $\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge )) \| o((\neg R \wedge \neg Z_i)\;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[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.

# Constrained Response Chain Property Pattern: 2 stimuli 1 response

## Untimed version (Constrained Response Chain 2-1)

 Pattern Name and Classification Constrained Response Chain 2-1: Order Specification Pattern Structured English Specification Scope, if S followed by T [has occurred] [without Constraint(1)], then in response P eventually holds [without Constraint(0)]. Pattern Intent 2 stimuli -1 response constrained response chain: A system responds to a stimulus chain (of events) $S, T$ with $P$ without $Z_P$ holding between the chain and the response and without $Z_1$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Logical Formula LTL Globally: $\Box (S \wedge \neg Z_1 \wedge o (\neg Z_1 \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o( \neg Z_1 \mathcal{U}(T \wedge (\neg Z_P \mathcal{U} P))))$ Before R: $\Diamond R \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) U (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) U (T \wedge (\neg Z_P U P)))) U R$ After Q: $\Box (Q \;\rightarrow \; \Box (S \wedge \neg Z_1 \wedge o(\neg Z_1 \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o(\neg Z_1 \mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P)))))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1)\mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P)))) U R)$ After Q until R: $\Box (Q \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \;o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P)))) U (R \vee \Box (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge (\neg Z_P \mathcal{U} 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 Untimed version (Response Chain N-1) pattern. Additional notes A generic formulation of the N-1 Constrained Response Chain similar to the 1-N Constrained Response Chain would require a simultaneous substitution of the extensions  since in the N-1 Constrained Response Chain formula fragment are repeated multiple times.

 Pattern Name and Classification Time-constrained Constrained Response Chain 2-1: Real-time Order Specification Pattern Structured English Specification Scope, if S followed by T [has occurred] [within Time(1)] [without Constraint(1)], then in response P eventually holds [within Time(0)][without Constraint(1)]. Pattern Intent 2 stimuli -1 responses constrained 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 and without $Z_P$ holding between the chain and the response and without $Z_1$ holding between the elements of the chain. Temporal Logic Mappings Logic Scope Logical Formula MTL Globally: $\Box (S \wedge \neg Z_1 \wedge o (\neg Z_1 \mathcal{U}^{[0, t_0]} (T \wedge \neg Z_P)) \;\rightarrow \; o( \neg Z_1 \mathcal{U}^{[0, t_1]}(T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P))))$ Before R: $\Diamond R \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) U ## Probabilistic version (Constrained Response Chain 2-1)  Pattern Name and Classification Probabilistic Constrained Response Chain N-1: Probabilistic Order Specification Pattern Structured English Specification Scope, if S followed by T [has occurred] [within Time(1)] [without Constraint(1)], then in response P eventually holds [within Time(0)][without Constraint(0)] with [ProbabilityBound] Pattern Intent N stimuli-1 response probabilistic time bounded constrained 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 and without$Z_P$holding between the chain and the response and without$Z_1,Z_2,.., Z_n$holding between the elements of the chain. Logic Scope Logical Formula PLTL Globally:$[\Box (S \wedge \neg Z_1 \wedge o (\neg Z_1 \mathcal{U}^{[0, t_0]} (T \wedge \neg Z_P)) \;\rightarrow \; o( \neg Z_1 \mathcal{U}^{[0, t_1]}(T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P))))]_{\bowtie p}$Before R:$[\Diamond R \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) \mathcal{U} R]_{\bowtie p}$After Q:$[\Box (Q \;\rightarrow \; \Box (S \wedge \neg Z_1 \wedge o(\neg Z_1 \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o(\neg Z_1 \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))))]_{\bowtie p}$Between Q and R:$[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1)\mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) U R)]_{\bowtie p}$After Q until R:$[\Box (Q \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) U (R \vee \Box (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[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 TOLL Road Design: Stimuli - (1) a car is passing a gantry and (2) then the system detects a speed greater than 130km/h; Constraint: Without an OCR failure to recognize the number plate; Response -the image made by the camera is send to the operator within 1 second with a probability of 99.99%. Relationships This pattern is closely related (it is an extension) to the Probabilistic version (Response Chain N-1) pattern.

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