Mappings for bounds other than two can be constructed relatively
simply from the given mappings. For QREs one simply defines
k appropriately. For LTL and CTL we simply add
additional copies of the nested until structures,
for example in LTL 3-bounded global existence is:
(!P W (P W (!P W (P W (!P W (P W []!P))))))
(where the nested 2-bounded version is in bold).
If the weak-until operator is not available directly one can
simply expand the mapping using the definition given above. For
example, the 2-bounded global LTL mapping:
(!P W (P W (!P W (P W []!P))))
would become:
(!P U ([]!P | (P U ([]P | (!P U ([]!P | (P U ([]P | []!P))))))))
Note that response chain patterns are different than bounded existence in two ways: response chains require the responding sequence to be of the designated length (whereas here we only bound a sequences length), and the notion of an instance of a state/event differs between the two. In particular, a stuttered instance (i.e., in consecutive states on a path) counts as multiple instances with the chain whereas it is a single instance with bounded existence.
This is an Occurrence pattern.