Characterizations of locally testable events

Let Σ be a finite alphabet, Σ* the free monoid generated by Σ and |x| the length of x ε Σ*. For any integer k ≥ 0, fk(x)(tk (x)) is x if |x| ≪ k+1, and it is the prefix (suffix) of x of length k, otherwise. Also let mk+1 (x) = {v|x = uvw and |v| = k+1}. For x,y ε Σ* define x ∼k+1y iff fk(x) = fk(y), tk(x) = tk(y) and mk+1(x) = mk+1 (y). The relation ∼k+1 is a congruence of finite index over Σ*. An event E ⊆ Σ*. is (k+1)-testable iff it is a union of congruence classes of ∼k+1. E is locally testable (LT) if it is k+1-testable for some k. (This definition differs from that of [MP] but is equivalent.) We show that the family of LT events is a proper sub-family of star-free events of dot-depth 1. LT events and k-testable events are characterized in terms of (a) restricted star-free expressions based on finite and cofinite events, (b) finite automata accepting these events, (c) semigroups, and (d) structural decomposition of such automata. Algorithms are given for deciding whether a regular event is (a) LT and (b) k+1-testable. Generalized definite events are also characterized.