Verifying Communicating Multi-pushdown Systems via Split-Width
2014 (English)In: Automated Technology for Verification and Analysis, 2014, 1-17 p.Conference paper (Refereed)
Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. We extend the notion of split-width  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.
Place, publisher, year, edition, pages
2014. 1-17 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8837
IdentifiersURN: urn:nbn:se:uu:diva-240882DOI: 10.1007/978-3-319-11936-6_1ISI: 000345585700005ISBN: 978-3-319-11936-6ISBN: 978-3-319-11935-9OAI: oai:DiVA.org:uu-240882DiVA: diva2:777668
12th International Symposium on Automated Technology for Verification and Analysis (ATVA), NOV 03-07, 2014, Sydney, AUSTRALIA