Application of DES theory to verification of software components

Software model checking is typically applied to components of a large systems. The assumption generation is the problem of finding the least restrictive environment in which the components satisfies a given safety property. There is an algorithm for computing the environment for properties given as a regular language. In this paper, we propose a general scheme for computing the assumption even for non-regular properties. Dealing with non-regular languages may fall into undecidability. We show a class of non-regular properties for which the assumption is computable. This result relies on the proposing scheme.