Constrained Precedence Chain Property Pattern

Untimed version: N causes - 1 effect

The Constrained Precedence Chain Property Pattern has been proposed by Dwyer in [1].

 Pattern Name and Classification Untimed Precedence Chain N-1: Untimed Order Specification Pattern. Extension of the 2 causes - 1 effect constrained precedence chain pattern proposed by Dwyer in [1]. Structured English Specification Scope, if P [holds] then it must have been the case that S and afterwards [] [have occurred] before P [holds] without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. (see the English grammar). := T(i)[] Pattern Intent N causes -1 effect constrained precedence chain: “$S$, $T^1$, …, $T^n$ without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain” precede $P$. Temporal Logic Mappings Logic Scope Base Formula Extension (with $1 \leq i \leq n$) LTL Globally: $\Diamond P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U} \; (S \wedge \neg P \wedge \neg Z_0 [\wedge ]))]$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Before R: $\Diamond R \rightarrow ((\neg P \wedge \neg Z_0) \; \mathcal{U} \; (R \vee (S \wedge \neg P \wedge \neg Z_0 [\wedge ])))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ After Q: $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge \Diamond P \rightarrow ((\neg P \wedge \neg Z_0) \; \mathcal{U} \; (S \wedge \neg P \wedge \neg Z_0 [\wedge ]))))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow ((\neg P \wedge \neg Z_0) \; \mathcal{U} \; (R \vee (S \wedge \neg P \wedge \neg Z_0 [\wedge ]))))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ After Q until R: $\Box (Q \rightarrow (\Diamond P \rightarrow ((\neg P \wedge \neg Z_0) \; \mathcal{U} \; (R \vee (S \wedge \neg P \wedge \neg Z_0 [\wedge ])))))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ 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 Constrained 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] without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain (see the English grammar). := T(i)[[UpperTimeBound(i)]][] Pattern Intent N causes -1 effect time-bounded precedence chain: “$S$, $T^1$, …, $T^n$ without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain” 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 ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]} \; (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ])))))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Before R: $\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{3.9cm}(S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))) \vee \Diamond^{[0,t_{max})} R) \; \mathcal{U} \; R)$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ After Q: $\Box (Q \;\rightarrow \; \Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]} (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))))))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{6.2cm}(S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{U} R))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ After Q until R: $\Box ((Q \wedge \neg R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{5.3cm}(S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{W} R))$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension.

Probabilistic version: N causes - 1 effect

 Pattern Name and Classification Constrained 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 ] without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain (see the English grammar). := T(i)[[UpperTimeBound(i)]][] Pattern Intent N causes -1 effect probability response chain: “$S$, $T^1$, …, $T^n$” precede $P$ without $Z_0$ holding between P and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain'' precede $P$ within the specified time intervals with a certain probability $\bowtie p$. Temporal Logic Mappings Logic Scope Base Formula Extension (with $2 \leq i \leq n$) MTL Globally: $[\Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]} \; (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ])))))]_{\bowtie p}$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Before R: $[\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{4cm} (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))) \vee \Diamond^{[0,t_{max})} R) \; \mathcal{U} \; R)]_{\bowtie p}$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ After Q: $[\Box (Q \;\rightarrow \; \Box (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{4cm} (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))))))]_{\bowtie p}$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Between Q and R: $[\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{5.8cm} (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{U} R))]_{\bowtie p}$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{3.5cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ After Q until R: $[\Box ((Q \wedge \neg R) \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; P \rightarrow ((\neg P \wedge \neg Z_0)\; \mathcal{U}^{[0,t_{max} - t_{min}]}$ $\hspace{5.3cm} (S \wedge \neg Z_1 \wedge o (\neg Z_1 \; \mathcal{U}^{[0,t_{max} - t_{min} - t_{ST^1}]}(T^1 [\wedge ]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{W} R))]_{\bowtie p}$ $\; := o((\neg P \wedge \neg Z_i) \; \mathcal{U}^{[0, t_{max}- t_{min} - t_{ST^1} - \dots - t_{T^{i-1}T^i}]}$ $\hspace{4cm}(T^i \wedge \neg P \wedge \neg Z_i [\wedge ] ))$ Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension.

Untimed version: 1 Cause - N Effects

 Pattern Name and Classification Constrained Untimed Precedence Chain N-1: Untimed Order Specification Pattern. Extension of 1 cause - 2 effects constrained 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 [] [hold] then it must have been the case that P [has occurred] before S [holds] without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain (see the English grammar). := T(i)[] Pattern Intent 1 cause - N effects constrained precedence chain: $P$ precedes “$S$, $T^1$, …, $T^n$” without $Z_0$ holding between P 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 (with $1 \leq i \leq n$) MTL Globally: $(\Diamond (S \wedge \neg Z_0 \wedge )) \rightarrow ((\neg S \wedge \neg Z_0) \mathcal{U} P)$ $\; := o (\neg Z_i \; \mathcal{U} \; (T^i \wedge \neg Z_i [\wedge ]))$ Before R: $\Diamond R \rightarrow ((\neg (S \wedge \neg R \wedge \neg Z_0 \wedge )) \mathcal{U} (R \vee P))$ $\; := o(\neg R \wedge \neg Z_i \mathcal{U} (T_i \wedge \neg R \wedge \neg Z_i [\wedge ]))$ After Q: $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge ((\Diamond (S \wedge \neg Z_0 \wedge )) \rightarrow ((\neg S \wedge \neg Z_0) \; \mathcal{U} \; P))))$ $\; := o (\neg Z_i \; \mathcal{U} \; (T^i \wedge \neg Z_i [\wedge ]))$ Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow ((\neg (S \wedge \neg R \wedge \neg Z_0 \wedge )) \; \mathcal{U} \; (R \vee P))))$ $\; := o(\neg R \wedge \neg Z_i \mathcal{U} (T_i \wedge \neg R \wedge \neg Z_i [\wedge ]))$ After Q until R: $\Box (Q \rightarrow (\neg (S \wedge \neg R \wedge \neg Z_0 \wedge ) \; \mathcal{U} \; (R \vee P) \vee \Box(\neg (S \wedge ))))$ $\; := o(\neg R \mathcal{U} (T_i \wedge \neg R [\wedge ]))$ $\; := o (\neg Z_i \; \mathcal{U} \; (T^i \wedge \neg Z_i [\wedge ]))$ 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 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] without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain (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$” without $Z_0$ holding between P and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain 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 \neg Z_0 [\wedge ]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ Before R: $\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)}R)\mathcal{U} R)$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ After Q: $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond^{[0, t_{max}]} \; (S \wedge \neg Z_0 [\wedge ] ))))$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ Between Q and R: $\Box (Q \wedge \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{U} \; R)$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ After Q until R: $\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\wedge ]) \rightarrow (\Diamond^{[0, t_{max}-t_{min}]}P \vee \Diamond^{[0, t_{max}+t_1+\dots+t_n)} R ) ) \; \mathcal{W} \; R)$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ Syntax notes The square brackets (as used in $[\wedge ]$) are used as a EBNF syntax construct to describe an optional extension.

Probabilistic version: 1 Cause - N Effects

 Pattern Name and Classification Probabilistic Constrained 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] without $Z_0$ holding between S and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain [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$” without $Z_0$ holding between P and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain within the specified time intervals 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 \neg Z_0 [\wedge ]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)]_{\bowtie p}$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ Before R: $[\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ After Q: $[\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \Diamond^{[0, t_0]} \; (S \wedge \neg Z_0 [\wedge ] ))))]_{\bowtie p}$ $\; := o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ Between Q and R: $[\Box (Q \wedge \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ After Q until R: $[\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge ] ))$ 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.