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.