Automata-based techniques for the analysis of dynamic concurrent programs
Seminar Room 1, Newton Institute
We propose formal models for dynamic programs with procedure calls and dynamic creation of concurrent processes. The considered models are based on (combinations of) various classes of rewrite systems such as multiset rewrite systems and prefix rewrite systems. We address the reachability analysis problem for such models. More precisely, we consider the problem of of computing finite representations of the (potentially infinite) sets of reachable configurations in such models. We consider finite word/tree automata for the representation of these reachability sets. The proposed constructions can be used for solving model-checking problems for the considered classes of infinite-state models.