Deriving Compositionally Deadlock-Free Components over Synchronous Automata Compositions
Nina Vladimirovna Yevtushenko, Khaled El‐Fakih, Tiziano Villa, Jie-Hong Roland Jiang · The Computer Journal · 2014
The composition of two arbitrary component automata can have deadlock states. A method is proposed to minimally reduce a component automaton such that the resulting composition with the other automaton is deadlock-free. The method is applied to deriving compositionally deadlock-free solutions of automata equations over the synchronous composition.