# Occurrence Specification Patterns

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