A state-based framework for supervisory control synthesis and verification