TY - GEN
T1 - On reachability analysis of pushdown systems with transductions
T2 - 26th International Conference on Concurrency Theory, CONCUR 2015
AU - Song, Fu
AU - Miao, Weikai
AU - Pu, Geguang
AU - Zhang, Min
N1 - Publisher Copyright:
© Fu Song, Weikai Miao, Geguang Pu, and Min Zhang; licensed under Creative Commons License CC-BY.
PY - 2015/8/1
Y1 - 2015/8/1
N2 - 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 modelchecking approach for Boolean programs with call-by-reference parameter passing against safety properties.
AB - 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 modelchecking approach for Boolean programs with call-by-reference parameter passing against safety properties.
KW - Boolean programs with call-by-reference
KW - Pushdown system with transductions
KW - Reachability problem
KW - Verification
UR - https://www.scopus.com/pages/publications/84958231964
U2 - 10.4230/LIPIcs.CONCUR.2015.383
DO - 10.4230/LIPIcs.CONCUR.2015.383
M3 - 会议稿件
AN - SCOPUS:84958231964
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 383
EP - 397
BT - 26th International Conference on Concurrency Theory, CONCUR 2015
A2 - Aceto, Luca
A2 - de Frutos Escrig, David
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Y2 - 1 September 2015 through 4 September 2015
ER -