# FSM form symbolic representation

I am stuck in forming FSM. This relation is getting too complex to solve because of double <->. Can anyone help please?Consider the following symbolic representation of a FSM: A=(2Vin,2Vout,φI,2Vstate,φR)A=(2Vin,2Vout,φI,2Vstate,φR), where Vin={a}Vin={a}Vout={o}Vout={o}Vstate={p,q}Vstate={p,q}φI=pqφI=p∨qφR=φR=(next(p)->(p&(o<->q)<->next(q)))&a

You can partially evaluate the formula. Note the structure (p' → …) ∧ a. This means that edges only exist with a being true. Also, every state has all possible transitions with variable a being true for successor states where p' is false.

Hence, you can already draw transitions from all states to the half without p, and label the transitions {a}, {a,o}.

Next, we assume that a and p' are true. We then consider the inner formula p ∧ (o ↔ q) ↔ q'. For p being false, the inner biimplication doesn't matter. Just q' needs to be false. So you can add transitions labeled {a} and {a,o} from states without p to the state with p' true, and q' false.

Now we look at the inner biimplication. We assume a, p', p to be true In this case, we need to statisfy (o ↔ q) ↔ q'. If q' is true, the inner biimplication needs to be satisfied; for q' false, the inner bimimplication may not be satisfied. Hence, you add the transitions from all states with p to states with p'. Just be careful with the labels. Add o precisely to the labels of transitions from positive q to positive q' and negative q to negative q'.

Now, we have covered all cases. If you want to do it with care, you can create a partial truth table for a, p, p'.

pp'aφR
falsefalse
falsetruetrue
falsetruetrue¬q'
truetruetrue(o ↔ q) ↔ q'

by (25.6k points)
edited by