Interaction in Concurrent Systems

This dissertation is concerned with the theoretical analysis of component-based models for concurrent systems. We focus on interaction systems, which were introduced by Sifakis et al. in 2003. Centered around interaction systems, we also cover Minsky machines, Petri nets and the Linda calculus and establish relations between the models by giving translations from one to the other. Thus, we gain an insight concerning the expressiveness of the models and learn, given a system described in one syntax, how to simulate it in another. Additionally, these translations allow us to deduce complexity and undecidability results. Namely, we show that the questions whether a LinCa process terminates or diverges under a maximum progress semantics are undecidable. We also prove that the problems of reachability, progress, local and global deadlock and availability are PSPACE-complete in interaction systems. This complexity-theoretic classification serves as a motivation for the sufficient condition approach that is presented in the second half of this work: We present a generic approach to prove properties for component-based systems that allow for decomposition into subsystems. To avoid the problem of state space explosion, we consider overlapping projections and thus compute over-approximations of the reachable global state space. We enhance the quality of these over-approximations by a technique we call Cross-Checking. Based on the enhanced over-approximations, we may then prove properties of the global system in polynomial time. We demonstrate our ideas by means of interaction systems and for the property of local deadlock