To build a transition system from a sequential circuit, in general, one needs to define three components:
the states of the transition system, which are all possible combinations of
values of your inputs and registers in the circuit
transitions between states in the transition system, which result from the functions that determine the output and the registers (according to used logical circuits and wire connections)
labels for states in the transition system, which consist of all variables and registers that are evaluated true given the valuations in the circuit
As per the (contrived) circuit in C2, the states reflect only the possible values of the single register. In turn, the function of the output equals to the register (Y2=R3
), while the current value of the register is the negation of its previous value. This should give you enough insights to build the transition system.
The circuit given in C1 is indeed more convoluted, but it can be decomposed into functions on how values (for the registers and the output Y1
) change, which then can be used to derive possible transitions in the system. (This is done with respect to possible changes of the input X
.) For example, Y1 = R1 && R2
and the form for the value of R1
is R1 = (X AND ...) OR (... AND ...)
, while the missing values ...
can be traced down according to the wire connections of the circuit.
More details on modelling sequential circuits as transition systems can be found in [1].
[1] Baier, Christel, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of model checking. MIT press, 2008.