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.