Special Issue – Reachability Problems (RP 2009)No Access

FORWARD ANALYSIS OF DYNAMIC NETWORK OF PUSHDOWN SYSTEMS IS EASIER WITHOUT ORDER

DENIS LUGIEZ

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

https://doi.org/10.1142/S0129054111008453Cited by:4 (Source: Crossref)

Abstract

Dynamic networks of Pushdown Systems (DNPS 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 yields decidability of the forward analysis of DNPS. Finally, we extend this result to the model where configurations are sets of threads running in parallel.

Keywords:

References

A. Bouajjani, M. Müller-Olm and T. Touili, Regular symbolic analysis of dynamic networks of pushdown systems, CONCUR3653, Lecture Notes in Computer Science, eds. Martín Abadi and Luca de Alfaro (Springer, 2005) pp. 473–487. Google Scholar
J. Esparza and A. Podelski, Efficient algorithms for pre* and post* on interprocedural parallel flow graphs, POPL (2000) pp. 1–11. Google Scholar
O. Maler, A. Bouajjani and J. Esparza, Reachability analysis of pushdown automata: Application to model-checking, Proceedings 8th International Conference on Concurrency Theory (CONCUR)1243, Lecture Notes in Computer Science (Springer-Verlag, 1997) pp. 14–25. Google Scholar
T. W. Reps, S. Schwoon and S. Jha, Weighted pushdown systems and their application to interprocedural dataflow analysis, SAS2694, Lecture Notes in Computer Science, ed. Radhia Cousot (Springer, 2003) pp. 189–213. Google Scholar
D. Lugiez and Ph. Schnoebelen, The regular viewpoint on pa-processes, Concur'981466, Lecture Notes in Computer Science, eds. D. Sangiorgi and R. de Simone (Springer-Verlag, 1998) pp. 50–66. Google Scholar
V. Kahlon and A. Gupta, On the analysis of interacting pushdown systems, POPL, eds. Martin Hofmann and Matthias Felleisen (ACM, 2007) pp. 303–314. Google Scholar
P. Lammich, M. Mller-Olm and A. Wenner, Predecessor sets of dynamic pushdown networks with tree-regular constraints, Proc. of 21st Conf. on Computer Aided Verification (CAV)5643, Lecture Notes in Computer Science (Springer, 2009) pp. 525–539. Google Scholar
S. Dal Zilio and D. Lugiez, Applicable Algebra in Engineering, Communication and Computing 17(5), 337 (2006). Crossref, Web of Science, Google Scholar
R. Mayr and M. Rusinowitch, Reachability is decidable for ground ac rewrite systems, Proceedings of the 3rd INFINITY Workshop (1998) pp. 53–64. Google Scholar
D. Lugiez. Forward analysis of dynamic network of pushdown systems is easier without order, 2009. Available at http://www.lif.univ-mrs.fr/~lugiez . Google Scholar
H. Comon et al. , Tree Automata and their application ( Freeware Book , 1999 ) . Google Scholar
R. Buchi, Archiv fur Matematische Logik und Grundla-genforschung 6, 91 (1964). Google Scholar
D. Caucal, On word rewriting systems having a rational derivation, FoSSaCS1784, Lecture Notes in Computer Science, ed. Jerzy Tiuryn (Springer, 2000) pp. 48–62. Google Scholar
M. Presburger , Uber die vollstandigkeit eines gewissen system der arithmetik ganzer zahlen in welchem die addition als einzige operation hervortritt , Comptes Rendus du I Congres des Mathematiciens des Pays Slaves . Google Scholar
C. Reutenauer , The Mathematics Of Petri Nets ( Prentice-Hall , 1990 ) . Google Scholar
S. Ginsburg and E. Spanier, Pacific Journal of Mathematics 16, 285 (1966). Crossref, Web of Science, Google Scholar
K. N. Verma, H. Seidl and T. Schwentick, On the complexity of equational horn clauses, CADE3632, Lecture Notes in Computer Science, ed. Robert Nieuwenhuis (Springer, 2005) pp. 337–352. Google Scholar