Safe Realizability of High-Level Message Sequence Charts Markus Lohrey
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.
|
concur02@fi.muni.cz |