×

On the reachability analysis of acyclic networks of pushdown systems. (English) Zbl 1160.68451

van Breugel, Franck (ed.) et al., CONCUR 2008 – concurrency theory. 19th international conference, CONCUR 2008, Toronto, Canada, August 19–22, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85360-2/pbk). Lecture Notes in Computer Science 5201, 356-371 (2008).
Summary: We address the reachability problem in acyclic networks of pushdown systems. We consider communication based either on shared memory or on message passing through unbounded lossy channels. We prove mainly that the reachability problem between recognizable sets of configurations (i.e., definable by a finite union of products of finite-state automata) is decidable for such networks, and that for lossy channel pushdown networks, the channel language is effectively recognizable. This fact holds although the set of reachable configurations (including stack contents) for a network of depth (at least) 2 is not rational in general (i.e., not definable by a multi-tape finite automaton). Moreover, we prove that for a network of depth 1, the reachability set is rational and effectively constructible (under an additional condition on the topology for lossy channel networks).
For the entire collection see [Zbl 1149.68018].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

MAGIC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313-321 (1996)
[2] Abdulla, P. A.; Collomb-Annichini, A.; Bouajjani, A.; Jonsson, B., Using forward reachability analysis for verification of lossy channel systems, FMSD, 25, 1, 39-65 (2004) · Zbl 1073.68675
[3] Abdulla, P. A.; Jonsson, B., Verifying programs with unreliable channels, Inf. Comput., 127, 2, 91-101 (1996) · Zbl 0856.68096 · doi:10.1006/inco.1996.0053
[4] Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. Research report, LIAFA lab (April 2008) · Zbl 1160.68451
[5] Berstel, J.: Transductions and context-free langages. TeubnerStudienbucher Informatik (1979) · Zbl 0424.68040
[6] Bouajjani, A.; Esparza, J.; Schwoon, S.; Strejcek, J.; Ramanujam, R.; Sen, S., Reachability analysis of multithreaded software with asynchronous communication, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (2005), Heidelberg: Springer, Heidelberg · Zbl 1172.68422 · doi:10.1007/11590156_28
[7] Bouajjani, A.; Esparza, J.; Touili, T., A generic approach to the static analysis of concurrent programs with procedures, Int. J. Found. Comput. Sci., 14, 4, 551 (2003) · Zbl 1101.68457 · doi:10.1142/S0129054103001893
[8] Bouajjani, A.; Müller-Olm, M.; Touili, T.; Abadi, M.; de Alfaro, L., Regular symbolic analysis of dynamic networks of pushdown systems, CONCUR 2005 - Concurrency Theory (2005), Heidelberg: Springer, Heidelberg · doi:10.1007/11539452_36
[9] Bouajjani, A.; Touili, T.; Pandya, P. K.; Radhakrishnan, J., Reachability analysis of process rewrite systems, FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 74-87 (2003), Heidelberg: Springer, Heidelberg · Zbl 1205.68183
[10] Bouajjani, A.; Touili, T.; Giesl, J., On computing reachability sets of process rewrite systems, Term Rewriting and Applications (2005), Heidelberg: Springer, Heidelberg · Zbl 1078.68652
[11] Bouajjani, A.; Esparza, J.; Pfenning, F., Rewriting models of boolean programs, Term Rewriting and Applications, 136-150 (2006), Heidelberg: Springer, Heidelberg · Zbl 1151.68440 · doi:10.1007/11805618_11
[12] Chadha, R.; Viswanathan, M.; Caires, L.; Vasconcelos, V. T., Decidability results for well-structured transition systems with auxiliary storage, CONCUR 2007 - Concurrency Theory, 136-150 (2007), Heidelberg: Springer, Heidelberg · Zbl 1151.68515 · doi:10.1007/978-3-540-74407-8_10
[13] Chaki, S.; Clarke, E. M.; Kidd, N.; Reps, T. W.; Touili, T.; Hermanns, H.; Palsberg, J., Verifying concurrent message-passing c programs with recursive calls, Tools and Algorithms for the Construction and Analysis of Systems, 334-349 (2006), Heidelberg: Springer, Heidelberg · Zbl 1180.68109 · doi:10.1007/11691372_22
[14] Chambard, P.; Schnoebelen, P.; Arvind, V.; Prasad, S., Post embedding problem is not primitive recursive, with applications to channel systems, FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 265-276 (2007), Heidelberg: Springer, Heidelberg · Zbl 1136.03030 · doi:10.1007/978-3-540-77050-3_22
[15] Esparza, J.; Knoop, J.; Thomas, W., An automata-theoretic approach to interprocedural dataflow analysis, Foundations of Software Science and Computation Structures (1999), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-49019-1_2
[16] Esparza, J., Podelski, A.: Efficient algorithms for \(pre^{\mbox{*}}\) and \(post^{\mbox{*}}\) on interprocedural parallel flow graphs. In: POPL, pp. 1-11 (2000) · Zbl 1323.68407
[17] Finkel, A.; Schnoebelen, P.., Well-structured transition systems everywhere!, TCS, 256, 1-2, 63-92 (2001) · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[18] Jhala, R.; Majumdar, R., Interprocedural analysis of asynchronous programs, POPL (2007), Los Alamitos: IEEE, Los Alamitos · Zbl 1295.68086
[19] Kahlon, V.; Ivancic, F.; Gupta, A.; Etessami, K.; Rajamani, S. K., Reasoning about threads communicating via locks, Computer Aided Verification (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68623
[20] La Torre, S.; Madhusudan, P.; Parlato, G.; Ramakrishnan, C. R.; Rehof, J., Context-bounded analysis of concurrent queue systems, Tools and Algorithms for the Construction and Analysis of Systems (2008), Heidelberg: Springer, Heidelberg · Zbl 1134.68446 · doi:10.1007/978-3-540-78800-3_21
[21] Lammich, P.; Müller-Olm, M.; Caires, L.; Vasconcelos, V. T., Precise fixpoint-based analysis of programs with thread-creation and procedures, CONCUR 2007 - Concurrency Theory (2007), Heidelberg: Springer, Heidelberg · Zbl 1151.68361 · doi:10.1007/978-3-540-74407-8_20
[22] Lugiez, D.; Schnoebelen, P..; Sangiorgi, D.; de Simone, R., The regular viewpoint on PA-processes, CONCUR ’98 Concurrency Theory, 50-66 (1998), Heidelberg: Springer, Heidelberg · Zbl 0932.68052 · doi:10.1007/BFb0055615
[23] Mayr, R.: Undecidable problems in unreliable computations. Theor. Comput. Sci. 1-3(297) (2003) · Zbl 1044.68119
[24] Qadeer, S.; Rehof, J.; Halbwachs, N.; Zuck, L. D., Context-bounded model checking of concurrent software, Tools and Algorithms for the Construction and Analysis of Systems (2005), Heidelberg: Springer, Heidelberg
[25] Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5) (2002) · Zbl 1043.68016
[26] Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universität München (2002)
[27] Sen, K.; Viswanathan, M.; Ball, T.; Jones, R. B., Model checking multithreaded programs with asynchronous atomic methods, Computer Aided Verification, 300-314 (2006), Heidelberg: Springer, Heidelberg · Zbl 1188.68198 · doi:10.1007/11817963_29
[28] La Torre, S.; Madhusudan, P.; Parlato, G., A robust class of context-sensitive languages, LICS, 161-170 (2007), Los Alamitos: IEEE, Los Alamitos
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.