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