On the Complexity of Flanked Finite State Automata

TL;DR

This paper introduces Flanked Finite Automata (FFA), a new subclass of nondeterministic automata for prefix-closed languages, which allows efficient verification operations like universality, inclusion, quotient, and inclusion checks.

Contribution

The paper defines FFA and demonstrates their advantageous complexity properties, enabling efficient language operations without powerset construction.

Findings

Universality problem for FFA is solvable in linear time.

Language inclusion for FFA can be checked in polynomial time.

FFA facilitate efficient computation of language quotient and inclusion.

Abstract

We define a new subclass of nondeterministic finite automata for prefix-closed languages called Flanked Finite Automata (FFA). We show that this class enjoys good complexity properties while preserving the succinctness of nondeterministic automata. In particular, we show that the universality problem for FFA is in linear time and that language inclusion can be checked in polynomial time. A useful application of FFA is to provide an efficient way to compute the quotient and inclusion of regular languages without the need to use the powerset construction. These operations are the building blocks of several verification algorithms.