Deadlock analysis for deterministic finite state automata using affine linear models

Deterministic finite state automata can be modelled within the framework of the boolean differential calculus. One way back to conventional arithmetics leads to multi-linear discrete models of the automata. There the escrow issue is that even if state feedback is applied, in general the models still remain nonlinear. The method presented here is to embed the nonlinear state space within a linear state space of higher dimension, which provides a remedy for the problem of this kind of nonlinearity. As a result the system equations of the fed back automaton become affine linear in the state variables. The latter outcome grants a new way of deadlock analysis with which a method of deadlock prevention via state feedback is proposed.