Recurrence Property Pattern

# Untimed version

 Pattern Name and Classification Recurrence: Occurrence Qualitative Patterns Structured English Specification Scope, P [holds] repeatedly. Pattern Intent This pattern requires that P must recurrently hold. Temporal Logic Mappings LTL Globally: $\Box (\Diamond \; P)$ Before R: $\Diamond R \rightarrow ((\Diamond (P \vee R)) \cup R)$ After Q: $\Box (Q \rightarrow \Box (\Diamond \; P))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow ((\Diamond (P \vee R)) \mathcal{U} R))$ After Q until R: $\Box ((Q \wedge \neg R) \rightarrow ((\Diamond (P \vee R)) \mathcal{W} R))$ CTL Globally: $AG(AF \;P)$ Before R: $A[((AF (P \vee R \vee AG(\neg R)))) \mathcal{W} R]$ After Q: $AG(Q \rightarrow AG(AF\; P))$ Between Q and R: $AG((Q \wedge \neg R) \rightarrow A[(AF (P \vee R \vee AG(\neg R))) \mathcal{W} R])$ After Q until R: $AG((Q \wedge \neg R) \rightarrow A[AF (P \vee R) \mathcal{W} R])$ Example and Known Uses The system infinitely often checks the functioning of its sensors. Additional notes This pattern is the repetition over time of the Existence Pattern presented in [1]. As highlighted in [2], this untimed version can be found in several publication, such as [3], and it is commonly used to specify the absence on non-progress cycles in a system.

# Time constrained version

The Recurrence Property Pattern has been proposed in [2].

 Pattern Name and Classification Recurrence: Occurrence Specification Pattern Structured English Specification Scope, P [holds] repeatedly [every $t_u^0 \in \mathbb{R}^+$ TimeUnits]. (see the English grammar). Pattern Intent This pattern describes the periodic satisfaction of a propositional formula. Intuitively, it captures the property that in every c time unit(s), the proposition P has to hold at least once. The proposition P holding more often than every c time units or holding continously is considered a correct behavior in this pattern. Temporal Logic Mappings LTL Globally: $\Box(\Diamond_{\leq c} P)$ Before R: $\Diamond R \rightarrow ((\Diamond_{\leq c}(P \vee R)) \; \mathcal{U}\; R)$ After Q: $\Box (Q \rightarrow \Box (\Diamond_{\leq c P}))$ Between Q and R: $\Box ((Q \wedge \neg R\wedge \Diamond R) \rightarrow ((\Diamond_{\leq c}(P \vee R)) \; \mathcal{U} \; R))$ After Q until R: $\Box ((Q \wedge \neg R) \rightarrow ((\Diamond_{\leq c}(P \vee R)) \; \mathcal{W} \;R))$ CTL Globally: $AG (AF_{\leq c} P)$ Before R: $A[((AF_{\leq c} (P \vee R)) \vee AG(\neg R)) \; \mathcal{W} \;R]$ After Q: $AG(Q \rightarrow AG (AF_{\leq c} P))$ Between Q and R: $AG((Q \wedge \neg R) \rightarrow A[((AF_{\leq c} (P \vee R)) \vee AG(\neg R)) \; \mathcal{W} \;R])$ After Q until R: $AG((Q \wedge \neg R) \rightarrow A[(AF_{\leq c} (P \vee R)) \; \mathcal{W} \;R])$ Additional notes The Recurrence Property Pattern has been proposed by Konrad and Cheng in [2].

# Probabilistic version

 Pattern Name and Classification Probabilistic Recurrence: Time Constrained Patterns Structured English Specification Scope, P [holds] repeatedly [every $t_u^0 \in \mathbb{R}^+$ TimeUnits] [Probability]. (see the English grammar). Pattern Intent This pattern describes the periodic satisfaction of a state formula. Intuitively, it captures the property that in every interval [a, a +c] within the scope of the property at time, the state formula P has to hold at least once. Temporal Logic Mappings PLTL Globally: $[\Box (\Diamond^{[t1,t2]}\; P)]_{\bowtie p}$ Before R: $[\Diamond R \rightarrow ((\Diamond^{[t1,t2]}\; (P \vee R)) \mathcal{U} R)]_{\bowtie p}$ After Q: $[\Box (Q \rightarrow \Box (\Diamond^{[t1,t2]}\; P))]_{\bowtie p}$ Between Q and R: $[\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow ((\Diamond^{[t1,t2]}\;(P \vee R)) \mathcal{U} R))]_{\bowtie p}$ After Q until R: $[\Box ((Q \wedge \neg R) \rightarrow ((\Diamond^{[t1,t2]}\;(P \vee R)) \mathcal{W} R))]_{\bowtie p}$ CSL Globally: $\mathcal{P}_{\bowtie p}(\Box (\Diamond^{[t1,t2]}\; P))$ Before R: $\mathcal{P}_{= 1}(\Diamond R \rightarrow \mathcal{P}_{\bowtie p}((\Diamond^{[t1,t2]}\; (P \vee R)) \mathcal{U} R))$ After Q: $\mathcal{P}_{= 1}(\Box (Q \rightarrow \mathcal{P}_{\bowtie p} \Box (\Diamond^{[t1,t2]}\; P)))$ Between Q and R: $\mathcal{P}_{= 1}(\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow \mathcal{P}_{\bowtie p}((\Diamond^{[t1,t2]}\;(P \vee R)) \mathcal{U} R)))$ After Q until R: $\mathcal{P}_{= 1}(\Box ((Q \wedge \neg R) \rightarrow \mathcal{P}_{\bowtie p}((\Diamond^{[t1,t2]}\;(P \vee R)) \mathcal{W} R)))$ Example and Known Uses The system checks the functioning of its sensors in an interval of 3 units of time. Additional notes This pattern is a probabilistic version of the recurrence pattern.

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. Sascha Konrad; Betty H.C. Cheng, Real-time specification patterns.ICSE 2005. pp. 372-381.
3. Holzmann, Gerard J.The Spin Model Checker: Primer and Reference Manual.Addison Wesley Publishing Company, 2003.