skip to content

Automata-based techniques for the analysis of dynamic concurrent programs

Tuesday 23rd May 2006 - 11:00 to 12:00
INI Seminar Room 1

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.

University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons