Font Size: 

In the framework of supervisory control theory (SCT) for discrete event systems (DES), there is an essential problem of checking formal languages for nonconflict. This problem usually arises if decentralized control is implemented. In this case, system behavior under each local supervisor`s control is described by the formal language generated by finite automata. These languages must be nonconflicting to not prevent the system from achieving the desired behavior. We present an algorithm for checking if the languages generated by local supervisors conflict, based on the automatic theorem proving method in the calculus of positively constructed formulas (PCFs). We use the fact that to check languages for conflict it is enough to check if the parallel composition of generating them automata is blocking. A new way of representing finite automata as PCFs is proposed. New formalization is more compact than the formalization proposed earlier and provides more opportunities for setting up logical inference search strategies. Using this formalization, a new method has been developed for constructing a parallel composition of finite automata, and, as a result, a composition of the languages they generate. The parallel composition is then examined to be nonblocking. The advantage of the method is the fact that the parallel composition resulting from the automatic logical inference does not have inaccessible states, so there is no need to use the trim operation on the output automaton.