Compositionality and Locality for Improving Model Checking in the Selective Mu-Calculus