Constrained Reachability of Process Rewrite Systems

We consider the problem of analyzing multi-threaded programs with recursive calls, dynamic creation of parallel procedures, and communication. We model such programs by Process Rewrite Systems (PRS) which are sets of term rewriting rules. Terms in this framework represent program control structures. The semantics of PRS systems is defined modulo structural equivalences on terms expressing properties of the operators appearing in the terms (idle process, sequential composition, and asynchronous parallel composition). We consider the problem of reachability analysis of PRSs under constraints on the execution actions. This problem is undecidable even for regular constraints. [LS98] showed that it becomes decidable for decomposable constraints for the PRS subclass PA if structural equivalences are riot taken into account. In this work, we go further and show that for decomposable constraints, we can compute tree automata representations of the constrained reachability sets for the whole class of PRS modulo different structural equivalences. Our results can be used to solve program (data flow) analysis and verification problems that can be reduced to the constrained reachability analysis problem.