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 [<Chain>] [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).  <Chain>:= T(i)[<Chain>]  
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 <Chain>]))]$ $<Chain>\; :=  o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge <Chain>] ))$
        Before R:               $\Diamond R \rightarrow ((\neg P \wedge \neg Z_0) \; \mathcal{U} \; (R \vee (S \wedge \neg P \wedge \neg Z_0 [\wedge <Chain>])))$ $<Chain>\; :=  o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge <Chain>] ))$  
        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 <Chain>]))))$ $<Chain>\; :=  o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge <Chain>] ))$
        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 <Chain>]))))$ $<Chain>\; :=  o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge <Chain>] ))$
        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 <Chain>])))))$ $<Chain>\; :=  o((\neg P \wedge \neg Z_i) \; \mathcal{U} \; (T^i \wedge \neg P \wedge \neg Z_i [\wedge <Chain>] ))$
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
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 [<Chain>] [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). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
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 <Chain>])))))$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))) \vee \Diamond^{[0,t_{max})} R) \; \mathcal{U} \; R)$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))))))$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{U} R))$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{W} R))$ $<Chain>\; := 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 <Chain>] ))$
Syntax notes
The square brackets (as used in $[\wedge <Chain>]$) 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 [<Chain>] [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). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
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 <Chain>])))))]_{\bowtie p}$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))) \vee \Diamond^{[0,t_{max})} R) \; \mathcal{U} \; R)]_{\bowtie p}$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))))))]_{\bowtie p}$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{U} R))]_{\bowtie p}$ $<Chain>\; := 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 <Chain>] ))$
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 <Chain>]))) \vee \Diamond^{[0,t_{max})} R) \mathcal{W} R))]_{\bowtie p}$ $<Chain>\; := 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 <Chain>] ))$
Syntax notes
The square brackets (as used in $[\wedge <Chain>]$) 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 [<Chain>] [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).  <Chain>:= T(i)[<Chain>]  
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 <Chain>)) \rightarrow ((\neg S \wedge \neg Z_0) \mathcal{U} P)$ $<Chain>\; :=  o (\neg Z_i \; \mathcal{U} \; (T^i \wedge \neg Z_i [\wedge <Chain>]))$
        Before R:               $\Diamond R \rightarrow ((\neg (S \wedge \neg R \wedge \neg Z_0 \wedge <Chain>)) \mathcal{U} (R \vee P))$ $<Chain>\; :=  o(\neg R \wedge \neg Z_i \mathcal{U} (T_i \wedge \neg R \wedge \neg Z_i [\wedge <Chain>]))$  
After Q: $(\Box \neg Q) \vee (\neg Q \; \mathcal{U} \; (Q \wedge ((\Diamond (S \wedge \neg Z_0 \wedge <Chain>)) \rightarrow ((\neg S \wedge \neg Z_0) \; \mathcal{U} \; P))))$ $<Chain>\; :=  o (\neg Z_i \; \mathcal{U} \; (T^i \wedge \neg Z_i [\wedge <Chain>]))$
        Between Q and R: $\Box ((Q \wedge \Diamond R) \rightarrow ((\neg (S \wedge \neg R \wedge \neg Z_0 \wedge <Chain>)) \; \mathcal{U} \; (R \vee P))))$ $<Chain>\; :=  o(\neg R \wedge \neg Z_i \mathcal{U} (T_i \wedge \neg R \wedge \neg Z_i [\wedge <Chain>]))$
        After Q until R:       $\Box (Q \rightarrow (\neg (S \wedge \neg R \wedge \neg Z_0 \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 (\neg Z_i \; \mathcal{U} \; (T^i \wedge \neg Z_i [\wedge <Chain_2>]))$
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 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] 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).  <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]  
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 <Chain>]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)$ $<Chain>\; :=  o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        Before R:               $\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        After Q:                 $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \;  ( \Diamond^{[0, t_{max}]} \; (S \wedge \neg Z_0 [\wedge <Chain>] ))))$ $<Chain>\; :=  o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        Between Q and R: $\Box (Q \wedge \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        After Q until R:       $\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
Syntax notes
The square brackets (as used in $[\wedge <Chain>]$) 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 [<Chain>] [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). <Chain>:= T(i)[[UpperTimeBound(i)]][<Chain>]
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 <Chain>]) \rightarrow \Diamond^{[0, t_{max}-t_{min}]}P)]_{\bowtie p}$ $<Chain>\; :=  o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        Before R:               $[\Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        After Q:                 $[\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \;  ( \Diamond^{[0, t_0]} \; (S \wedge \neg Z_0 [\wedge <Chain>] ))))]_{\bowtie p}$ $<Chain>\; :=  o(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        Between Q and R: $[\Box (Q \wedge \neg R \wedge \Diamond R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
        After Q until R:       $[\Box (Q \wedge \neg R \rightarrow (\Diamond^{[t_{max}, t_{max}]} \; (S \wedge \neg Z_0 [\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(\neg Z_i\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge \neg Z_i [\wedge <Chain>] ))$
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