Absence Property Pattern

# Untimed version

This pattern has been proposed in [1].

 Pattern Name and Classification Absence: Occurrence Specification Pattern Structured English Specification Scope, it is never 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 (\neg P)$ Before R: $\Diamond R \rightarrow (\neg P \; \mathcal{U} \; R)$ After Q: $\Box (Q \rightarrow \Box (\neg P))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\neg P \; \mathcal{U} \; R))$ After Q until R: $\Box (Q \wedge \neg R \rightarrow (\neg P \; \mathcal{W} \; R))$ CTL Globally: $AG(\neg P)$ Before R: $A[(\neg P \vee AG(\neg R)) \; \mathcal{W} \; R]$ After Q: $AG(Q \rightarrow AG(\neg P))$ Between Q and R: $AG(Q \wedge \neg R \rightarrow A[(\neg P \vee AG(\neg R)) \; \mathcal{W} \; R])$ After Q until R: $AG(Q \wedge \neg R \rightarrow A[\neg P \; \mathcal{W} \; R])$ Additional notes The Absence 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 Absence: Real-time Occurrence Specification Pattern Structured English Specification Scope, it is never the case that P [holds] [ Time(0)]. (see the English grammar). Pattern Intent This pattern describes a portion of a system's execution that is free of certain events or states within a time-constraint. Temporal Logic Mappings MTL Globally: $\Box^{[t1,t2]}\;(\neg P)$ Before R: $\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P)))$ After Q: $\Box (Q \rightarrow \Box^{[t1,t2]}\;(\neg P))$ Between Q and R: $\Box((Q \; \wedge \; \Box^{[0,t1]} (\neg R) \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P)))$ After Q until R: $\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow (\neg P \;\mathcal{W}^{[t1,t2]} \;R))$ TCTL Globally: $AG\;^{[t1,t2]}\;(\neg P)$ Before R: $A(((\neg P \;\vee \;AG( \neg R)) \; \mathcal{U}^{[t1,t2]} \;R) \vee (G^{[t1,t2]}(\neg P \wedge \neg R) \; \mathcal{U}^{[t2,\infty)} \;R ))$ After Q: $AG(Q \rightarrow AG\;^{[t1,t2]}\;( \neg P))$ Between Q and R: $AG((Q \; \wedge \; AG^{[0,t1]} (\neg R)) \rightarrow A(((\neg P \;\vee \;AG( \neg R)) \;\mathcal{U}^{[t1,t2]} \;R) \vee (G^{[t1,t2]}(\neg P \wedge \neg R) \;\mathcal{U}^{[t2,\infty)} \;R )))$ After Q until R: $AG((Q\; \wedge \;AG^{[0,t1]} (\neg R)) \rightarrow A(\neg P \; \mathcal{W}^{[t1,t2]} \;R))$ Example and Known Uses For security reasons, after a login failure the system must be free of login attempts between 10 to 50 milliseconds. In this example "after a login failure" represents the scope After Q. Additional notes This pattern is the extension of the Absence pattern introduced by Dwyer in [1]. This pattern can be considered the dual of the Time-constrained Universality pattern.

# Probabilistic version:

 Pattern Name and Classification Probabilistic Absence: Probabilistic Occurrence Specification Pattern Structured English Specification Scope, it is never the case that P [holds] [ Time(0)] [Probability]. (see the English grammar). Pattern Intent This pattern describes a portion of a system's execution that is free of certain events or states with a defined probability. Temporal Logic Mappings PLTL Globally: $[\Box^{[t1,t2]}\;(\neg P)]_{\bowtie p}$ Before R: $[\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P)))]_{\bowtie p}$ After Q: $[\Box (Q \rightarrow \Box^{[t1,t2]}\;(\neg P))]_{\bowtie p}$ Between Q and R: $[\Box((Q \; \wedge \; \Box^{[0,t1]} (\neg R) \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P))]_{\bowtie p}$ After Q until R: $[\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow (\neg P \; \mathcal{W}^{[t1,t2]} \;R))]_{\bowtie p}$ CSL Globally: $\mathcal{P}_{\bowtie p}(\Box^{[t1,t2]}\;(\neg P))$ Before R: $\mathcal{P}_{\bowtie p} (\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee \mathcal{P}_{=1}(\Box^{[t1,t2]} (\neg P))))$ After Q: $\mathcal{P}_{=1} (\Box (Q \rightarrow \mathcal{P}_{\bowtie p} (\Box\;^{[t1,t2]}\;(\neg 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 ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee \mathcal{P}_{=1}(\Box^{[t1,t2]} (\neg P))))$ After Q until R: $\mathcal{P}_{=1} (\Box ((Q\; \wedge \;\mathcal{P}_{=1}(\Box^{[0,t1]} (\neg R))) \rightarrow \mathcal{P}_{\bowtie p}(\neg P \; \mathcal{W}^{[t1,t2]} \;R)))$ Example and Known Uses The probability that the system is free of failures in 2 time units is 0.98. Additional notes This pattern is the extension of the Absence pattern. This pattern can be considered the dual of the Probabilistic Invariance pattern proposed in [2].

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.