L# for DFAs. - Frits W. Vaandrager; Martijn Sanders (Principles of Verification (3), 2024)