PRESS: analysis of Process Rewrite Systems

BARRE

Contents

BARRE

Introduction

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

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

Reachability Analysis: The approach implemented in PRESS

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:

Examples

Several toy examples are available in the package (input directory). Moreover, a description of a concurrent lexer can be found in [ST06].

Credits

PRESS is written, debugged, maintained and improved by Mihaela Sighireanu and Tayssir Touili.

Download

You can download the PRESS tool via HTTP.

For installing PRESS you need:

References

ST06
M. Sighireanu and T. Touili, Bounded Communication Reachability Analysis of O-Process Rewrite Systems. In Proc. of 8th International Workshop on Verification of Infinite-State Systems (Infinity'06).
BT03
A. Bouajjani and T. Touili, Reachability Analysis of Process Rewrite Systems. In Proc. Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03).
Tou03
T. Touili, Analyse symbolique de systèmes infinis basée sur les automates: Application à la vérification de systèmes paramétrés et dynamiques. PhD. thesis, 2003.
BT05
A. Bouajjani and T. Touili, On Computing Reachability Sets of Process Rewrite Systems. In Proc. 16th Intern. Conf. on Rewriting Techniques and Applications (RTA'05).
May98
R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Sytems. PhD thesis, 1998.

BARRE

Last updated: Tue Jul 18 16:19:27 CEST 2006