Liveness in Interaction Systems

Interaction systems are a formal model for component-based systems. It has been shown that in this formalism the question whether a component is live is NP-hard. Therefore it is desirable to find sufficient criteria that can be checked in polynomial time. In this report we present the proofs of propositions concerning such criteria that have been given in previous work. We also present the proof of a characterization of liveness that has also been introduced previously