Quotient automaton

In computer science, in particular in language theory">formal language">language theory, a quotient automaton can be obtained from a given nondeterministic [finite automaton] by joining some of its states. The quotient recognizes a superset of the given automaton; in some cases, handled by the Myhill–Nerode theorem, both languages are equal.

Formal definition

A finite automaton is a quintuple A = ⟨Σ, S, s₀, δ, S_f⟩, where:Σ is the input alphabet,S is a finite, non-empty set of states,s₀ is the initial state, an element of S,δ is the state-transition relation: δ ⊆ S × Σ × S, andS_f is the set of final states, a subset of S.
A string a₁...a_n ∈ Σ^* is recognized by A if there exist states s₁,..., s_n ∈ S such that ⟨s_i-1,a_i,s_i⟩ ∈ δ for i=1,...,n, and s_n ∈ S_f. The set of all strings recognized by A is called the language recognized by A; it is denoted as L.
For an equivalence relation ≈ on the set S of A’s states, the quotient automaton A/_≈ = ⟨Σ, S/_≈,, δ/_≈, S_f/_≈⟩ is defined by

the input alphabet Σ being the same as that of A,
the state set S/_≈ being the set of all equivalence classes of states from S,
the start state being the equivalence class of A’s start state,
the state-transition relation δ/_≈ being defined by δ/_≈ if δ for some s ∈ and t ∈, and
the set of final states S_f/_≈ being the set of all equivalence classes of final states from S_f.

The process of computing A/_≈ is also called factoring A by ≈.

Example

	Automaton diagram	Recognized language	Is the quotient of	-	-
A by	B by	C by	-	-	-
A:		1+10+100
B:		1^+1^0+1^*00	a≈b
C:		1^0^	a≈b, c≈d	c≈d
D:		^*	a≈b≈c≈d	a≈c≈d	a≈c

For example, the automaton A shown in the first row of the table is formally defined by Σ^A =,S^A =,s = a,δ^A =, andS =.
It recognizes the finite set of strings ; this set can also be denoted by the regular expression "1+10+100".
The relation =, more briefly denoted as a≈b,c≈d, is an equivalence relation on the set of automaton A’s states.
Building the quotient of A by that relation results in automaton C in the third table row; it is formally defined by Σ^C =,S^C =,s = a,δ^C =, andS =.
It recognizes the finite set of all strings composed of arbitrarily many 1s, followed by arbitrarily many 0s, i.e. ; this set can also be denoted by the regular expression "1^*0^*".
Informally, C can be thought of resulting from A by glueing state onto state b, and glueing state c onto state d.
The table shows some more quotient relations, such as B = A/_a≈b, and D = C/_a≈c.

Properties

For every automaton A and every equivalence relation ≈ on its states set, L is a superset of L.
Given a finite automaton A over some alphabet Σ, an equivalence relation ≈ can be defined on Σ^* by x ≈ y if ∀ z ∈ Σ^*: xz ∈ L ↔ yz ∈ L. By the Myhill–Nerode theorem, A/_≈ is a deterministic automaton that recognizes the same language as A. As a consequence, the quotient of A by every refinement of ≈ also recognizes the same language as A.