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

alt text

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$