Control-Flow Modeling with DECLARE: Behavioral Properties, Computational Complexity, and Tools