Paper Details

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.