Precedence Chain Property Pattern

Untimed version: N causes - 1 effect

Pattern Name and Classification
Untimed Precedence Chain N-1: Untimed Order Specification Pattern. Extension of the 2 causes - 1 effect precedence chain pattern proposed by Dwyer in [1]: $S, T_1,T_2,.., T_n$ precede $P$.
Structured English Specification
Scope, if P [holds] then it must have been the case that S and afterwards [<Chain>] [have occurred] before P [holds]. (see the English grammar).  <Chain>:= T(i)[<Chain>]  
Pattern Intent
N causes -1 effect precedence chain: “$S$, $T^1$, …, $T^n$” precede $P$.
Temporal Logic Mappings
Logic Scope                   Base Formula Extension (with $1 \leq i \leq n$)
LTL   Globally:               $\Diamond P \rightarrow (\neg P \; \mathcal{U} \; (S \wedge \neg P [\wedge <Chain>]))]$ $<Chain>\; :=  o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge <Chain>] ))$
        Before R:               $\Diamond R \rightarrow (\neg P \; \mathcal{U} \; (R \vee (S \wedge \neg P [\wedge <Chain>])))$ $<Chain>\; :=  o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge <Chain>] ))$  
        After Q:                 $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge \Diamond P \rightarrow (\neg P \; \mathcal{U} \; (S \wedge \neg P [\wedge <Chain>]))))$ $<Chain>\; :=  o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge <Chain>] ))$
        Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow (\neg P \; \mathcal{U} \; (R \vee (S \wedge \neg P [\wedge <Chain>]))))$ $<Chain>\; :=  o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge <Chain>] ))$
        After Q until R:       $\Box (Q \rightarrow (\Diamond P \rightarrow (\neg P \; \mathcal{U} \; (R \vee (S \wedge \neg P [\wedge <Chain>])))))$ $<Chain>\; :=  o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge <Chain>] ))$
Relationships
This pattern is closely related (it is an extension) to the Precedence 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.

Time constrained version: N causes - 1 effect

Pattern Name and Classification
Time-constrained Precedence Chain N-1: Real-time Order Specification Pattern
Structured English Specification
Scope, if P [holds] then it must have been the case that S and afterwards [<Chain>] [have occurred] [ Interval(P) ] before P [holds]. (see the English grammar). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
Pattern Intent
N causes -1 effect time-bounded precedence chain: “$S$, $T^1$, …, $T^n$” precede $P$ within the specified time intervals. For example for $n$=2, if $P$ holds, it must be the case that (i) $S$ held no more than $t_{max}$ time units before and no less than $t_{min}$ time units before, and (ii) $T$ held no more than $t_{min}$ time units before and no less than $t_{ST}$ time units before, where $t_{ST}$ is the maximum time distance between $S$ and $T$.
Temporal Logic Mappings
Logic Scope Base Formula Extension (with $2 \leq i \leq n$)
MTL Globally: $\Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>])))))$ $<Chain>\; := o (\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge <Chain>] ))$
Before R: $\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]} $ $\hspace{3.7cm}(S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))) \vee \Diamond_{[0,t_{max})} R) \; \mathcal{U} \; R)$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge <Chain>] ))$
After Q: $\Box (Q \;\rightarrow \; \Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))))))$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge <Chain>] ))$
Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]}$ $\hspace{3.7cm} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{U} R))$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge <Chain>] ))$
After Q until R: $\Box ((Q \wedge \neg R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]}$ $\hspace{3.7cm} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{W} R))$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge <Chain>] ))$
Example and Known Uses
For $n$=2, the brake assist system must be activated only if, no more than 50ms before, the electronic control unit has detected a wheel rotating significantly slower than the others and, after that, the valves have been actuated to reduce hydraulic pressure to the brake at the affected wheel.
Relationships
This pattern is closely related (it is an extension) to the Precedence 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
For $n$=2, it is worth noting that, looking into the past, $t_{max}$ and $t_{min}$ are time distances that start from the time of $P$. In particular, $t_{min}$ is the minimum time distance between “$S$,$T$” and $P$ and it can be set to zero if no minimum time distance is required between “$S$,$T$” and $P$. Moreover, $t_{ST}$ is the maximum time distance between $S$ and $T$ and it can be omitted if no maximum time distance is required between $S$ and $T$. For instance, concerning the brake assist system above, the time distance $t_{min}$ can be set to zero and the time distance $t_{ST}$ can be omitted. The time bound $t_{max}$ will be set to 50ms.

