Intent
To describe a portion of a system's execution that contains at most a specified number of instances of a designated state transition or event.
Example Mappings
Examples and Known Uses
Bounded overtaking properties can naturally be expressed using instances of this pattern. For example, if we wish to say that process 1 can enter its critical region at most twice while process 2 is waiting to enter its region we would use a between scope (delimited by process 2 entering and exiting its waiting region) with 2-bounded existence for process 1 entering its critical region.
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))))))))
Relationships
This pattern is related to existence and chains. Note that this pattern does not require the occurrence of any number of instances of the given states/events (rather it bounds the number of instances). Single instances can be required with existence patterns. Multiple instances can be required with a slight variant to the above mappings.
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.