Bounded Existence Pattern
Untimed version
In these mappings we illustrate one instance of the bounded existence pattern, where the bound is at most 2 designated states. Other bounds can be specified by variations on this mapping.
transitions to P-states occur at most 2 times
| Pattern Name and Classification | ||
| Bounded Existence: Occurrence Specification Pattern | ||
| Structured English Specification | ||
| Scope, P [holds] at most n times. (see the English grammar). | ||
| Pattern Intent | ||
| This pattern describes a portion of a system's execution that contains at most a specified number of instances of a designated state transition or event. | ||
| Temporal Logic Mappings | ||
| LTL | Globally: | $(\neg P \; \mathcal{W} \; (P \; \mathcal{W} \; (\neg P \; \mathcal{W} \; (P \; \mathcal{W} \; \Box \neg P))))$ |
| Before R: | $\Diamond R \rightarrow ((\neg P \wedge \neg R) \; \mathcal{U} \; (R \vee ((P \wedge \neg R) \; \mathcal{U} \; (R \vee ((\neg P \wedge \vee R) \mathcal{U} (R \vee ((P \wedge \neg R) \; \mathcal{U} \; (R \vee (\neg P \; \mathcal{U} \; R)))))))))$ | |
| After Q: | $\Diamond Q \rightarrow (\neg Q \; \mathcal{U} \; (Q \wedge (\neg P \; \mathcal{W} \; (P \; \mathcal{W} \; (\neg P \; \mathcal{W} \; (P \; \mathcal{W} \; \Box \neg P))))))$ | |
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \rightarrow ((\neg P \wedge \neg R) \; \mathcal{U} \; (R \; \vee \; ((P \wedge \neg R) \; \mathcal{U} \; (R \vee ((\neg P \wedge \neg R) \; \mathcal{U} \; (R \; \vee \; ((P \wedge \neg R) \; \mathcal{U} \; (R \; \vee \; (\neg P \; \mathcal{U} \; R))))))))))$ | |
| After Q until R: | $\Box (Q \rightarrow ((\neg P \wedge \neg R) \; \mathcal{U} \; (R \; \vee \; ((P \wedge \neg R) \mathcal{U} (R \vee ((\neg P \wedge \neg R) \mathcal{U} (R \vee ((P \wedge \neg R) \; \mathcal{U} \; (R \; \vee \; (\neg P \; \mathcal{W} \; R) \vee \Box P)))))))))$ | |
| CTL | Globally: | $\neg EF(\neg P \wedge EX(P \wedge EF(\neg P \wedge EX(P \wedge EF(\neg P \wedge EX(P))))))$ |
| Before R: | $\neg E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge \neg R))]))]))]$ | |
| After Q: | $\neg E[\neg Q \; \mathcal{U} \; (Q \wedge EF(\neg P \wedge EX(P \wedge EF(\neg P \wedge EX(P \wedge EF(\neg P \wedge EX(P)))))))]$ | |
| Between Q and R: | $AG(Q \rightarrow \neg E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge \neg R \wedge EF(R)))]))]))])$ | |
| After Q until R: | $AG(Q \rightarrow \neg E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge E[\neg R \; \mathcal{U} \; (\neg P \wedge \neg R \wedge EX(P \wedge \neg R))]))]))])$ | |
| Additional notes | ||
| The Bounded Existence 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
A time-constrained extension for the bounded existence is not applicable.
Indeed, we could not find any use case, in published papers and other available documents we searched, justifying the need of such a pattern.
Probabilistic version
A probabilistic extension for the bounded existence is not applicable.
Indeed, we could not find any use case, in published papers and other available documents we searched, justifying the need of such a 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.