Occurrence Specification Patterns
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.
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))))
(!P U (!P | (P U (P | (!P U (!P | (P U (P | !P))))))))
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.