Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction