Bounded Response |
INTENTION |
This pattern is applicable if one phenomenon, represented by ,
always
reacts on another phenomenon, represented by ,
with a maximal time
delay . |
SIGNATURE |
,
,
,
![$\mathcal{V}^{\mathit{ti}} = \{\tau\}$](img7.gif) |
FORMAL |
![$\square( \varphi \rightarrow \lozenge_{\le \tau} \psi)$](img8.gif) |
NATURAL LANGUAGE |
Whenever
holds, then eventually within the next
time
units,
is true. |
Examples |
EXAMPLE 1 |
|
FORMAL |
![$\square( [\mathit{malDetMach}] \rightarrow \lozenge_{\le 11}
\mathit{userInformed})$](img9.gif) |
|
NATURAL
LANGUAGE |
Whenever the machine starts assuming that there is a malfunction the user
is informed about this within the next 11 time units. |
Theorem Part |
THEOREM SIGNATURE |
,
,
,
![$\mathcal{V}^{\mathit{ti}} = \{\tau_1, \tau_2\}$](img11.gif) |
THEOREM 1 Transitivity |
|
FORMAL |
![$\rightarrow \square( \varphi_1 \rightarrow \lozenge_{\le \tau_1+\tau_2} \varphi_3)$](img13.gif) |
|
EXPLANATION |
This theorem expresses the transitivity of this pattern. |
THEOREM 2 Conclusion
Distributivity over ![$\wedge$](img14.gif) |
|
FORMAL |
![$\leftrightarrow \square( \varphi_1 \rightarrow \lozenge_{\le \tau_1}
(\psi_1 \wedge \psi_2))$](img16.gif) |
|
EXPLANATION |
This theorem expresses the distributivity over
of the conclusions of two
instantiations of this pattern. |