Constrained Response Property Pattern

# Untimed version

 Pattern Name and Classification Response: Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response S eventually holds without $Z_S$ [holding] in between. Pattern Intent To describe cause-effect relationships between a pair of events/states. An occurrence of the first, the cause $P$, must be followed by an occurrence of the second, the effect $S$. Temporal Logic Mappings LTL Globally: $\Box \; (P \;\rightarrow \; \neg Z_S \; \mathcal{U} \; S)$ Before R: $\Diamond \; R \;\rightarrow \; (P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U} \; (S \wedge \neg R))) \; \mathcal{U} \; R$ After Q: $\Box(Q \;\rightarrow \; \Box(P \;\rightarrow \; \neg Z_S \; \mathcal{U} \; S))$ Between Q and R: $\Box((Q \;\wedge \Box \neg R \;\wedge \Diamond \; R) \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \wedge \neg Z_S\mathcal{U} \; (S \;\wedge \neg R))) \; \mathcal{U} \; R)$ After Q until R: $\Box(Q \;\wedge \Box \neg R \;\rightarrow \; ((P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U} \; (S \;\wedge \neg R))) \; \mathcal{W} \; R)$ CTL Globally: $AG(P \;\rightarrow \; A[!Z_S \; \mathcal{U} (S)])$ Before R: $A[(P \;\rightarrow \; (A[!R \& !Z_S\; \mathcal{U} \; (S \wedge \neg R)]) \vee AG(!R)) \; \mathcal{W} \; R]$ After Q: $A[!Q \; \mathcal{W} \; (Q \wedge AG(P \;\rightarrow \; A[!Z_S\mathcal{U}(S)])]$ Between Q and R: $AG(Q \wedge AG !R \;\rightarrow \; A[((P \;\rightarrow \; A[!R \& !Z_S\; \mathcal{U} \; (S \wedge !R)]) \vee AG(!R)) \; \mathcal{W} \; R])$ After Q until R: $AG(Q \wedge \Box !R \;\rightarrow \; A[(P \;\rightarrow \; A[!R \& !Z_S\; \mathcal{U} \; (S \wedge !R)]) \; \mathcal{W} \; R])$ Additional notes The Response Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on the following webpage: Response Property Pattern .

# Time-constrained version

 Pattern Name and Classification Time-constrained Response: Real-time Order Specification Pattern Structured English Specification Scope, if P [has occurred], then in response S eventually holds without $Z_S$ [holding] in between and within [ Time(0)]. Pattern Intent To describe cause-effect relationships between a pair of events/states. An occurrence of the first, the cause $P$, must be followed by an occurrence of the second, the effect $S$ without $Z_S$ holding and within a timebound [t_1,t_2]. Temporal Logic Mappings MTL Globally: $\Box \; (P \;\rightarrow \; \neg Z_S \; \mathcal{U}^{[ t_1, t_2]} \; S)$ Before R: $\Diamond^{[ t_1, \infty)} \; R \;\rightarrow \; (P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R))) \; \mathcal{U} \; R$ After Q: $\Box(Q \;\rightarrow \; \Box(P \;\rightarrow \; \neg Z_S \; \mathcal{U}^{[ t_1, t_2]} \; S))$ Between Q and R: $\Box((Q \;\wedge \Box^{[ 0, t_1]}\neg R \;\wedge \Diamond^{[ t_1, \infty)} \; R) \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \wedge \neg Z_S\mathcal{U}^{[ t_1, t_2]} \; (S \;\wedge \neg R))) \; \mathcal{U} \; R)$ After Q until R: $\Box(Q \;\wedge \Box^{[ 0, t_1]} \neg R \;\rightarrow \; ((P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \;\wedge \neg R))) \; \mathcal{W} \; R)$ TCTL Globally: $AG(P \;\rightarrow \; A[\neg Z_S \; \mathcal{U}^{[ t_1, t_2]} (S)])$ Before R: $A[(P \;\rightarrow \; (A[\neg R \& \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R)]) \vee AG(\neg R)) \; \mathcal{W} \; R]$ After Q: $A[\neg Q \; \mathcal{W} \; (Q \wedge AG(P \;\rightarrow \; \neg Z_S \; A[\mathcal{U}^{[ t_1, t_2]}(S)])]$ Between Q and R: $AG(Q \wedge AG^{[0, t_1]}\neg R \;\rightarrow \; A[((P \;\rightarrow \; A[\neg R \& \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R)]) \vee AG(\neg R)) \; \mathcal{W} \; R])$ After Q until R: $AG(Q \wedge \Box^{[0, t_1]}\neg R \;\rightarrow \; A[(P \;\rightarrow \; A[\neg R \& \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R)]) \; \mathcal{W} \; R])$ Additional notes The Time-constrained Response Property Pattern has been proposed by Cheng in [2], proposed as Bounded Response .

# Probabilistic version

The Response Property Pattern has been proposed by Grunske in [3] and it can be found on the following webpage: Probabilistic Response 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. Lars Grunske, Specification patterns for probabilistic quality properties. ICSE 2008. pp. 31-40.