Is there formal way to write state transition? I know how to usually draw a state diagram. I'm looking for a formal way to write it. My project is that I'm supposed to make a formal model of physical hardware. I have sketched a state diagram as below and I want to write it with formal notation.
One should first choose between transition relation and transition function. If transitions are not labeled and $Q$ is the set of states, then the transition relation is a subset of $Q \times Q$, while the transition function maps $Q$ to $2^Q$ (the powerset of $Q$).
If the transitions are labeled with elements of $\Sigma$, then the transition relation is a subset of $Q \times \Sigma \times Q$, while the transition function maps $Q \times \Sigma$ to $2^Q$.
If the transition system is deterministic and complete, then the transition function can be taken to map $Q$ (or $Q \times \Sigma$) to $Q$.
For example, to say that there are transitions labeled $\sigma_1$ from $q_1$ to $q_2$ and $q_3$, we would write
$$ \{(q_1,\sigma_1,q_2),(q_1,\sigma_1,q_3)\} \subseteq \rho $$ or $$ \{q_2, q_3\} \subseteq \delta(q_1,\sigma_1) \enspace, $$
where $\rho$ is the transition relation and $\delta$ is the transition function. It is also possible to adopt more compact notation and denote by something like $q_1 \stackrel{\sigma_1}{\rightarrow} q_2$ the existence of a transition from $q_1$ to $q_2$ labeled $\sigma_1$.