## Intent

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

## LTL Template

$\mathcal{F} (\underbrace{l_1 \wedge \mathcal{X} (\mathcal{F}(l_1 \wedge \ldots \mathcal{X} (\mathcal{F}(l_1)}_\text{n}))))$, where $l_1 \in L$

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

## CTL Template

$\forall \mathcal{F} (\underbrace{l_1 \wedge \forall \mathcal{X} (\forall \mathcal{F}(l_1 \wedge \ldots \forall \mathcal{X} (\forall \mathcal{F}(l_1)}_\text{n}))))$, where $l_1 \in L$