Slicing communicating automata specifications: polynomial algorithms for model reduction