VRS Exam 2019.02. Problem 6c.

Question

Hello all,

Can someone help me with the procedure to draw the automata from the formula in the screenshot?

Thanks in advance.

Answer 1

You just have to determine the satisfying assignments of the transition relation. Why not using the teaching tool https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html with the following inputs to double-check your result?

    state variables      : p;q    
    input variables      : a 
    initial states       : !p&q
    transition relation  : (p -> a & next(p)) & !b & q & next(q)
    state set            : false