A logic for modular descriptions of asynchronous and synchronized concurrent systems