Abstract:Interaction systems were proposed and implemented by Sifakis et al. as a model for the design and study of component based systems. We investigate here the property of liveness in interaction systems ...Interaction systems were proposed and implemented by Sifakis et al. as a model for the design and study of component based systems. We investigate here the property of liveness in interaction systems where liveness of an action, a component or a set of components means that the action (component, set of components) will repeatedly participate in every run of the global system. We show that deciding liveness is NP-hard. Then we present a characterization of liveness. Finally, by exploiting local information, we establish a polynomial-time criterion that guarantees liveness. We combine the criterion with the characterization to obtain a test for liveness.Read More