Maximum Duration
Untimed version:
The untimed version of this pattern does make no sense.
Time-constrained version:
Pattern Name and Classification | ||
Maximum Duration: Real-Time Specification Pattern (Duration) | ||
Structured English Specification | ||
Scope, once P [becomes satistied] it remains so for less than $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 most t time unit(s). | ||
Temporal Logic Mappings | ||
MTL | Globally: | $\Box \; (P \; \vee \; (\; \neg P \; \mathcal{W} \; (P \wedge \Diamond^{[0,t]} \; (\neg P))))$ |
Before R: | $\Diamond \; R \rightarrow ((P \; \vee (\neg P\;\mathcal{U} \; ((P \wedge \Diamond^{[0,t]} \; (\neg P \; \vee\; R)) \; \vee \; R))) \;\mathcal{U} \; R)$ | |
After Q: | $\Box \; ( Q \; \rightarrow \; \Box (P \; \vee \; (\; \neg P \; \mathcal{W} \; (P \wedge \Diamond^{[0,t]} \; (\neg P)))))$ | |
Between Q and R: | $\Box((Q \; \wedge \; \neg R \; \wedge \; \Diamond R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{U} \; ((P \wedge \Diamond^{[0,t]} \; (\neg P\; \vee\; R)) \; \vee \; R))) \;\mathcal{U} \; R))$ | |
After Q until R: | $\Box((Q \; \wedge \; \neg R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{W} \; ((P \wedge \Diamond^{[0,t]} \; (\neg P\; \vee \; R) \; \vee \; R))) \;\mathcal{W} \; R))$ | |
TCTL | Globally: | $AG (P \; \vee \; A(\neg P \; \mathcal{W} \; ( P \wedge AF^{[0,t]} (\neg P ))))$ |
Before R: | $A((P \vee A(\neg P \; \mathcal{W} ((P \wedge AF^{[0,t]}(\neg P \; \vee \; R \; \vee \; AG(\neg R))) \; \vee \; R \vee AG(\neg R))) \vee AG(\neg R)) \; \mathcal{W} \; R)$ | |
After Q: | $AG (Q \; \rightarrow \; AG (P \; \vee \; A(\neg P \; \mathcal{W} \; ( P \wedge AF^{[0,t]} (\neg P )))))$ | |
Between Q and R: | $AG ((Q \wedge \neg R ) \; \rightarrow \; A((P \vee A(\neg P \; \mathcal{W} ((P \wedge AF^{[0,t]}(\neg P \; \vee \; R \; \vee \; AG(\neg R))) \; \vee \; R \vee AG(\neg 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} \; ((P \wedge AF^{[0,t]} (\neg P \; \vee \; 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 Maximum Duration: Probabilistic Specification Pattern (Duration) | ||
Structured English Specification | ||
Scope, once P [becomes satistied] it remains so for less than $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 maximum of t time unit(s) after it switches from false to true. | ||
Temporal Logic Mappings | ||
PLTL | Globally: | $[\Box \; (P \; \vee \; (\; \neg P \; \mathcal{W} \; (P \wedge \Diamond^{[0,t]} \; (\neg P))))]_{\bowtie p}$ |
Before R: | $[\Diamond \; R \rightarrow ((P \; \vee (\neg P\;\mathcal{U} \; ((P \wedge \Diamond^{[0,t]} \; (\neg P \; \vee\; R)) \; \vee \; R))) \;\mathcal{U} \; R)]_{\bowtie p}$ | |
After Q: | $[\Box \; ( Q \; \rightarrow \; \Box (P \; \vee \; (\; \neg P \; \mathcal{W} \; (P \wedge \Diamond^{[0,t]} \; (\neg P)))))]_{\bowtie p}$ | |
Between Q and R: | $[\Box((Q \; \wedge \; \neg R \; \wedge \; \Diamond R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{U} \; ((P \wedge \Diamond^{[0,t]} \; (\neg P\; \vee\; R)) \; \vee \; R)) \;\mathcal{U} \; R))]_{\bowtie p}$ | |
After Q until R: | $[\Box((Q \; \wedge \; \neg R) \; \rightarrow \; ((P \; \vee (\neg P\;\mathcal{W} \; ((P \wedge \Diamond^{[0,t]} \; (\neg P\; \vee \; R) \; \vee \; R))) \;\mathcal{W} \; R))]_{\bowtie p}$ | |
CSL | Globally: | $\mathcal{P}_{=1} \Box (P \; \vee \; \mathcal{P}_{=1}(\neg P \; \mathcal{W} \; ( P \wedge \mathcal{P}_{\bowtie p}\Diamond^{[0,t]} (\neg P))))$ |
Before R: | $\mathcal{P}_{=1}((P \vee \mathcal{P}_{=1}(\neg P \; \mathcal{W} ((P \wedge \mathcal{P}_{\bowtie p}\Diamond^{[0,t]}(\neg P \; \vee \; R \; \vee \; R \;\vee \; \mathcal{P}_{=1}\Box \;(\neg R))) \; \vee \; R \; \vee \mathcal{P}_{=1}\Box \;(\neg 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} \; ( P \wedge \mathcal{P}_{\bowtie p}\Diamond^{[0,t]} (\neg 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} ((P \wedge \mathcal{P}_{\bowtie p}\Diamond^{[0,t]}(\neg P \; \vee \; R \; \vee \; R \;\vee \; \mathcal{P}_{=1}\Box \;(\neg R))) \; \vee \; R \; \vee \mathcal{P}_{=1}\Box \;(\neg 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} \; ((P \wedge \mathcal{P}_{\bowtie p}\Diamond^{[0,t]} (\neg P \; \vee \; R )) \; \vee \; R )) \; \mathcal{W} \; R)))$ | |
Example and Known Uses | ||
Engine starter system [1]: The probability that the system operate in engine cranking mode for no longer that 10 seconds at one time is 0.98. | ||
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.