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.