On Checking Controllability of Specification Languages for DES

The paper provides further development of the authors’ original approach to the representation and properties checking of discrete event systems. The approach suggested is based on the automated inference in the calculus of positively constructed formulas (PCF). Discrete event system is supposed to be modeled in the form of finite automata within the framework of Ramage-Wonham supervisory control theory. It is shown how constructive inference helps to build the product of two finite automata which results in the automaton with accessible states only. Based on the nonmonotonic logical inference of PCF, a new method is presented for checking the controllability of formal languages describing specifications on the functioning of discrete event systems.