# what is a prefix automaton

+1 vote

An automaton with one or more acceptance conditions of the form F(φ) ∧ G(!ψ). This means that it accepts those runs that touch at least one state satisfying φ and never a bad state satisfying ψ for at least one of the acceptance conditions.
by (25.6k points)
edited by
Well, the acceptance condition could also be a disjunction of these pairs, i.e., \/_i (Fφ_i) ∧ (Gψ_i), and it could be also given in the dual form /\_i ((Fφ_i) ⋁ (Gψ_i)). Some people prefer to write the latter as /\_i (G(¬φ_i) ➞ (Gψ_i)) or /\_i (F(¬ψ_i) ➞ (Fφ_i)).
+1 vote
Maybe a little bit more background is worth to be mentioned here. Neither Det-G nor Det-F automata are closed under negation (but both are closed under conjunction and disjunction). The boolean closure, i.e., what you get when you consider all boolean combinations of either Det-G or Det-F or even both leads to prefix automata. That name is not really standard, this class of automata appears in the literature under many names, sometimes also weak Rabin or weak Streett automata.

By definition, Det-Prefix has acceptance condition \/_i (Fφ_i) ∧ (Gψ_i) with finitely many pairs φ_i,ψ_i, and it could be also given in the dual form /\_i ((Fφ_i) ⋁ (Gψ_i)). Some people prefer to write the latter as /\_i (G(¬φ_i) ➞ (Gψ_i)) or /\_i (F(¬ψ_i) ➞ (Fφ_i)). The number of pairs is sometimes called the index of the automaton, and it is known that there are prefix automata having index n+1 that cannot be expressed by any equivalent prefix automaton having index n.

Concerning determinization, NDet-Prefix is more powerful than Det-Prefix, hence, there is no determinization procedure that could transform any NDet-Prefix automaton to an equivalent Det-Prefix automaton. If you want to see an example, simply consider FGa which can be converted to NDet-F, but not to Det-F and neither to Det-Prefix (why not? If so, Det-FG would become equivalent to NDet-Prefix = NDet-FG).

Prefix automata are used when it comes to boolean operations of safety and liveness automata, and sometimes also for the determinization of NDet-F automata (but here you have to be careful and need some special properties since it does not work in general as written above).

Finally, what prefix automata are for Det-G and Det-F, Rabin/Streett automata are for Det-FG and Det-GF.
by (166k points)