|Résumé||We consider systems of concurrent boolean programs equipped with several data structures. The data structures can be unbounded stacks or unbounded queues. Each data structure allows write access to only one process (call it writer), and read access to only one (possibly different) process (call it reader). A stack whose writer and reader are the same corresponds to an unbounded local stack of the writer. A queue serves as an unbounded reliable FIFO channel from its writer to its reader. As these systems are very powerful, they render most verification problems undecidable.
We introduce a parameter called split-width for its under-approximate verification. Split-width is a notion similar to tree-width, but more handy for the systems we consider. Restricting to bounded split-width behaviors gives an EXPTIME decision procedure for model checking these systems against temporal logics and propositional dynamic logics, and a decision procedure for model checking against MSO. We show that split-width can capture several interesting and relaxed scheduling policies.
This is a joint work with Paul Gastin and K. Narayan Kumar.