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.