Portal de Periódicos da CAPES

Alphabet-Based Synchronisation is Exponentially Cheaper

2002; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-45694-5_12

1611-3349

Antti Valmari, Antti Kervinen,

Cellular Automata and Applications

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.