Specifying and Verifying Partial Order Properties Using Template MSCs

Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the style of LSCs and Triggered MSCs. We enrich MSCs with the possibility of using gaps (template MSC), and show their ex-pressivity. This formalism also allows to express logical formulas. We analyze the model-checking problem, whose complexity is linear in the size of the system, and ranges from PTIME to EXPSPACE in the size of the template formula.