On Computing Reachability Sets of Process Rewrite Systems

  • Ahmed Bouajjani
  • Tayssir Touili
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We consider the problem of symbolic reachability analysis of a class of term rewrite systems called Process Rewrite Systems (PRS). A PRS can be seen as the union of two mutually interdependent sets of term rewrite rules: a prefix rewrite system (or, equivalently, a pushdown system), and a multiset rewrite system (or, equivalently, a Petri net). These systems are natural models for multithreaded programs with dynamic creation of concurrent processes and recursive procedure calls. We propose a generic framework based on tree automata allowing to combine (finite-state automata based) procedures for the reachability analysis of pushdown systems with (linear arithmetics/semilinear sets based) procedures for the analysis of Petri nets in order to analyze PRS models. We provide a construction which is parametrized by such procedures and we show that it can be instantiated to (1) derive procedures for constructing the (exact) reachability sets of significant classes of PRS, (2) derive various approximate algorithms, or exact semi-algorithms, for the reachability analysis of PRS obtained by using existing symbolic reachability analysis techniques for Petri nets and counter automata.


Model Check Reachability Analysis Tree Automaton Model Check Problem Multithreaded Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ammirati, P., Delzanno, G., Ganty, P., Geeraerts, G., Raskin, J.-F., Van Begin, L.: Babylon: An integrated toolkit for the specification and verification of parameterized systems. In: SAVE 2002 (2002)Google Scholar
  2. 2.
    Annichini, A., Asarin, E., Bouajjani, A.: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A Tool for Reachability Analysis of Complex Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 368. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 158. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223–235. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Boigelot, B., Wolper, P.: Symbolic Verification with Periodic Sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, Springer, Heidelberg (1994)Google Scholar
  9. 9.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, Springer, Heidelberg (1997)Google Scholar
  10. 10.
    Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proc. of the 30th ACM Symp. on Principles of Programming Languages, POPL 2003 (2003)Google Scholar
  11. 11.
    Bouajjani, A., Esparza, J., Touili, T.: Reachability Analysis of Synchronized PA Systems. In: Proc. Infinity Workshop (2004)Google Scholar
  12. 12.
    Bouajjani, A., Touili, T.: Reachability Analysis of Process Rewrite Systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 74–87. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Bruggemann-Klein, A., Murata, M., Wood, D.: Regular tree and regular hedge languages over unranked alphabets. Research report (2001)Google Scholar
  14. 14.
    Bultan, T., Gerber, R., League, C.: Verifying Systems With Integer Constraints and Boolean Predicates: A Composite Approach. In: Proc. of the Intern. Symp. on Software Testing and Analysis, ACM press, New York (1998)Google Scholar
  15. 15.
    Caucal, D.: On the regular structure of prefix rewriting. Theoret. Comput. Sci. 106, 61–86 (1992)CrossRefMathSciNetGoogle Scholar
  16. 16.
    Colcombet, T.: Rewriting in the partial algebra of typed terms modulo ac. In: Proc. Infinity Workshop. Electronic Notes in Theoretical Computer Science, vol. 68, Elsevier Science Pub., Amsterdam (2002)Google Scholar
  17. 17.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, ACM, New York (1978)Google Scholar
  18. 18.
    Delzanno, G., Van Begin, L., Raskin, J.-F.: Attacking symbolic state explosion in parametrized verification. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 298. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Delzanno, G., Van Begin, L., Raskin, J.-F.: Toward the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 173. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  20. 20.
    Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, Springer, Heidelberg (1995)Google Scholar
  21. 21.
    Esparza, J.: Grammars as processes. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, p. 277. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithm for model checking pushdown systems. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)Google Scholar
  23. 23.
    Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 14–30. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  24. 24.
    Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design 16 (2000)Google Scholar
  25. 25.
    Esparza, J., Nielsenl, M.: Decidability issues for Petri nets - a survey. Bulletin of the EATCS 52, 85–107 (1994)Google Scholar
  26. 26.
    Esparza, J., Schwoon, S.: A bdd-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  27. 27.
    Esparza, J., Podelski, A.: Efficient algorithms for pre * and post * on interprocedural parallel flow graphs. In: Symposium on Principles of Programming Languages, pp. 1–11 (2000)Google Scholar
  28. 28.
    Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  29. 29.
    Finkel, A., Willems, B., Wolper, P.: A Direct Symbolic Approach to Model Checking Pushdown Systems. In: Infinity 1997 (1997)Google Scholar
  30. 30.
    Hopcroft, J., Pansiot, J.-J.: On The Reachability Problem for 5-Dimensional Vector Addition Systems. Theoret. Comput. Sci. 8 (1979)Google Scholar
  31. 31.
    The Liège Automata-based Symbolic Handler, LASH (2001), Available at
  32. 32.
    Lugiez, D.: Counting and equality constraints for multitree automata. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 328–342. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  33. 33.
    Lugiez, D., Schnoebelen, P.: The regular viewpoint on PA-processes. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 50–66. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  34. 34.
    Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Phd. thesis, Techn. Univ. of Munich (1998)Google Scholar
  35. 35.
    Qadeer, S., Rajamani, S.K., Rehof, J.: Procedure Summaries for Model Checking Multithreaded Software. In: POPL 2004, ACM, New York (2004)Google Scholar
  36. 36.
    Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit ät München (2002)Google Scholar
  37. 37.
    Seidl, H., Schwentick, T., Muscholl, A.: Numerical Document Queries. In: PODS 2003, ACM Press, New York (2003)Google Scholar
  38. 38.
    Touili, T.: 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, University of Paris 7 (2003)Google Scholar
  39. 39.
    Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ahmed Bouajjani
    • 1
  • Tayssir Touili
    • 1
  1. 1.LIAFAUniversity of Paris 7Paris cedex 5France

Personalised recommendations