Thread automaton

In automata theory, the thread automaton (plural: automata) is an extended type of finite-state automata that recognizes a mildly context-sensitive language class above the tree-adjoining languages. 
Formal definition.
A thread automaton consists of
A path "u"1..."u""n" ∈ "U"* is a string of path components "u""i" ∈ "U"; "n" may be 0, with the empty path denoted by ε.
A thread has the form "u"1..."u""n":"A", where "u"1..."u""n" ∈ "U"* is a path, and "A" ∈ "N" is a state.
A thread store "S" is a finite set of threads, viewed as a partial function from "U"* to "N", such that "dom"("S") is closed by prefix.
A thread automaton configuration is a triple ‹"l","p","S"›, where "l" denotes the current position in the input string, "p" is the active thread, and "S" is a thread store containing "p".
The initial configuration is ‹0,ε,{ε:"A""S"}›.
The final configuration is ‹"n","u",{ε:"A""S","u":"A""F"}›, where "n" is the length of the input string and "u" abbreviates δ("A""S").
A transition in the set Θ may have one of the following forms, and changes the current automaton configuration in the following way:
One may prove that δ("B")="u" for POP and SPOP transitions, and δ("C")=⊥ for SPUSH transitions.
An input string is accepted by the automaton if there is a sequence of transitions changing the initial into the final configuration.