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.

Home page

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