PRESS is a tool for computing finite representations of the forward/backward reachable configurations of multi-threaded programs with dynamic creation of processes and (recursive) procedure calls. Such programs are modeled using Process Rewrite Systems. Reachable configurations are computed modulo several term structural equivalences [BT03, Tou03, ST06].
Process Rewrite Systems (PRS for short) [May98] is a finite set of rules of the form t -> t' where t and t' are terms built up from the idle process ("0"), a finite set of process variables ("X"), sequential composition ("·"), and asynchronous parallel composition ("||"). The semantics of PRSs considers terms modulo a structural equivalence (=) which expresses the fact that "0" is a neutral element of "·" and "||", that "·" is associative, and that "||" is associative and commutative. It is easy to see that with this semantics, PRS subsumes well-known models such as pushdown automata and Petri nets. Examples of programs modeled using PRS can be found in [BT03, Tou03, ST06].
PRESS can also analyze O-PRS systems [ST06], which is the extension of PRS with a new parallel operator "O" that is associative but not commutative, and hence it preserves the order between parallel processes. This parallel operator is needed to model programs where the order between parallel processes is important, such as the concurrent lexer described in [ST06].
Unfortunately, while reachability between terms is decidable for PRS [May98], it becomes undecidable for O-PRS due to the associativity of "O" [ST06]. Despite this undecidability, PRESS tackles the reachability problem between two (infinite) sets of terms. Since process terms can be seen as trees, (bottom-up) tree automata are used to represent (infinite) sets of terms. To sidestep the undecidability problem, PRESS proceeds as follows:
Several toy examples are available in the package (input
directory). Moreover, a description of a concurrent
lexer can be found in [ST06].
PRESS is written, debugged, maintained and improved by Mihaela Sighireanu and Tayssir Touili.
You can download the PRESS tool via HTTP.
For installing PRESS you need:
Last updated: Tue Jul 18 16:19:27 CEST 2006