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