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.