Existence Property Pattern
Untimed existence
| Pattern Name and Classification | ||
| Existence : Occurrence Specification Pattern | ||
| Structured English Specification | ||
| Scope, P eventually [holds]. (see the English grammar). | ||
| Pattern Intent | ||
| To describe a portion of a system's execution that contains an instance of certain events or states. Also known as Eventually. | ||
| Temporal Logic Mappings | ||
| LTL | Globally: | $\Diamond (P)$ |
| Before R: | $\neg R \; \mathcal{W}\; (P \wedge \neg R)$ | |
| After Q: | $\Box (\neg Q) \vee \Diamond (Q \wedge \Diamond P))$ | |
| Between Q and R: | $\Box (Q \wedge \neg R \rightarrow (\neg R \; \mathcal{W} \; (P \wedge \neg R)))$ | |
| After Q until R: | $\Box (Q \wedge \neg R \rightarrow (\neg R \; \mathcal{U} \; (P \wedge \neg R)))$ | |
| CTL | Globally: | $AF(P)$ |
| Before R: | $A[\neg R \; \mathcal{U} \; (P \wedge \neg R)]$ | |
| After Q: | $A[\neg Q \; \mathcal{W} \; (Q \wedge AF(P))]$ | |
| Between Q and R: | $AG(Q \wedge \neg R \rightarrow A[\neg R \; \mathcal{W} \; (P \wedge \neg R)])$ | |
| After Q until R: | $AG(Q \wedge \neg R \rightarrow A[\neg R \; \mathcal{U} \; (P \wedge \neg R)])$ | |
| Additional notes | ||
| The Existence Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on Untimed version. | ||
Time-constrained version
| Pattern Name and Classification | ||
| Time-constrained Existence: Real-time Occurrence Specification Pattern | ||
| Structured English Specification | ||
| Scope, P eventually [holds] [ Time(0)]. (see the English grammar). | ||
| Pattern Intent | ||
| This pattern aims at describing a portion of a system's execution bounded by a time interval that contains an instance of certain events or states. | ||
| Temporal Logic Mappings | ||
| MTL | Globally: | $\Diamond ^{[t1,t2]}\; (P)$ |
| Before R: | $\neg R \; \mathcal{W}^{[t1,t2]} \; (P \wedge \neg R)$ | |
| After Q: | $\Box (\neg Q) \vee \Diamond(Q \wedge \Diamond^{[t1,t2]} P))$ | |
| Between Q and R: | $\Box ((Q \wedge \Box^{[0,t1]} (\neg R) \wedge (\Diamond^{[t1,\infty)} R)) \rightarrow (\neg R \; \mathcal{W}^{[t1,t2]}\; (P \wedge \neg R)))$ | |
| After Q until R: | $\Box ((Q \wedge \Box^{[0,t1]} (\neg R)) \rightarrow (\neg R \; \mathcal{U}^{[t1,t2]}\; (P \wedge \neg R)))$ | |
| TCTL | Globally: | $AF^{[t1,t2]}\;(P)$ |
| Before R: | $A[\neg R \; \mathcal{W}^{[t1,t2]}\; (P \wedge \neg R)]$ | |
| After Q: | $A[\neg Q \; \mathcal{W} \; (Q \wedge AF^{[t1,t2]}\; (P))]$ | |
| Between Q and R: | $AG(Q \wedge \neg R \rightarrow A[\neg R \; v{W}^{[t1,t2]}\; (P \wedge \neg R)])$ | |
| After Q until R: | $AG(Q \wedge \neg R \rightarrow A[\neg R \; \mathcal{U}^{[t1,t2]} \; (P \wedge \neg R)])$ | |
| Example and Known Uses | ||
| The classic example of existence [1] is specifying termination, e.g., on all executions do we eventually reach a terminal state within a certain time bound. | ||
| Additional notes | ||
| This pattern is the extension of the Existence pattern introduced by Dwyer in [1]. This pattern can be considered the dual of the Time-constrained Absence pattern. | ||
Probabilistic version
| Pattern Name and Classification | ||
| Probabilistic Existence: Probabilistic Occurrence Specification Pattern | ||
| Structured English Specification | ||
| Scope, P eventually [holds] [ Time(0)] [Probability]. (see the English grammar). | ||
| Pattern Intent | ||
| This pattern aims at describing a portion of a system's execution bounded by a time interval that contains an instance of certain events or states with a certain probability. | ||
| Temporal Logic Mappings | ||
| PLTL | Globally: | $[\Diamond ^{[t1,t2]}\; (P)]_{\bowtie p}$ |
| Before R: | $[\neg R \; \mathcal{W}^{[t1,t2]} \; (P \wedge \neg R)]_{\bowtie p}$ | |
| After Q: | $[\Box (\neg Q) \vee \Diamond(Q \wedge \Diamond^{[t1,t2]} P))]_{\bowtie p}$ | |
| Between Q and R: | $[\Box ((Q \wedge \Box^{[0,t1]} (\neg R) \wedge (\Diamond^{[t1,\infty)} R)) \rightarrow (\neg R \; \mathcal{W}^{[t1,t2]}\; (P \wedge \neg R)))]_{\bowtie p}$ | |
| After Q until R: | $[\Box ((Q \wedge \Box^{[0,t1]} (\neg R)) \rightarrow (\neg R \; \mathcal{U}^{[t1,t2]}\; (P \wedge \neg R)))]_{\bowtie p}$ | |
| CSL | Globally: | $\mathcal{P}_{\bowtie p}\Diamond^{[t1,t2]}\;(P)$ |
| Before R: | $\mathcal{P}_{\bowtie p}(\neg R \; \mathcal{W}^{[t1,t2]}\; (P \wedge \neg R))$ | |
| After Q: | $\mathcal{P}_{=1}[\neg Q \; \mathcal{W} \; (Q \wedge \mathcal{P}_{\bowtie p}\Diamond^{[t1,t2]}\; (P))]$ | |
| Between Q and R: | $AG(Q \wedge \neg R \rightarrow A[\neg R \; \mathcal{W}^{[t1,t2]}\; (P \wedge \neg R)])$ | |
| After Q until R: | $AG(Q \wedge \neg R \rightarrow A[\neg R \; \mathcal{U}^{[t1,t2]} \; (P \wedge \neg R)])$ | |
| Example and Known Uses | ||
| Some example of the probabilistic existence pattern from [2]: An ambulance must arrive at the incident scene within 15 min in 95 percent of the cases. or At least 95 percent of issued checks are success-fully cleared. | ||
| Additional notes | ||
| This pattern is the extension of the Existence pattern introduced by Dwyer in [1]. The Existence Property Pattern has been proposed by Dwyer in [2] and it can be found on the following webpage Probabilistic version. | ||
Bibliography
1. Matthew B. Dwyer; George S. Avrunin; James C. Corbett, Patterns in Property Specifications for Finite-State Verification. ICSE 1999. pp. 411-420.
2. Lars Grunske, Specification patterns for probabilistic quality properties. ICSE 2008. pp. 31-40.