Modelling using propositions, syntax and standards
Generally you have:


Some boolean variables that collectively represent the current state, say $s,t,u$.
Some boolean variables that collectively represents the inputs, say $i,j,k$.  For instance, you might have one variable per sensor (assuming each sensor returns a boolean value).
Some boolean variables that collectively represents the inputs, say $o,p,q$.  For instance, you might have one variable per actuator (assuming each actuator can be either on or off).
Some boolean variables that collectively represent the next state.  You could give them a different name (e.g., $x,y,z$), but often, to help us remember the relationship to the variables for the current state, we used primed versions of the variables for the current state.  So, the next state might be represented by $s',t',u'$.


Now, we introduce a predicate $\Psi(s,t,u,i,j,k,o,p,q,s',t',u')$ to represent the transition relation.  The idea is that if this is true, it means the following: if you're in state $s,t,u$ and you receive inputs $i,j,k$, then you output $o,p,q$ AND transition to the state $s',t',u'$.  You can use boolean logic to express the predicate $\Psi(s,t,u,i,j,k,o,p,q,s',t',u')$ as a boolean formula, using AND, NOT, OR, implication, etc.

Then you also need to describe the initial state of the system.  For instance, it might be $(s,t,u)=(T,F,T)$.

As you can see, the notation can get a bit much.  Often we collect all the variables associated with the current state into a vector $s$ of variables, $s=(s_1,\dots,s_k)$ where the state is $k$ bits (it is represented by $k$ boolean variables), and collect all of the variables associated with the input into a vector $i$ of variables, $i=(i_1,\dots,i_m)$; you similarly collect all the output variables into a vector $o=(o_1,\dots)$; and the next state is given by a vector $s'=(s'_1,\dots,s'_k)$ represents the next state.

As a generalization, you can consider variables that have more than two possible values (they aren't restricted to be booleans).  Booleans are convenient for digital logic implementation, but more general variables can enable a specification that is easier to think about and understand.

So, basically, yes, this is compatible with the kind of approach you were showing.