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

File

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

Document Identifiers

Subject Classification

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

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.

Cite As Get 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

Author Details

Fu Song
Weikai Miao
Geguang Pu
Min Zhang

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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact