Concurrency and Deadlock

We are usually only interested in concurrent processes that eventually interact. If 2 procs have the same alphabet (of events) and run in ;SPM_quot;lockstep;SPM_quot;, we have simultaneous engaging by each process. i.e. each is concurrently behaving as if it was on its own. In other words, in our example where the games player and GAME are processes, if we consider the events in their alphabet, InCoin and OutCome, they (in some sense) engage simultaneously in each. This is written:

#equation1089#

At the top level of a concurrent system, only the interactions are interesting.