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.
@InProceedings{song_et_al:LIPIcs.CONCUR.2015.383, author = {Song, Fu and Miao, Weikai and Pu, Geguang and Zhang, Min}, title = {{On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {383--397}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-91-0}, ISSN = {1868-8969}, year = {2015}, volume = {42}, editor = {Aceto, Luca and de Frutos Escrig, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.383}, URN = {urn:nbn:de:0030-drops-53624}, doi = {10.4230/LIPIcs.CONCUR.2015.383}, annote = {Keywords: Verification, Reachability problem, Pushdown system with transductions, Boolean programs with call-by-reference} }
Feedback for Dagstuhl Publishing