Minimum Duration

Untimed version:

The untimed version of this pattern does make no sense.


Time-constrained version:

Pattern Name and Classification
Minimum Duration: Real-Time Specification Pattern (Duration)
Structured English Specification
Scope, once P [becomes satistied] it remains so for at least $t_u^0 \in \mathbb{R}^+$ TimeUnits. (see the English grammar).
Pattern Intent
This pattern captures the property that every time the state formula P switches from false to true, it will remain true for at least t time unit(s).
Temporal Logic Mappings
MTL Globally: $\Box \; (P \; \vee \; (\; \neg P \; \mathcal{W} \; \Box^{[0,t]} \; P))$
Before R: $\Diamond \; R \rightarrow ((P \; \vee (\neg P\;\mathcal{U} \; (\Box^{[0,t]} \; (P\; \wedge \; \neg R) \; \vee \; R))) \;\mathcal{U} \; R)$
After Q: $\Box \; ( Q \; \rightarrow \; \Box (P \; \vee \; (\; \neg P \; \mathcal{W} \; \Box^{[0,t]} \; P)))$
Between Q and R: $\Box((Q \; \wedge \; \neg R \; \wedge \; \Diamond R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{U} \; (\Box^{[0,t]} \; (P\; \wedge \; \neg R) \; \vee \; R))) \;\mathcal{U} \; R))$
After Q until R: $\Box((Q \; \wedge \; \neg R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{W} \; (\Box^{[0,t]} \; (P\; \wedge \; \neg R) \; \vee \; R))) \;\mathcal{W} \; R))$
TCTL Globally: $AG (P \; \vee \; A(\neg P \; \mathcal{W} \; AG^{[0,t]} P ))$
Before R: $A((P \vee A(\neg P \; \mathcal{W} (AG^{[0,t]}((P \; \wedge \; \neg R) \; \vee AG(\neg R)) \; \vee \; R )) \vee AG(\neg R)) \; \mathcal{W} \; R)$
After Q: $AG (Q \; \rightarrow \; AG (P \; \vee \; A(\neg P \; \mathcal{W} \; AG^{[0,t]} P )))$
Between Q and R: $AG ((Q \wedge \neg R ) \; \rightarrow \; A((P \; \vee \;A(\neg P \; \mathcal{W} \; ( AG^{[0,t]} ((P \; \wedge \; \neg R ) \; \vee \; AG(\neg R)) \; \vee \; R )) \vee AG(\neg R)) \; \mathcal{W} \; R))$
After Q until R: $AG ((Q \wedge \neg R ) \;\rightarrow \; (A(P \; \vee A(\neg P \; \mathcal{W} \; ( AG^{[0,t]} (P \; \wedge \; \neg R )) \; \vee \; R ) \; \mathcal{W} \; R)))$
Additional notes
The Minimum Duration Property Pattern has been proposed in [1].

Probabilistic version:

Pattern Name and Classification
Probabilistic Minimum Duration: Probabilistic Specification Pattern (Duration)
Structured English Specification
Scope, once P [becomes satistied] it remains so for at least $t_u^0 \in \mathbb{R}^+$ TimeUnits [Probability]. (see the English grammar).
Pattern Intent
This pattern captures the property that with a probability higher or lower than p ($\mathcal{P}_{\bowtie p}$) the state formula P will hold for at least c time unit(s).
Temporal Logic Mappings
PLTL Globally: $[\Box \; (P \; \vee \; (\; \neg P \; \mathcal{W} \; \Box^{[0,t]} \; P))]_{\bowtie p}$
Before R: $[\Diamond \; R \rightarrow ((P \; \vee (\neg P\;\mathcal{U} \; (\Box^{[0,t]} \; (P\; \wedge \; \neg R) \; \vee \; R))) \;\mathcal{U} \; R)]_{\bowtie p}$
After Q: $[\Box \; ( Q \; \rightarrow \; \Box (P \; \vee \; (\; \neg P \; \mathcal{W} \; \Box^{[0,t]} \; P)))]_{\bowtie p}$
Between Q and R: $[\Box((Q \; \wedge \; \neg R \; \wedge \; \Diamond R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{U} \; (\Box^{[0,t]} \; (P\; \wedge \; \neg R) \; \vee \; R))) \;\mathcal{U} \; R))]_{\bowtie p}$
After Q until R: $[\Box((Q \; \wedge \; \neg R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{W} \; (\Box^{[0,t]} \; (P\; \wedge \; \neg R) \; \vee \; R))) \;\mathcal{W} \; R))]_{\bowtie p}$
CSL Globally: $\mathcal{P}_{=1} \Box (P \; \vee \; \mathcal{P}_{=1}(\neg P \; \mathcal{W} \; \mathcal{P}_{\bowtie p}\Box^{[0,t]} P ))$
Before R: $\mathcal{P}_{=1}((P \vee \mathcal{P}_{=1}(\neg P \; \mathcal{W} (\mathcal{P}_{\bowtie p}\Box^{[0,t]}((P \; \wedge \; \neg R) \; \vee \mathcal{P}_{=1}\Box \;(\neg R)) \; \vee \; R )) \vee \mathcal{P}_{=1}\Box \;(\neg R)) \; \mathcal{W} \; R)$
After Q: $\mathcal{P}_{=1}\Box \;(Q \; \rightarrow \; \mathcal{P}_{=1}\Box \; (P \; \vee \; \mathcal{P}_{=1}(\neg P \; \mathcal{W} \; \mathcal{P}_{\bowtie p}\Box^{[0,t]} P )))$
Between Q and R: $\mathcal{P}_{=1}\Box\; ((Q \wedge \neg R ) \; \rightarrow \; \mathcal{P}_{=1}((P \; \vee \;\mathcal{P}_{=1}(\neg P \; \mathcal{W} \; ( \mathcal{P}_{\bowtie p}\Box^{[0,t]} ((P \; \wedge \; \neg R ) \; \vee \; \mathcal{P}_{=1}\Box \;(\neg R)) \; \vee \; R )) \vee \mathcal{P}_{=1}\Box (\neg R)) \; \mathcal{W} \; R))$
After Q until R: $\mathcal{P}_{=1}\Box ((Q \wedge \neg R ) \;\rightarrow \; (\mathcal{P}_{=1}(P \; \vee \mathcal{P}_{=1}(\neg P \; \mathcal{W} \; ( \mathcal{P}_{\bowtie p}\Box^{[0,t]} (P \; \wedge \; \neg R )) \; \vee \; R ) \; \mathcal{W} \; R)))$
Example and Known Uses
Engine starter system [1]: The probability that the system has a minimum "off" period of 120 seconds before it reenters the cranking mode is 0.95.
Additional notes
This pattern is an extension of the original time-constrained proposed in [1].

Bibliography
1. Sascha Konrad; Betty H.C. Cheng, Real-time specification patterns.ICSE 2005. pp. 372-381.

Home page

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License