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.