Reachability analysis of process rewrite systems

Process Rewrite Systems (PRS for short) subsume many common (infinite-state) models such as pushdown systems and Petri nets. They can be adopted as formal models of parallel programs (multithreaded programs) with procedure calls. We develop automata techniques allowing to build finite representations of the forward/backward sets of reachable configurations of PRSs modulo various term structural equivalences (corresponding to properties of the operators of sequential composition and parallel composition). We show that, in several cases, these reachability sets can be represented by polynomial size finite bottom-up tree-automata. When associativity and commutativity of the parallel composition is taken into account, nonregular representations based on (a decidable class of) counter tree automata are sometimes needed.