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.

Home page

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License