Question

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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top