Document Open Access Logo

On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference

Authors Fu Song, Weikai Miao, Geguang Pu, Min Zhang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.383.pdf
  • Filesize: 0.62 MB
  • 15 pages

Document Identifiers

Author Details

Fu Song
Weikai Miao
Geguang Pu
Min Zhang

Cite AsGet BibTex

Fu Song, Weikai Miao, Geguang Pu, and Min Zhang. On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 383-397, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.383

Abstract

Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems (PDSs) by associating each transition rule with a transduction, which allows to inspect and modify the stack content at each step of a transition rule. It was shown by Uezato and Minamide that TrPDSs can model PDSs with checkpoint and discrete-timed PDSs. Moreover, TrPDSs can be simulated by PDSs and the predecessor configurations pre^*(C) of a regular set C of configurations can be computed by a saturation procedure when the closure of the transductions in TrPDSs is finite. In this work, we comprehensively investigate the reachability problem of finite TrPDSs. We propose a novel saturation procedure to compute pre^*(C) for finite TrPDSs. Also, we introduce a saturation procedure to compute the successor configurations post^*(C) of a regular set C of configurations for finite TrPDSs. From these two saturation procedures, we present two efficient implementation algorithms to compute pre^*(C) and post^*(C). Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing. The TrPDS model has finite closure of transductions which results in model-checking approach for Boolean programs with call-by-reference parameter passing against safety properties.
Keywords
  • Verification
  • Reachability problem
  • Pushdown system with transductions
  • Boolean programs with call-by-reference

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. Dense-timed pushdown automata. In Proceedings of LICS, pages 35-44, 2012. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. The minimal cost reachability problem in priced timed pushdown systems. In Proceedings of LATA, pages 58-69, 2012. Google Scholar
  3. Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Proceedings of SPIN, pages 113-130, 2000. Google Scholar
  4. Ahmed Bouajjani and Michael Emmi. Analysis of recursively parallel programs. In Proceedings of POPL, pages 203-214, 2012. Google Scholar
  5. Ahmed Bouajjani and Michael Emmi. Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst., 35(3):10, 2013. Google Scholar
  6. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of CONCUR, pages 135-150, 1997. Google Scholar
  7. Ahmed Bouajjani, Markus Müller-Olm, and Tayssir Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In Proceedings of CONCUR, pages 473-487, 2005. Google Scholar
  8. Tomás Brázdil, Antonín Kucera, and Oldrich Strazovský. On the decidability of temporal properties of probabilistic pushdown automata. In Proceedings of STACS, pages 145-157, 2005. Google Scholar
  9. Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. Google Scholar
  10. Xiaojuan Cai and Mizuhito Ogawa. Well-structured pushdown systems. In Proceedings of CONCUR, pages 121-136, 2013. Google Scholar
  11. Xiaojuan Cai and Mizuhito Ogawa. Well-structured pushdown system: Case of dense timed pushdown automata. In Proceedings of FLOPS, pages 336-352, 2014. Google Scholar
  12. Christopher Earl, Ilya Sergey, Matthew Might, and David Van Horn. Introspective pushdown analysis of higher-order programs. In Proceedings of ICFP, pages 177-188, 2012. Google Scholar
  13. Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In Proceedings of CAV, pages 232-247, 2000. Google Scholar
  14. Javier Esparza, Antonín Kucera, and Richard Mayr. Model checking probabilistic pushdown automata. In Proceedings of LICS, pages 12-21, 2004. Google Scholar
  15. Javier Esparza, Antonín Kucera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. In Proceedings of TACS, pages 316-339, 2001. Google Scholar
  16. Javier Esparza and Stefan Schwoon. A bdd-based model checker for recursive programs. In Proceedings of CAV, pages 324-336, 2001. Google Scholar
  17. Matthew Hague and C.-H. Luke Ong. Analysing mu-calculus properties of pushdown systems. In Proceedings of SPIN, pages 187-192, 2010. Google Scholar
  18. Vineet Kahlon, Franjo Ivancic, and Aarti Gupta. Reasoning about threads communicating via locks. In Proceedings of CAV, pages 505-518, 2005. Google Scholar
  19. Akash Lal, Thomas W. Reps, and Gogul Balakrishnan. Extended weighted pushdown systems. In Proceedings of CAV, pages 434-448, 2005. Google Scholar
  20. Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, and Shoji Yuen. Nested timed automata. In Proceedings of FORMATS, pages 168-182, 2013. Google Scholar
  21. Xin Li and Mizuhito Ogawa. Conditional weighted pushdown systems and applications. In Proceedings of PEPM, pages 141-150, 2010. Google Scholar
  22. Yasuhiko Minamide and Shunsuke Mori. Reachability analysis of the HTML5 parser specification and its application to compatibility testing. In Proceedings of FM, pages 293-307, 2012. Google Scholar
  23. Thomas W. Reps, Stefan Schwoon, and Somesh Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proceedings of SAS, pages 189-213, 2003. Google Scholar
  24. Koushik Sen and Mahesh Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In Proceedings of CAV, pages 300-314, 2006. Google Scholar
  25. Fu Song and Tayssir Touili. Efficient CTL model-checking for pushdown systems. In Proceedings of CONCUR, pages 434-449, 2011. Google Scholar
  26. Fu Song and Tayssir Touili. PuMoC: a CTL model-checker for sequential programs. In Proceedings of ASE, pages 346-349, 2012. Google Scholar
  27. Fu Song and Tayssir Touili. Model checking dynamic pushdown networks. In Proceedings of APLAS, pages 33-49, 2013. Google Scholar
  28. Fu Song and Tayssir Touili. Efficient CTL model-checking for pushdown systems. Theor. Comput. Sci., 549:127-145, 2014. Google Scholar
  29. Fu Song and Tayssir Touili. Model checking dynamic pushdown networks. Formal Asp. Comput., 27(2):397-421, 2015. Google Scholar
  30. Yuya Uezato and Yasuhiko Minamide. Pushdown systems with stack manipulation. In Proceedings of ATVA, pages 412-426, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact