+1 vote
in * TF "Emb. Sys. and Rob." by (870 points)

1 Answer

+2 votes

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. 
by (15k points)
edited by

Related questions

+2 votes
2 answers
asked Aug 7, 2018 in * TF "Emb. Sys. and Rob." by Pavonlo (280 points)
+1 vote
2 answers
asked Aug 17, 2018 in * TF "Emb. Sys. and Rob." by alogan (870 points)
+2 votes
1 answer
+1 vote
1 answer
Imprint | Privacy Policy
...