We propose a logical formalism for the supervisory control
specifications where the maximal permissiveness is explicitly
handled, independently of the plant. The approach relies on a modal
logic with quantified propositions and additionally provides a
powerful machinery for decision and synthesis procedures.