推导系统可达性分析：应用到带引用调用的布尔程序
201 浏览量
更新于2024-07-15
收藏 640KB PDF 举报
本文主要探讨了带转换的推导系统(TrPDS)在可达到性分析中的应用，特别是针对带有引用调用的布尔程序。推导系统（Pushdown Systems, PDS）是一种理论模型，它在计算理论中扮演着重要角色，尤其是自动机理论。PDS通过栈操作来处理输入符号序列，而TrPDS则是对其的一种扩展，每个转换规则都关联了一个转换，允许在执行规则时检查和修改栈内容。
Uezato和Minamide的工作表明，TrPDS能够捕获具有检查点的PDS和离散时间PDS，这增加了其灵活性和适用范围。它们之间的关系体现在TrPDS可以通过PDS进行模拟，并且当TrPDS中的转换集合是有限的时，可以通过饱和过程计算出配置集合C的前驱状态集pre*(C)。饱和过程是一种递归方法，用于穷举所有可能的状态演变路径。
本文的焦点在于对有限TrPDS的可达到性问题进行深入研究。作者提出了一个新的饱和过程算法，旨在计算有限TrPDS中给定配置集合C的前驱状态pre*(C)，这对于理解系统的初始可达性和状态空间至关重要。此外，文中还引入了一种新的饱和过程，用于计算配置集合C的后继状态集post*(C)，这对于分析程序的终止行为和错误检测非常有用。
对于实际应用而言，这篇研究有助于开发者更好地理解和控制带转换的程序行为，尤其是在处理那些涉及复杂数据结构和状态管理的布尔程序时。通过这些新颖的分析方法，研究人员和工程师可以设计更有效的静态分析工具，用于检测潜在的问题并优化代码性能。因此，本文不仅深化了理论基础，也提供了实用的工程实践指导。
F. Song, W. Miao, G. Pu, and M. Zhang 385
2 Preliminaries
2.1 Finite-State Transducers and Transduction
I Definition 1.
A finite-state transducer (FST)
T
is a tuple (
Q,
Γ
, δ, I, F
), where
Q
is a
finite set of states, Γ is a finite alphabet,
δ ⊆ Q ×
Γ
∗
×
Γ
∗
× Q
is a finite set of transition
rules,
I ⊆ Q
(resp.
F ⊆ Q
) is a finite set of initial (resp. final) states. The transducer is
letter-to-letter if δ ⊆ Q × Γ × Γ × Q.
We will write
q
ω
1
/ω
2
−−−−−→ q
0
if (
q, ω
1
, ω
2
, q
0
)
∈ δ
. Let
−→
∗
be the smallest relation such
that
q
/
−−−−→
∗
q
for every
q ∈ Q
; if
q
ω
1
/ω
2
−−−−−−→
∗
q
0
and
q
0
ω
3
/ω
4
−−−−−→ q
00
, then
q
ω
1
ω
3
/ω
2
ω
4
−−−−−−−−−→
∗
q
00
.
A FST
T
transduces a string
ω
1
∈
Γ
∗
into a string
ω
2
∈
Γ
∗
if there exist states
q
0
∈ I
and
q
f
∈ F
such that
q
0
ω
1
/ω
2
−−−−−−→
∗
q
f
. The language
L
(
T
) of a FST
T
is the set of pairs (
ω
1
, ω
2
)
such that T can transduce ω
1
into ω
2
.
A transduction
τ ⊆
Γ
∗
×
Γ
∗
is a relation over Γ
∗
. A transduction
τ
is rational (regular)
and length-preserving if there is a letter-to-letter transducer
T
such that
τ
=
L
(
T
). Let
τ
id
denote the identity transduction, i.e.,
τ
id
=
{
(
ω, ω
)
| ∀ω ∈
Γ
∗
}
. In the rest of this
paper, we assume that transductions (resp. transducers) are length-preserving rational (resp.
letter-to-letter) unless stated explicitly, and we do not differentiate the terms transduction
and transducer. Given a transduction τ, let τ(ω) = {ω
0
| (ω, ω
0
) ∈ τ } for ω ∈ Γ
∗
.
The composition ◦ of two transductions τ
1
, τ
2
is defined as
τ
1
◦ τ
2
= {(ω
1
, ω
3
) | ∃ω
2
∈ Γ
∗
, (ω
1
, ω
2
) ∈ τ
1
and (ω
2
, ω
3
) ∈ τ
2
}.
I Proposition 2. For every transduction τ, τ ◦ τ
id
= τ = τ
id
◦ τ .
The left quotient
d·, ·c
−1
over transductions is defined as follows:
∀ω
1
, ω
2
∈
Γ
∗
with
|ω
1
| = |ω
2
|, dω
1
, ω
2
c
−1
τ = {(ω, ω
0
) | (ω
1
ω, ω
2
ω
0
) ∈ τ }.
I Proposition 3. [30] For every ω
1
, ω
2
∈ Γ
n
, for every transduction τ
1
, τ
2
,
dω
1
, ω
2
c
−1
(τ
1
◦ τ
2
) =
[
ω
3
∈Γ
|ω
1
|
(dω
1
, ω
3
c
−1
τ
1
) ◦ (dω
3
, ω
2
c
−1
τ
2
)
.
Let
T
be a set of transductions, the closure
hT i
∪
of
T
over the composition
◦
, left quotient
d·, ·c
−1
and union ∪ is defined as follows:
T ⊆ hT i
∪
, ∅ ∈ hT i
∪
and τ
id
∈ hT i
∪
;
if τ
1
, τ
2
∈ hT i
∪
, then τ
1
◦ τ
2
∈ hT i
∪
and τ
1
∪ τ
2
∈ hT i
∪
;
if τ ∈ hT i
∪
, then dγ, γ
0
c
−1
τ ∈ hT i
∪
for all γ, γ
0
∈ Γ.
Similarly, let
hT i
denote the closure of
T
over the composition
◦
and left quotient
d·, ·c
−1
.
I Proposition 4. (a) The set hT i is finite iff the set hT i
∪
is finite.
(b) The set
hT i
∪
is the semigroup generated by (
hT i, ∪
), that is,
∀τ ∈ hT i
∪
,
∃τ
1
, ..., τ
m
∈
hT i for m ≥ 1 such that τ =
S
m
i=1
τ
i
.
2.2 Pushdown Systems with Transductions
Pushdown systems with transductions (TrPDSs) [
30
] are an extension of pushdown systems
by associating each transition with a transduction which modifies the stack content by
applying the transduction. This extension allows TrPDSs to model sequential programs that
manipulate the stack content rather than only the top of the stack.
C O N C U R ’ 1 5
剩余14页未读，继续阅读
2016-04-12 上传
2021-05-23 上传
2021-02-09 上传
2021-06-16 上传
2021-04-22 上传
2021-02-06 上传
2021-04-22 上传
2021-03-25 上传
2021-02-07 上传
weixin_38626943
- 粉丝: 5
- 资源: 935
我的内容管理
展开
最新资源
- Java集合ArrayList实现字符串管理及效果展示
- 实现2D3D相机拾取射线的关键技术
- LiveLy-公寓管理门户：创新体验与技术实现
- 易语言打造的快捷禁止程序运行小工具
- Microgateway核心：实现配置和插件的主端口转发
- 掌握Java基本操作：增删查改入门代码详解
- Apache Tomcat 7.0.109 Windows版下载指南
- Qt实现文件系统浏览器界面设计与功能开发
- ReactJS新手实验：搭建与运行教程
- 探索生成艺术：几个月创意Processing实验
- Django框架下Cisco IOx平台实战开发案例源码解析
- 在Linux环境下配置Java版VTK开发环境
- 29街网上城市公司网站系统v1.0：企业建站全面解决方案
- WordPress CMB2插件的Suggest字段类型使用教程
- TCP协议实现的Java桌面聊天客户端应用
- ANR-WatchDog: 检测Android应用无响应并报告异常
