## Intent

Applies when a restriction on the minimum number of occurrences is desired.

## LTL Template

## Examples and Known Uses

A robot to enter location $l_1$ at least $3$ times.
The trace `$l_4 \rightarrow l_3 \rightarrow l_2 \rightarrow l_2\rightarrow l_4 \rightarrow ( l_3)^\omega$`

violates the mission requirement since location $1$ is never entered.
The trace `$l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_1 \rightarrow ( l_3)^\omega$`

satisfies the mission requirement.

## Relationships

The LTL formula used to encode Lower Restricted Avoidance constrains the LTL visit pattern by forcing a location to be visited at least X times.

## Occurences

Chen et al. proposed an LTL formula that forces a service to occur at least a number of time, this can be considered as an example of usage of the lower restricted avoidance pattern.

## Büchi Automaton representing accepting sequences of events

where circled states are accepting states and states with an incoming arrow with no source are initial states. The automaton above is deterministic.