Verifying Communicating Multi-pushdown Systems

Aiswarya Cyriac (1, 2) , Paul Gastin (1, 2) , K. Narayan Kumar (3)

1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
3 Chennai Mathematical Institute [Inde]

Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. Hence their verification problems are undecidable in general. The behaviours of these systems can be represented as directed graphs, which subsume both Message Sequence Charts and nested words. We extend the notion of split-width to these graphs, defining a simple algebra to compose/decompose these behaviours using two natural operations: shuffle and merge. We obtain simple, uniform and optimal decision procedures for various verification problems parametrized by split-width, ranging from reachability to model-checking against MSO, PDL and Temporal Logics.

Mots clés: Under-approximate verification; Split-width; Concurrent systems; Model-checking; Propositional Dynamic Logic; Monadic Second-Order Logic

Domaines: Logique en informatique [cs.LO]

Aiswarya Cyriac, Paul Gastin, K. Narayan Kumar. Verifying Communicating Multi-pushdown Systems. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA'14), 2014, Sydney, Australia. pp.1-17. ⟨hal-00943690⟩