Probabilistic version: N causes - 1 effect

Pattern Name and Classification
Probabilistic Precedence Chain N-1: Probabilistic Order Specification Pattern
Structured English Specification
Scope, if P [holds] then it must have been the case that S and afterwards [<Chain>] [have occurred] [ Interval(P) ] before P [holds] [with ProbabilityBound ]. (see the English grammar). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
Pattern Intent
N causes -1 effect probabilistic precedence chain: “$S$, $T^1$, …, $T^n$” precede $P$ within the specified time intervals with a certain probability $\bowtie p$. For example for $n$=2, if $P$ holds, it must be the case that (i) $S$ held no more than $t_{max}$ time units before and no less than $t_{min}$ time units before, and (ii) $T$ held no more than $t_{min}$ time units before and no less than $t_{ST}$ time units before, where $t_{ST}$ is the maximum time distance between $S$ and $T$, with a certain probability $\bowtie p$.
Temporal Logic Mappings
Logic Scope Base Formula Extension (with $2 \leq i \leq n$)
LTL Globally: $[\Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>])))))]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge <Chain>] ))$
Before R: $[\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]}$ $\hspace{3.7cm} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))) \vee \Diamond_{[0,t_{max})} R) \; \mathcal{U} \; R)]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge <Chain>] ))$
After Q: $[\Box (Q \;\rightarrow \; \Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))))))]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge <Chain>] ))$
Between Q and R: $[\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]}$ $\hspace{3.7cm} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{U} R))]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge <Chain>] ))$
After Q until R: $[\Box ((Q \wedge \neg R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow (\Diamond^{[0,t_{max} - t_{min}]}$ $\hspace{3.7cm} (S \wedge o (\Diamond^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge <Chain>]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{W} R))]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge <Chain>] ))$
Example and Known Uses
For $n$=2, the brake assist system must be activated only if, no more than 50ms before, the electronic control unit has detected a wheel rotating significantly slower than the others and, after that, the valves have been actuated to reduce hydraulic pressure to the brake at the affected wheel, with a probability greater than 0.995.
Relationships
This pattern is closely related (it is an extension) to the Precedence Pattern(Probabilistic 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

Untimed version: 1 Cause - N Effects

Pattern Name and Classification
Untimed Precedence Chain N-1: Untimed Order Specification Pattern. Extension of 1 cause - 2 effects precedence chain pattern proposed by Dwyer in [1]: $P$ precedes $S, T_1,T_2,.., T_n$.
Structured English Specification
Scope, if S [has occurred] and afterwards [<Chain>] [hold] then it must have been the case that P [has occurred] before S [holds]. (see the English grammar).  <Chain>:= T(i)[<Chain>]  
Pattern Intent
1 cause - N effects precedence chain: $P$ precedes “$S$, $T^1$, …, $T^n$”.
Temporal Logic Mappings
Logic Scope                   Base Formula Extension (with $1 \leq i \leq n$)
MTL   Globally:               $(\Diamond (S \wedge <Chain>)) \rightarrow (\neg S \mathcal{U} P)$ $<Chain>\; :=  o \Diamond (T^i [\wedge <Chain>])$
        Before R:               $\Diamond R \rightarrow ((\neg (S \wedge \neg R \wedge <Chain>)) \mathcal{U} (R \vee P))$ $<Chain>\; :=  o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge <Chain>]))$  
After Q: $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge ((\Diamond (S \wedge <Chain>)) \rightarrow (\neg S \; \mathcal{U} \; P))))$ $<Chain>\; := o \Diamond (T^i [\wedge <Chain>])$
        Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow ((\neg (S \wedge \neg R \wedge <Chain>)) \; \mathcal{U} \; (R \vee P))))$ $<Chain>\; :=  o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge <Chain>]))$
        After Q until R:       $\Box (Q \rightarrow (\neg (S \wedge \neg R \wedge <Chain>) \; \mathcal{U} \; (R \vee P) \vee \Box(\neg (S \wedge <Chain_2>))))$ $<Chain>\; :=  o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge <Chain>]))$ $<Chain_2>\; :=  o \Diamond (T^i [\wedge <Chain_2>])$
