2026-07-22T06:21:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5362 2024-03-06T10:36:32Z ddc:004 open_access

On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference Song, Fu Miao, Weikai Pu, Geguang Zhang, Min Verification Reachability problem Pushdown system with transductions Boolean programs with call-by-reference 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fu Song and Weikai Miao and Geguang Pu and Min Zhang 2015 Is Part Of LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2015.383 urn:nbn:de:0030-drops-53624 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.383 eng https://creativecommons.org/licenses/by/3.0/legalcode