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).
Left:TS1 Right:TS2

A tutor proposed that the resulting Interleaving Transition System ITS is enter image description here

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?

  • $\begingroup$ 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. $\endgroup$ Oct 21 '15 at 13:12
  • $\begingroup$ @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? $\endgroup$
    – eyeezzi
    Oct 22 '15 at 1:56
  • $\begingroup$ 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. $\endgroup$ 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]|$.

The point is that (together with additional operations like hiding) this allows you to represent a far greater variety of models of interaction.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.