Résumé de séminaire

Résumé :

Hierarchical Message Sequence Charts are a well-established formalism to specify scenarios of communications in telecommunication protocols. Normalized by the ITU (International Telecommunication Union), they are frequently used at an early stage of the design. Unfortunately, many related decision problems were recently shown to be undecidable, in particular w.r.t. model checking. In order to deal with possibly unbounded specifications, we focus on star-connected HMSCs. We relate this subclass with recognizability and MSO-definability by means of a new connection with Mazurkiewicz traces. Our main result is that we can check effectively whether a star-connected HMSC is realizable by a finite system of communicating automata with possibly unbounded channels.

Références :

Page web personnelle : http://www.cmi.univ-mrs.fr/~morin/

Groupe MOVE : http://www.cmi.univ-mrs.fr/~amadio/ModVer/modver.html