First converting it to a NDet-FG that is then determinized to a Det-FG automaton using the breakpoint construction. The former is done by replacing F and G constraints by equivalent FG constraints, and then applying boolean closures of conjunction and disjunction of the FG constraints. Here is an example for the first steps to transform the prefix automaton A∃(Q,I,R,(Gφ)⋀(Fψ)) with symbolic representations:
- A∃(Q,I,R,(Gφ)⋀(Fψ))
- A∃(Q,I,R,A∃({p},p,p′↔p∧φ,FGp) ⋀ A∃({q},¬q,q′↔q∨ψ,FGq))
- A∃(Q,I,R, A∃({p,q},p∧¬q,(p′↔p∧φ)∧(q′↔q∨ψ),(FGp)⋀(FGq)))
- A∃(Q∪{p,q},I∧p∧¬q,R∧(p′↔p∧φ)∧(q′↔q∨ψ),(FGp)⋀(FGq))
- A∃(Q∪{p,q},I∧p∧¬q,R∧(p′↔p∧φ)∧(q′↔q∨ψ),FG(p⋀q))
The latter is not (maybe) a NDet-FG automaton so that the breakpoint construction will do the final transformation to Det-FG.
