Based on the system architecture described above, we can readily deduce the state transition function for the Bitcoin finite state machine model like below.
Let the initial state of a user address A be represented as Si=State(A), where State() is a query function that returns the transaction history associated with that user.
A conditional transaction initiated by user A can be abstracted as a state transition function Ti= UTXO_OP().
The verification of computational integrity is represented as Vi = Verify(Si+1, Si, Ti).
Therefore, the complete global state transition function for A can be abstracted as: