Safe Realizability of High-Level Message Sequence Charts
We study the notion of safe realizability for high-level message sequence charts (HMSCs), which was introduced by Alur et al. We prove that safe realizability is EXPSPACE-complete for bounded HMSCs but undecidable for the class of all HMSCs. This solves two open problems from Alur et al. Moreover we prove that safe realizability is also EXPSPACE-complete for the larger class of transition-connected HMSCs.