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...

• Type: Conference
• Year: 2003
• Where: FSTTCS
• Authors: Ahmed Bouajjani, Tayssir Touili
• Keywords: Exact Reachable Configurations, FSTTCS 2003, Parallel Processes, Reachable Configurations