A method to verify the controllability of language specifications in Petri nets based on basis marking analysis

In this paper we propose an effective method based on basis marking analysis to verify the controllability of a given language specification in Petri nets. We compute the product, i.e., the concurrent composition, of the plant and of the specification nets and enumerate a subset of its reachable states, called basis markings. Each of these basis markings can be classified as controllable or uncontrollable by solving an integer programming problem. We show that the specification is controllable if and only if no basis marking is uncontrollable. The method can lead to practically efficient verification because it does not require an exhaustive enumeration of the state space.