This paper deals with the automatic traffic control of vessels moving through the marine canal traffic system. Dangerous vessel deadlock situations may occur in case of vessels’ irregular moving through the system. To avoid this, the vessel traffic is supervised and controlled by traffic lights. Derived supervisor is maximally permissive (responsible for vessels’ stopping only in the case of dangerous situation and until this situation elapses). This paper shows a formal method of calculating such supervisor by using Petri net. To ensure deadlock free operation of supervisor, the paper proposes finding and controlling critical minimal siphons (specific set of places in the Petri net which are responsible for deadlock). The supervisor is verified using computer simulation.