This thesis is concerned with the use of formal methods towards automatic verification of distributed message passing systems with a fixed finite number of agents. Main concentration is on developing logics to reason about ...