The Use of language projection for compositional verification of discrete event systems

This paper proposes the use of abstraction by language projection to improve the performance of compositional verification to prove or disprove that a large system of composed finite-state machines satisfies a given safety property. Algorithms are presented for the automatic verification of language inclusion and controllability for discrete event systems, and are applied to a set realistic industrial examples. The experimental results suggest that the method can improve performance considerably, particularly in cases where previous methods of compositional verification fail because a large number of automata need to be considered.