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 : $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 [] [have occurred] before P [holds]. (see the English grammar). := T(i)[] 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 ]))]$ $\; := o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge ] ))$ Before R: $\Diamond R \rightarrow (\neg P \; \mathcal{U} \; (R \vee (S \wedge \neg P [\wedge ])))$ $\; := o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge ] ))$ After Q: $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge \Diamond P \rightarrow (\neg P \; \mathcal{U} \; (S \wedge \neg P [\wedge ]))))$ $\; := o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge ] ))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow (\neg P \; \mathcal{U} \; (R \vee (S \wedge \neg P [\wedge ]))))$ $\; := o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge ] ))$ After Q until R: $\Box (Q \rightarrow (\Diamond P \rightarrow (\neg P \; \mathcal{U} \; (R \vee (S \wedge \neg P [\wedge ])))))$ $\; := o(\neg P \; \mathcal{U} \; (T^i \wedge \neg P [\wedge ] ))$ 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 ]$) 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 [] [have occurred] [ Interval(P) ] before P [holds]. (see the English grammar). := T(i)[[UpperTimeBound(i)]][] 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 ])))))$ $\; := o (\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge ] ))$ 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 ]))) \vee \Diamond_{[0,t_{max})} R) \; \mathcal{U} \; R)$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge ] ))$ 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 ]))))))$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge ] ))$ 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 ]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{U} R))$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge ] ))$ 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 ]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{W} R))$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm} (T_i [\wedge ] ))$ 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 ]$) 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 [] [have occurred] [ Interval(P) ] before P [holds] [with ProbabilityBound ]. (see the English grammar). := T(i)[[UpperTimeBound(i)]][] 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 ])))))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge ] ))$ 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 ]))) \vee \Diamond_{[0,t_{max})} R) \; \mathcal{U} \; R)]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge ] ))$ 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 ]))))))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge ] ))$ 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 ]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{U} R))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge ] ))$ 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 ]))) \vee \Diamond_{[0,t_{max})} R) \mathcal{W} R))]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{2.6cm}(T_i [\wedge ] ))$ 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 ]$) 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 : $P$ precedes $S, T_1,T_2,.., T_n$. Structured English Specification Scope, if S [has occurred] and afterwards [] [hold] then it must have been the case that P [has occurred] before S [holds]. (see the English grammar). := T(i)[] 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 )) \rightarrow (\neg S \mathcal{U} P)$ $\; := o \Diamond (T^i [\wedge ])$ Before R: $\Diamond R \rightarrow ((\neg (S \wedge \neg R \wedge )) \mathcal{U} (R \vee P))$ $\; := o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge ]))$ After Q: $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge ((\Diamond (S \wedge )) \rightarrow (\neg S \; \mathcal{U} \; P))))$ $\; := o \Diamond (T^i [\wedge ])$ Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow ((\neg (S \wedge \neg R \wedge )) \; \mathcal{U} \; (R \vee P))))$ $\; := o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge ]))$ After Q until R: $\Box (Q \rightarrow (\neg (S \wedge \neg R \wedge ) \; \mathcal{U} \; (R \vee P) \vee \Box(\neg (S \wedge ))))$ $\; := o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge ]))$ $\; := o \Diamond (T^i [\wedge ])$ This pattern is closely related (it is an extension) to the Precedence 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: 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 [] [hold] then it must have been the case that P [has occurred] [ Interval(S) ] before S [holds]. (see the English grammar). := T(i)[[UpperTimeBound(i)]][] 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 ]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ] ))$ Before R: $\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)}R)\mathcal{U} R)$ $\; := 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 \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{U} \; R)$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ After Q until R: $\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{W} \; R)$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ 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 ]$) 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 [] [hold] then it must have been the case that P [has occurred] [ Interval(S) ] before S [holds] [with ProbabilityBound ]. (see the English grammar). := T(i)[[UpperTimeBound(i)]][] 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 ]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ] ))$ Before R: $[\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)}R)\mathcal{U} R)]_{\bowtie p}$ $\; := 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 \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{U} \; R)]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ After Q until R: $[\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{W} \; R)]_{\bowtie p}$ $\; := o(\Diamond^{[0, t_i]} \;(T_i [\wedge ]))$ 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 ]$) 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.