Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism

We define a new model called O-PRS that extends the Process Rewrite Systems formalism with a new associative operator, “⦶”, that allows to model parallel composition while keeping the order between parallel processes. Indeed, sometimes, it is important to remember the order between the parallel processes. The reachability problem of O-PRS being undecidable, we develop tree automata techniques allowing to build polynomial finite representations of (1) the exact reachable configurations in O-PRS modulo various equivalences that omit the associativity of “⦶”, and (2) underapproximations of the reachable configurations if the associativity of “⦶” is considered. We show that these underapproximations are exact if the number of communications between ordered parallel processes is bounded. We implemented our algorithms in a tool that was used for the analysis of a concurrent lexer server.