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.