Alphabet-Based Synchronisation is Exponentially Cheaper Antti Valmari and Antti Kervinen
We study the complexity of verification problems in which a preorder
relation between an implementation and a specification is checked,
when the specification is given as a parallel composition of
processes. This problem turns out to be PSPACE or EXPSPACE-complete,
depending on the type of the parallel composition operator that is
used in the construction of the specification. This implies that
confusion with different parallel composition operators may lead to
erroneous complexity claims. We fix one such erroneous result
presented in an earlier publication. We also show that the application
of hiding, renaming or just one interleaving parallel composition
operation to a specification for which the problem is in PSPACE, may
raise the complexity of the problem to EXPSPACE-hard.
|
concur02@fi.muni.cz |