As mentioned in the Q&A session today, that is done as follows: For a deterministic automaton, we can always write down the transition relation as a conjunction of equivalences of the form Xq_i <-> phi_i such that phi_i is a propositional logic formula on the current state and input variables that enumerates all transitions pointing to a state where q_i holds next.
