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).

Home page

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License