Precedence Property Pattern

# Untimed version

The Precedence Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on Untimed version.

 Pattern Name and Classification Precedence: Order Specification Pattern Structured English Specification Scope, if P [holds], then it must have been the case that S [has occurred] before P [holds]. (see the English grammar). Pattern Intent To describe relationships between a pair of events/states P and S where the occurrence of P is a necessary pre-condition for an occurrence of S. We say that P precedes S Temporal Logic Mappings LTL Globally: $\neg P \; \mathcal{W} \; S$ Before R: $\Diamond R \rightarrow (\neg P \; \mathcal{U} \; (S \vee R))$ After Q: $\Box \neg Q \vee \Diamond (Q \wedge (\neg P \; \mathcal{W} \; S))$ Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\neg P \; \mathcal{U} \; (S \vee R)))$ After Q until R: $\Box (Q \wedge \neg R \rightarrow (\neg P \; \mathcal{W} \; (S \vee R)))$ CTL Globally: $A[\neg P \; \mathcal{W} \; S]$ Before R: $A[(\neg P \vee AG(\neg R)) \; \mathcal{U} \; (S \vee R)]$ After Q: $A[\neg Q \; \mathcal{W} \; (Q \wedge A[\neg P \; \mathcal{U} \; S])]$ Between Q and R: $AG(Q \wedge \neg R \rightarrow A[(\neg P \vee AG(\neg R)) \; \mathcal{W} \; (S \vee R)])$ After Q until R: $AG(Q \wedge \neg R \rightarrow A[\neg P \; \mathcal{W} \; (S \vee R)])$ Additional notes The Precedence 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

This pattern comes from [3].

 Pattern Name and Classification Time-constrained Precedence: Real-time Order Specification Pattern Structured English Specification Scope, if P [holds], then it must have been the case that S [has occurred] [Interval(0)] before P [holds]. (see the English grammar). Pattern Intent $S$ precedes $P$ between $t_{max}$ and $t_{min}$. If $P$ holds, it must be the case that $S$ held no more than $t_{max}$ time units before and no less than $t_{min}$ time units before. Temporal Logic Mappings MTL Globally: $\Box(\Box^{[0, t_{max} - t_{min})} \neg S \rightarrow \Box^{[t_{max},t_{max}]} \neg P)$ Globally (our version): $\Box ( \Diamond^{[t_{max},t_{max}]} P \rightarrow \Diamond^{[0, t_{max} - t_{min})} S)$ Before R: $\Diamond R \rightarrow (\Box^{[0, t_{max} - t_{min})} \neg S \wedge \Box^{[0,t_{max})} \neg R \rightarrow \Box^{[t_{max},t_{max}]} \neg P) \mathcal{U} R$ Before R (our version): $\Diamond R \rightarrow ( \Diamond^{[t_{max},t_{max}]} P \rightarrow (\Diamond^{[0, t_{max} - t_{min})} S \vee \Diamond^{[0,t_{max})} R) ) \mathcal{U} R$ After Q: $\Box (Q \rightarrow \Box (\Box^{[0, t_{max} - t_{min})} \neg S \rightarrow \Box^{[t_{max},t_{max}]} \neg P))$ After Q (our version): $\Box( Q \rightarrow \Box( \Diamond^{[t_{max},t_{max}]} P \rightarrow \Diamond^{[0, t_{max} - t_{min})} S) )$ Between Q and R: $\Box (Q \wedge \neg R \wedge \Diamond R \rightarrow (\Box^{[0, t_{max} - t_{min})} \neg S \wedge \Box^{[0,t_{max})} \neg R \rightarrow \Box^{[t_{max},t_{max}]} \neg P) \mathcal{U} R)$ Between Q and R (our version): $\Box (Q \wedge \neg R \wedge \Diamond R \rightarrow ( \Diamond^{[t_{max},t_{max}]} P \rightarrow (\Diamond^{[0, t_{max} - t_{min})} S \vee \Diamond^{[0,t_{max})} R) ) \mathcal{U} R)$ After Q until R: $\Box (Q \wedge \neg R \rightarrow (\Box^{[0, t_{max} - t_{min})} \neg S \wedge \Box^{[0,t_{max})} \neg R \rightarrow \Box^{[t_{max},t_{max}]} \neg P) \mathcal{W} R)$ After Q until R (our version): $\Box( Q \wedge \neg R \rightarrow ( \Diamond^{[t_{max},t_{max}]} P \rightarrow (\Diamond^{[0, t_{max} - t_{min})} S \vee \Diamond^{[0,t_{max})} R) ) \mathcal{W} R)$ TCTL Globally: $AG(AG^{[0, t_{max} - t_{min})} \neg S \rightarrow AG^{[t_{max},t_{max}]} \neg P)$ Before R: $AF R \rightarrow A(AG^{[0, t_{max} - t_{min})} \neg S \wedge AG^{[0,t_{max})} \neg R \rightarrow AG^{[t_{max},t_{max}]} \neg P) \mathcal{U} R$ After Q: $AG(Q \rightarrow AG(AG^{[0, t_{max} - t_{min})} \neg S \rightarrow AG^{[t_{max},t_{max}]} \neg P))$ Between Q and R: $AG(Q \wedge \neg R \wedge AF R \rightarrow A (AG^{[0, t_{max} - t_{min})} \neg S \wedge AG^{[0,t_{max})} \neg R \rightarrow AG^{[t_{max},t_{max}]} \neg P) \mathcal{U} R)$ After Q until R: $AG(Q \wedge \neg R \rightarrow A(AG^{[0, t_{max} - t_{min})} \neg S \wedge AG^{[0,t_{max})} \neg R \rightarrow AG^{[t_{max},t_{max}]} \neg P) \mathcal{W} R)$ Example and Known Uses Portable Gas Detector: The Audio alarm must be sounded only if, no more than 1 second before, a gas concentration higher than a threshold has been detected. This property states that the Portable Gas Detector must not have false alarms and that the cause for such an alarm must occur no more than 1 second before. Additional notes It is worth noting that, looking into the past, $t_{max}$ and $t_{min}$ are time distances that start from $T$. In particular, $t_{min}$ is the minimum time distance between $S$ and $T$ and it can be set to zero if no minimum time distance is required between $S$ and $T$. Our version and the version in [3] differ in principle from the one in [1] (e.g., $\neg P \; \mathcal{W} \; S$ for the globally scope). We can say that by dropping the external global $\Box$ they are equivalent.

# Probabilistic version

The Precedence Property Pattern has been proposed by Grunske in [2] and it can be found on ProProST webpage.

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.
3. Pierfrancesco Bellini ; Paolo Nesi ; Davide Rogai Expressing and organizing real-time specification patterns via temporal logics. Journal of Systems and Software 82(2): 183-196 (2009).