On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference
On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference
复制标题
DOI：
10.4230/lipics.concur.2015.383
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Fu Song;Weikai Miao;G. Pu;Min Zhang-
中科院分区：
文献类型：
--
作者：
Fu Song;Weikai Miao;G. Pu;Min Zhang-
带有转换的下推系统（TrPDS）是下推系统（PDS）的扩展，通过将每个转换规则与转换相关联，允许在转换规则的每个步骤检查和修改堆栈内容。Uezato和Minamide表明，TrPDS可以对具有检查点的PDS和离散时间的PDS进行建模。此外，TrPDS可以由PDS来模拟，并且当TrPDS中的转换的闭合是有限的时，可以通过饱和过程来计算配置的规则集合C的前驱配置pre^*（C）。在这项工作中，我们全面调查的可达性问题的有限TrPDS。我们提出了一种新的饱和过程来计算有限TrPDS的pre^*（C）。此外，我们还引入了一个饱和过程来计算有限TrPDS的正则配置集C的后继配置post^*（C）。从这两个饱和过程中，我们提出了两个有效的实现算法来计算前^*（C）和后^*（C）。最后，我们将展示如何存在的transmuctions使布尔程序的建模与调用引用参数传递。TrPDS模型具有有限的转换闭包，这导致了布尔程序的模型检查方法，通过引用调用参数传递安全属性。
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.