In this paper, we consider the discrete event systems (DES) modeled via a state - space representation. The control objective is the avoidance of a given set of states. We achieve this goal by verifying that certain predicates, specified in terms of states, are always false. We model the DES involved in physical systems with a class of controlled state machines, respectively the formalism of the controlled Petri nets. A model of a railway shunting system illustrates the theoretical approach.