Yes, and both rely on Pnueli's temporal logic. But Harel and Lamport apply a similar theory to different domains, neither suggesting the exclusion of the application to the other domain. Lamport offers abstract state machines as a universal mathematical formalism for reasoning about discrete dynamical systems regardless of how they're constructed, while Harel offers concrete state machines for programming safety-critical, hard-realtime embedded systems that are easy for both humans and machines to analyze.