Lasso Automaton

Definition

A lasso automaton is an automaton specifically designed to accept pairs $(u,v)\in {\Sigma }^{+}$ that generate a language $u{v}^{\omega }$ . It is often defined as a tuple including two sets of states ($X$ for the spoke, $Y$ for the loop) and transition functions that handle the move from the spoke to the loop.

Transitions

The automaton processes the spoke $u$ using standard transitions in $X$, “switches” to $Y$ non-deterministically (or via specific rules), and then verifies the loop $v$ in $Y$.

See also

Lasso Language