Design and synthesis of synchronization skeletons using branching time temporal logic