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 [<Chain>]. | <Chain>:= followed by T(i)[<Chain>] | ||
| 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 <Chain>])))$ | $<Chain>\; := o(\Diamond \;(T_i [\wedge <Chain>] ))$ |
| Before R: | $\Diamond R \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \mathcal{U} \; (S [\wedge <Chain>]))) \mathcal{U} R$ | $<Chain>\; := \neg R \wedge o(\Diamond \;(T_i [\wedge <Chain>]))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond \; (S [\wedge <Chain>] ))))$ | $<Chain>\; := o(\Diamond \;(T_i [\wedge <Chain>]))$ | |
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; (\neg R\; \mathcal{U} (S \; [\wedge \; <Chain>]))) U R)$ | $<Chain>\; := \neg R \wedge o(\Diamond \;(T_i [\wedge <Chain>]))$ | |
| After Q until R: | $\Box (Q \;\rightarrow \; (P \;\rightarrow \; ( \neg R\; \mathcal{U} (S \; [\wedge \; <Chain>]))) \mathcal{W} R )$ | $<Chain>\; := \neg R \wedge o(\Diamond \;(T_i [\wedge <Chain>]))$ | |
| CTL | Globally: | $AG(P \rightarrow AF(S [\& <Chain>]))$ | $<Chain>\; ::= AX(AF(T_i [\& <Chain>]))$ |
| 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 <Chain>]$) 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 [<Chain>]. | <Chain>:= followed by T(i)[within Time(i)][<Chain>] | ||
| 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 <Chain>])))$ | $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>] ))$ |
| Before R: | $\Diamond R \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>]))) \mathcal{U} R$ | $<Chain>\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond^{[0, t_0]} \; (S [\wedge <Chain>] ))))$ | $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; (\neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) U R)$ | $<Chain>\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q until R: | $\Box (Q \;\rightarrow \; (P \;\rightarrow \; ( \neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) \mathcal{W} R )$ | $<Chain>\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| TCTL | Globally: | $AG(P \rightarrow AF^{[0, t_0]}(S [\wedge <Chain>]))$ | $<Chain>\; ::= \wedge AX(AF^{[0, t_i]} (T_i [\wedge <Chain>]))$ |
| 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 <Chain>]$) 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 [<Chain>] with [ProbabilityBound]. | <Chain>:= followed by T(i)[within Time(i)][<Chain>] | ||
| 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 <Chain>])))]_{\bowtie p}$ | $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>] ))$ |
| Before R: | $[\Diamond R \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>]))) \mathcal{U} R]_{\bowtie p}$ | $<Chain>\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q: | $[\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond^{[0, t_0]} \; (S [\wedge <Chain>] ))))]_{\bowtie p}$ | $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| Between Q and R: | $[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; (\neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) U R)]_{\bowtie p}$ | $<Chain>\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q until R: | $[\Box (Q \;\rightarrow \; (P \;\rightarrow \; ( \neg R\; \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) \mathcal{W} R )]_{\bowtie p}$ | $<Chain>\; := \neg R \wedge o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| CSL | Globally: | $\mathcal{P}_{=1} (\Box (P \rightarrow \mathcal{P}_{\bowtie p}(\Diamond^{[0, t_0]}(S [\wedge <Chain>]))))$ | $<Chain>\; ::= \mathcal{P}_{=1}(o(\mathcal{P}_{=1}( \Diamond^{[0, t_i]} (T_i [\wedge <Chain>]))))$ |
| 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 <Chain>]$) 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[<Chain>] [has occurred], then P eventually holds. | <Chain>:= followed by //T(i)[<Chain>] | ||
| 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 <Chain>)))$ | $<Chain>\; := o(\Diamond \;(T_i \wedge <Chain>)) \| o(\Diamond \;(T_i \;\rightarrow \Diamond P ))$ |
| Before R: | $\Diamond R \;\rightarrow \; ((S \wedge o(\neg R \;\mathcal{U}\; T_1 \wedge <Chain> )) \mathcal{U} R)$ | $<Chain>\; := o(\neg R \; \mathcal{U} \;(T_i \wedge <Chain>)) \| o(\neg R \;\mathcal{U} \;(T_i \;\rightarrow \Diamond P ))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (S \wedge o (\Diamond (T _1 \wedge <Chain>))))$ | $<Chain>\; := o(\Diamond \;(T_i \wedge <Chain>)) \| 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 <Chain> ))) \mathcal{U} R))$ | $<Chain>\; := o(\neg R \; \mathcal{U} \;(T_i \wedge <Chain>)) \| 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 <Chain> ))) \mathcal{W} R))$ | $<Chain>\; := o(\neg R \; \mathcal{U} \;(T_i \wedge <Chain>)) \| 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 <Chain>]$) 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[<Chain>] [has occurred], then in response [within Time(0)] P eventually holds. | <Chain>:= followed by T(i)[within Time(i)][<Chain>] | ||
| 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 <Chain>)))$ | $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain> )) \mathcal{U} R)$ | $<Chain>\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain>))))$ | $<Chain>\; := o(\Diamond ^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain> ))) \mathcal{U} R))$ | $<Chain>\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain> ))) \mathcal{W} R))$ | $<Chain>\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain>]$) 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[<Chain>] [has occurred], then in response [within Time(0)] P eventually holds with [ProbabilityBound]. | <Chain>:= followed by T(i)[within Time(i)][<Chain>] | ||
| 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 <Chain>)))]_{\bowtie p}$ | $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain> )) \mathcal{U} R)]_{\bowtie p}$ | $<Chain>\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain>))))]_{\bowtie p}$ | $<Chain>\; := o(\Diamond ^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain> ))) \mathcal{U} R))]_{\bowtie p}$ | $<Chain>\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain> ))) \mathcal{W} R))]_{\bowtie p}$ | $<Chain>\; := o(\neg R \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| 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 <Chain>]$) 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 $<Chain>$ 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.