Verifying Communicating Multipushdown Systems

Abstract. Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO chan-nels. We extend the notion of split-width [8] to this setting, improv-ing and simplifying the earlier definition. Split-width, while having the same power of clique-/tree-width, gives a divide-and-conquer technique to prove the bound of a class, thanks to the two basic operations, shuffle and merge, of the split-width algebra. We illustrate this technique on ex-amples. We also obtain simple, uniform and optimal decision procedures for various verification problems parametrised by split-width.