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