Using branching time temporal logic to synthesize synchronization skeletons
scientific article; zbMATH DE number 3812940