This model of a combined state machine works but it's not so nice. Why? It's not compositional. We don't have the property that
or even that
Moreover, we can't say
That is, a property, Inv, that holds for both P and Q does not necessarily hold for its composition.
A property that does hold of P || Q is a global invariant. It's called ``global'' because it's a predicate that can involve, in general, the program counters of the individual processes as well as the global variables.
Nevertheless, it is a common model for a programming languages that support a shared memory model of concurrency. For example, any language that has a Threads interface such as C-Threads, Modula-2++, Modula-3, or any operating system that supports lightweight threads of control (e.g., Mach) is based on this model.
People also design systems with this model in mind. For example, Linda's tuple space is based on a so-called ``blackboard'' model, which is a shared resource; most transactional systems assume either physically centralized database or a globally-viewed distributed database; file systems like Andrew give the illusion of shared files and directories; user interfaces like X windows need to manage shared real estate. So, there are real-world systems that are very naturally modeled as shared memory-systems.