# Writing transition relation for deterministic automata

I am not able to figure out how to come up with transition relation for deterministic automata. Below is from 2022 paper where we need to write the transition relation for the deterministic automata.

Is this correct? If not could you please expand and write the transition of the automata shown in the picture?

(from q0)

(s1 & a & s1') v  (s1 & !a & (s0' v s1')) v ((s0 v s1) & !a &(s0' v s1')) & ((s0 v s1) & !a &(s0' v s1'))

Basically I am not able to come up with the transition when a state has variables like (r0,r1). When there is only one variable in the state, I know how to do it. +1 vote

For a deterministic automaton, the next state is determined uniquely by the current state and the current input. Hence, the transition relation can be written as a conjunction of equivalences of the form next(s) <-> phi(s,i) where the next state is determined by the current state s and the current input i. That also holds for a boolean encoding. The automaton above has two states. Let's encode it with a single boolean state variable q that is initially false. The transition relation will then be

next(q) <-> q | !a

Note that either we are already in the state where q holds (and then q does also hold next), or we need input !a to switch to that state.
by (162k points)
selected by
Thank you for the clarification.