# The Interleaved Transition System for 2 Independent and Concurrent Transition Systems

This question is about Model Checking for Software Formal Verification
How do you model the joint behavior of 2 independent and concurrent transition systems?

Specifically, given the two independent and concurrent Transition Systems below; TS1 and TS2 (left to right).

A tutor proposed that the resulting Interleaving Transition System ITS is

I understand how all the shown states and transitions of this ITS were gotten, however, why is there no transition from state (l1,q1) to (l3,q2)--as would be expected if both TS1 and TS2 transitioned on action a?

• The definition of the interleaving operator (as opposed to e.g. the interface parallel operator in CSP) is that each component can take $a$- or $b$-transitions on its own - there is no synchronization. – Klaus Draeger Oct 21 '15 at 13:12
• @KlausDraeger, thanks for your reply; I think I get it now: the interleaving operator is not synchronized by definition. In that case, can we say that the interleaving operator does not model the joint behavior of the two systems--since it does not account for synchronization? – eyeezzi Oct 22 '15 at 1:56
• Only if you assume that systems are supposed to synchronize on all shared symbols. The point of having interleaving (and, as in CSP, parametrizing the parallel composition operator with a set of symbols on which to synchronize) is to allow you to represent a greater variety of models of interaction. – Klaus Draeger Oct 22 '15 at 8:52

By definition, the interleaving operator is not synchronized, so any transition in $TS1\ |||\ TS2$ corresponds to a transition in a single component while the other one remains in whatever state it is.
More generally, in process algebras like CSP, the parallel composition operator $||$ can be parameterized with a set of symbols on which to synchronize - for example, you could consider $TS1\ |[\{a\}]|\ TS2$, which has the same states and $b$-transitions as $TS1\ |||\ TS2$, but only two (synchronized) $a$-transitions $(l_1,q_1)\to(l_3,q_2)$ and $(l_2,q_1)\to(l_1,q_2)$. In particular, $|||$ is the special case $|[\emptyset]|$.