Ndet automata

Question

Problem 5 b August 31,2021

 AE ({q}, ¬q, q' <-> q | p, FGq)

1) Can you please help me how to write the part highlighted translation relation of inner automata? 2) Can you explain why NDet-F called partially defined.

Answer 1

I don't understand your first question, maybe you can make that clearer? For the second question, the answer is found on page 86 of the automaton chapter: An automaton is totally defined if for every state and every input, there is a transition, otherwise, the automaton is partially defined. Partially defined automata have therefore states where they cannot react to one of the inputs since there is no transition for the input.

Comments

I have updated my question 1.
For question 2 - My understanding of partially defined automata is similair to non deterministic automata. Can you please tell in the question diagram which no transition for the input satisfies it as partially defined automata.

---

A partially defined automaton is certainly nondeterministic. The converse is not true, since there are totally defined automata which are also nondeterministic. The automaton in part 5b has no transition for input !a in state {}, and no transition for input a in state {q}. I am still not sure what your first question is, but I may add that we first replace the acceptance condition Fp by an equivalent NDetFG automaton (see page 64 of the chapter) and the nested automata can be flattened as shown o n page 45. Does this help?

---

My question 2 is very clear. Thsnk you.
For question 1 - How to write the transition relation q' <-> q | p for NDetFG

---

I still don't really understand the first question. For writing a transition relation, it does not matter whether the automaton is deterministic or nondeterministic. It is just the case that for deterministic automata, we can use a kind of normal form of equations (Xq <->...) which we cannot use for nondeterministic automata. But we can write any propositional logic formula using the state and input variables and the next-state variables.