Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

925 questions

1k answers

1.4k comments

441 users

+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 (143k points)
edited by

Related questions

Imprint | Privacy Policy
...