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.