Smart spaces contain a large number of computing devices communicating with each other to perform various high-order tasks. They are governed by predefined policies that users can put according to their preferences. In this paper, we investigate the policy interaction problem beyond the smart home domain. We use a formal method for detecting dynamic conflicts between policies. First, we give an abstract model of the system described with an actor-based language. Then, we identify different kinds of conflicts that may exist among policies in smart home domain. To reduce the complexity of model checking, we use compositional verification as well as data abstraction techniques.