Reachability Analysis of Process Rewrite Systems

10 years 11 months ago
Reachability Analysis of Process Rewrite Systems
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. Key words: Multithreaded programs with procedure calls, synchronisation, process algebra...
Ahmed Bouajjani, Tayssir Touili
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Authors Ahmed Bouajjani, Tayssir Touili
Comments (0)