Liveness enforcing in closed AGV systems with dynamic routing

The liveness of a closed AGV system is understood as the constant potential of each vehicle to attain any given zone in the guide path network. Based on the DES model of AGVS and the liveness condition proposed in our earlier work, we conduct a further analysis of the system behavior. The result is a general, algorithmically defined supervisor for AGVS, given in the form of the pseudo-code of a recursive parametric function. The parameter is a function that can implement various selection algorithms, and in combination with the general supervisor defines a class of particular, directly applicable supervisors of various permissiveness level. The correctness of the provided control is formally proved.