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. |
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. |
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 |
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. |
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. |
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 |