{Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach}