Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. We extend the notion of split-width [8] to this setting, improving 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 examples. We also obtain simple, uniform and optimal decision procedures for various verification problems parametrised by split-width.
CITATION STYLE
Aiswarya, C., Gastin, P., & Narayan Kumar, K. (2014). Verifying communicating multi-pushdown systems via split-width. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 1–17). Springer Verlag. https://doi.org/10.1007/978-3-319-11936-6_1
Mendeley helps you to discover research relevant for your work.