Finite state machines and deadlocks

Question

This is my problem

I know traces of two state machines that are deadlock free.

I want to know with the traces (I dont know estructure) , if the composition is deadlock free.

Any theorem to know is this is possible to know?

Answer 1

If you are indeed dealing with composition (run machine A with initial parameters, then machine B using final parameters of A as initial parameters), then a deadlock in the composition would necessarily happen either in A or in B.

It cannot happen in A (because then, it would also happen if B was not present), and it cannot happen in B (because then, it would also happen if A was not present and you used those same initial parameters for B). Therefore, based on the initial assumptions that A and B are deadlock-free, so is their composition.