Complexity of expressions allowing concurrency

Abstract

We study some consequences of the formal language approach to modelling software system behavior for the case of asynchronous, concurrent subsystems. We use the formal language shuffle operation to give an "algebraic" definition of semantics for a simple (structured) concurrent programming language and prove that the use of this operation is necessary. Having established this necessity, we investigate other types of behavioral expressions which use the operation and show that the analysis problem for these expressions is either undecidable or intractable. The results provide some limitations, for example, on the path expression method of system behavior analysis. Our lower bound proofs involve the use of synchronization symbols, which seem to be a formal language analogue of semaphores.