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
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