| 
  
     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  |