A temporal logic approach to specify and to prove properties of finite state concurrent systems