On Depth-bounded Message Passing Systems

We explore the border between decidability and undecidability of verification problems related to message passing systems that admit unbounded creation of threads and name mobility. Inspired by use cases in real-life programs we introduce the notion of depth-bounded message passing systems. A configuration of a message passing system can be represented as a graph. In a depth-bounded system the length of the longest acyclic path in each reachable configuration is bounded by a constant. While the general reachability problem for depth-bounded systems is undecidable, we prove that control reachability is decidable. In our decidability proof we show that depth-bounded systems are well-structured transition systems to which a forward algorithm for the covering problem can be applied.