A nondeterministic finite state machine whose states are labeled with boolean variables, which are the evaluations of expressions in that state. It may be extended with fairness constraints.