This pattern is closely related (it is an extension) to the Precedence 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.

Time constrained version: 1 Cause - N Effects

Pattern Name and Classification
Time-constrained Precedence Chain 1-N: Real-time Order Specification Pattern.
Structured English Specification
Scope, if S [has occurred] and afterwards [<Chain>] [hold] then it must have been the case that P [has occurred] [ Interval(S) ] before S [holds]. (see the English grammar). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
Pattern Intent
1 cause - N effects time-bounded precedence chain: $P$ precedes “$S$, $T^1$, …, $T^n$” within the specified time intervals. For example for $n$=2, if $S$ holds at time $t_{max}$ and $T$ holds no more than $t_{ST}$ time units later, it must be the case that $P$ held no more than $t_{max}$ time units before $S$ and no less than $t_{min}$ time units before $S$.
Temporal Logic Mappings
Logic Scope Base Formula Extension
MTL Globally: $\Box (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)$ $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>] ))$
Before R: $\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)}R)\mathcal{U} R)$ $<Chain>\; := 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 \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{U} \; R)$ $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$
After Q until R: $\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{W} \; R)$ $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$
Example and Known Uses
For $n$=2. Portable Gas Detector: The Audio alarm is sounded and after the Visual alarm is blink only if, no more than 1 second before, a gas concentration higher than a threshold has been detected. The property states that the Portable Gas Detector must not have false Audio and Visual alarms, and that the cause for such alarms must occur no more than 1 second before.
Additional notes **
This pattern is closely related (it is an extension) to the Precedence 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
It is worth noting that, in the case of $n$=2, looking into the past, $t_{max}$ and $t_{min}$ are time distances that start from the time of $S$. In particular, $t_{min}$ is the minimum time distance between $P$ and “$S$,$T$” and it can be set to zero if no minimum time distance is required between $P$ and “$S$,$T$”. Moreover, $t_{ST}$ is the maximum time distance between $S$ and $T$ and it can be omitted if no maximum time distance is required between $S$ and $T$. For instance, concerning the Portable Gas Detector above, the time distance $t_{min}$ can be set to zero and the time distance $t_{ST}$ can be set omitted. The time bound $t_{max}$ will be set to 1s.

Probabilistic version: 1 Cause - N Effects

Pattern Name and Classification
Probabilistic Precedence Chain 1-N: Probabilistic Order Specification Pattern.
Structured English Specification
Scope, if S [has occurred] and afterwards [<Chain>] [hold] then it must have been the case that P [has occurred] [ Interval(S) ] before S [holds] [with ProbabilityBound ]. (see the English grammar). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
Pattern Intent
1 cause - N effects probabilistic precedence chain: $P$ precedes “$S$, $T^1$, …, $T^n$” within the specified time intervals with a certain probability $\bowtie p$. For example for $n$=2, if $S$ holds at time $t_{max}$ and $T$ holds no more than $t_{ST}$ time units later, it must be the case that $P$ held no more than $t_{max}$ time units before $S$ and no less than $t_{min}$ time units before $S$, with a certain probability $\bowtie p$.
Temporal Logic Mappings
Logic Scope Base Formula Extension
MTL Globally: $[\Box (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>] ))$
Before R: $[\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)}R)\mathcal{U} R)]_{\bowtie p}$ $<Chain>\; := 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 \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{U} \; R)]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$
After Q until R: $[\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge <Chain>]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{W} \; R)]_{\bowtie p}$ $<Chain>\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge <Chain>]))$
Example and Known Uses
For $n$=2. Portable Gas Detector: The Audio alarm is sounded and after the Visual alarm is blink only if, no more than 1 second before, a gas concentration higher than a threshold has been detected. The property states that the Portable Gas Detector must not have false Audio and Visual alarms, and that the cause for such alarms must occur no more than 1 second before, with a probability greater than 0.995.
Additional notes **
This pattern is closely related (it is an extension) to the Precedence Pattern(Probabilistic 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

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