Universality Property Pattern

# Untimed version

This pattern has been proposed in [1].

 Pattern Name and Classification Universality : Occurrence Specification Pattern Structured English Specification Scope, it is always the case that P [holds]. (see the English grammar). Pattern Intent This pattern describes a portion of a system's execution that is free of certain events or states. Temporal Logic Mappings LTL Globally: $\Box (P)$ Before R: $\Diamond R \rightarrow (P \; \mathcal{U} \; R)$ After Q: $\Box (Q \rightarrow \Box (P))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (P \; \mathcal{U} \; R))$ After Q until R: $\Box (Q \wedge \neg R \rightarrow (P \; \mathcal{W} \; R))$ CTL Globally: $AG(P)$ Before R: $A[(P \vee AG(\neg R)) \; \mathcal{W} \; R]$ After Q: $AG(Q \rightarrow AG(P))$ Between Q and R: $AG(Q \wedge \neg R \rightarrow A[(P \vee AG(\neg R)) \; \mathcal{W} \; R])$ After Q until R: $AG(Q \wedge \neg R \rightarrow A[P \; \mathcal{W} \; R])$ Additional notes The Universality 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 Universality: Real-time Occurrence Specification Pattern Structured English Specification Scope, it is always the case that P [holds] [ Time(0)]. (see the English grammar). Pattern Intent This pattern describe a portion of a system's execution which contains only states that have a desired property within a given timebound. Temporal Logic Mappings MTL Globally: $\Box^{[t1,t2]}\;(P)$ Before R: $\Diamond^{[t1,\infty)} R \rightarrow ((P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (P)))$ After Q: $\Box (Q \rightarrow \Box^{[t1,t2]}\;(P))$ Between Q and R: $\Box((Q \; \wedge \; \Box^{[0,t1]} (\neg R) \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow ((P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (P)))$ After Q until R: $\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow (P \;\mathcal{W}^{[t1,t2]} \;R))$ TCTL Globally: $AG\;^{[t1,t2]}\;(P)$ Before R: $A(((P \;\vee \;AG( \neg R)) \;\mathcal{U}^{[t1,t2]} \;R) \vee (G^{[t1,t2]}(P \wedge \neg R) \;\mathcal{U}^{[t2,\infty)} \;R ))$ After Q: $AG(Q \rightarrow AG\;^{[t1,t2]}\;(P))$ Between Q and R: $AG((Q \; \wedge \; AG^{[0,t1]} (\neg R)) \rightarrow A(((P \;\vee \;AG( \neg R)) \;\mathcal{U}^{[t1,t2]} \;R) \vee (G^{[t1,t2]}(P \wedge \neg R) \;\mathcal{U}^{[t2,\infty)} \;R )))$ After Q until R: $AG((Q\; \wedge \;AG^{[0,t1]} (\neg R)) \rightarrow A(P \; \mathcal{W}^{[t1,t2]} \;R))$ Example and Known Uses The water pump is continuously working in the timebound of 10 units of time. Additional notes This pattern is an extension of the pattern proposed in [1]. This pattern is closely related to the Time-constrained Absence and Time-constrained Existence patterns. Universality of a state can be viewed as absence of its negation. For event-based formalisms, we look for the existence of the positive event and absence of the negating event.

# Probabilistic version

 Pattern Name and Classification Probabilistic Universality: Probabilistic Occurrence Specification Pattern Structured English Specification Scope, it is always the case that P [holds] [ Time(0)] [Probability]. (see the English grammar). Pattern Intent This pattern describes a portion of a system's execution universally contains certain events or states with a defined probability. Temporal Logic Mappings PLTL Globally: $[\Box^{[t1,t2]}\;(P)]_{\bowtie p}$ Before R: $[\Diamond^{[t1,\infty)} R \rightarrow ((P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (P)))]_{\bowtie p}$ After Q: $[\Box (Q \rightarrow \Box^{[t1,t2]}\;(P))]_{\bowtie p}$ Between Q and R: $[\Box((Q \; \wedge \; \Box^{[0,t1]} (\neg R) \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow \Diamond^{[t1,\infty)} R \rightarrow ((P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (P)))]_{\bowtie p}$ After Q until R: $[\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow (P \;\mathcal{W}^{[t1,t2]} \;R))]_{\bowtie p}$ CSL Globally: $\mathcal{P}_{\bowtie p}(\Box^{[t1,t2]}\;(P))$ Before R: $\mathcal{P}_{\bowtie p} (\Diamond^{[t1,\infty)} R \rightarrow ((P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee \mathcal{P}_{=1}(\Box^{[t1,t2]} (P))))$ After Q: $\mathcal{P}_{=1} (\Box (Q \rightarrow \mathcal{P}_{\bowtie p} (\Box\;^{[t1,t2]}\;(P))))$ Between Q and R: $\mathcal{P}_{=1} (\Box ((Q \; \wedge \; \mathcal{P}_{=1} \Box^{[0,t1]} (\neg R)) \rightarrow \mathcal{P}_{\bowtie p} (\Diamond^{[t1,\infty)} R \rightarrow ((P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee \; \mathcal{P}_{=1}(\Box^{[t1,t2]} (P)))))$ After Q until R: $\mathcal{P}_{=1} (\Box ((Q\; \wedge \;\mathcal{P}_{=1}\Box^{[0,t1]} (\neg R)) \rightarrow \mathcal{P}_{\bowtie p}(P \; \mathcal{W}^{[t1,t2]} \;R)))$ Example and Known Uses The probability that the water pump is continuously working for 10 units of time without interruption is 0.95. Additional notes This pattern is an extension of the pattern proposed in [1]. This pattern is closely related to the Probabilistic Absence and Probabilistic Existence patterns. Universality of a state can be viewed as absence of its negation. For event-based formalisms, we look for the existence of the positive event and absence of the negating event.

Bibliography
1. Matthew B. Dwyer; George S. Avrunin; James C. Corbett, Patterns in Property Specifications for Finite-State Verification. ICSE 1999. pp. 411-420.