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.