Skip to main content
SpringerLink
Log in

Forward Analysis of Dynamic Network of Pushdown Systems Is Easier without Order

  • Conference paper
Reachability Problems (RP 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5797))

Included in the following conference series:

Abstract

Dynamic networks of Pushdown Systems (PDN in short) have been introduced to perform static analysis of concurrent programs that may spawn threads dynamically. In this model the set of successors of a regular set of configurations can be non-regular, making forward analysis of these models difficult. We refine the model by adding the associative-commutative properties of parallel composition, and we define Presburger weighted tree automata, an extension of weighted automata and tree automata, that accept the set of successors of a regular set of configurations. This allows forward analysis of PDN since these automata have a decidable emptiness problem and are closed under intersection.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Maler, O., Bouajjani, A., Esparza, J.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 14–25. Springer, Heidelberg (1997)

    Google Scholar 

  2. Bouajjani, A., Müller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473–487. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Buchi, R.: Regular canonical systems. Archiv fur Matematische Logik und Grundlagenforschung 6(91-111) (1964)

    Google Scholar 

  4. Caucal, D.: On word rewriting systems having a rational derivation. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 48–62. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Comon, H., Dauchet, M., Jacquemard, F., Loeding, C., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata on their application. Freeware Book (1999), http://tata.gforge.inria.fr/

  6. Esparza, J., Podelski, A.: Efficient algorithms for pre\(^{\mbox{*}}\) and post\(^{\mbox{*}}\) on interprocedural parallel flow graphs. In: POPL, pp. 1–11 (2000)

    Google Scholar 

  7. Ginsburg, S., Spanier, E.: Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics 16, 285–296 (1966)

    Article  MathSciNet  MATH  Google Scholar 

  8. Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 303–314. ACM, New York (2007)

    Google Scholar 

  9. Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Proc. of 21st Conf. on Computer Aided Verification (CAV). LNCS, vol. 5643, pp. 525–539. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  11. Presburger, M.: Uber die vollstandigkeit eines gewissen system der arithmetik ganzer zahlen in welchem die addition als einzige operation hervortritt. In: Comptes Rendus du I Congres des Mathematiciens des Pays Slaves, Warszawa (1929)

    Google Scholar 

  12. Reps, T.W., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 189–213. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 337–352. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Zilio, S.D., Lugiez, D.: XML schema, tree logic and sheaves automata. Applicable Algebra in Engineering, Communication and Computing 17(5), 337–377 (2006)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIF UMR 6166 Aix-Marseille Université- CNRS, France

    Denis Lugiez

Authors
  1. Denis Lugiez
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Ecole Polytechnique, Laboratoire d’ Informatique (LIX), 91128, Palaiseau Cedex, France

    Olivier Bournez

  2. Department of Computer Science, Ashton Building, University of Liverpool, L69 3BX, Liverpool, England

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lugiez, D. (2009). Forward Analysis of Dynamic Network of Pushdown Systems Is Easier without Order. In: Bournez, O., Potapov, I. (eds) Reachability Problems. RP 2009. Lecture Notes in Computer Science, vol 5797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04420-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04420-5_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04419-9

  • Online ISBN: 978-3-642-04420-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation