没有合适的资源?快使用搜索试试~ 我知道了~
首页推导系统可达性分析:应用到带引用调用的布尔程序
推导系统可达性分析:应用到带引用调用的布尔程序
0 下载量 190 浏览量
更新于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),这对于分析程序的终止行为和错误检测非常有用。 对于实际应用而言,这篇研究有助于开发者更好地理解和控制带转换的程序行为,尤其是在处理那些涉及复杂数据结构和状态管理的布尔程序时。通过这些新颖的分析方法,研究人员和工程师可以设计更有效的静态分析工具,用于检测潜在的问题并优化代码性能。因此,本文不仅深化了理论基础,也提供了实用的工程实践指导。
资源详情
资源推荐
![](https://csdnimg.cn/release/download_crawler_static/15168265/bg3.jpg)
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页未读,继续阅读
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
weixin_38626943
- 粉丝: 5
- 资源: 935
上传资源 快速赚钱
我的内容管理 展开
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
最新资源
- 解决Eclipse配置与导入Java工程常见问题
- 真空发生器:工作原理与抽吸性能分析
- 爱立信RBS6201开站流程详解
- 电脑开机声音解析:故障诊断指南
- JAVA实现贪吃蛇游戏
- 模糊神经网络实现与自学习能力探索
- PID型模糊神经网络控制器设计与学习算法
- 模糊神经网络在自适应PID控制器中的应用
- C++实现的学生成绩管理系统设计
- 802.1D STP 实现与优化:二层交换机中的生成树协议
- 解决Windows无法完成SD卡格式化的九种方法
- 软件测试方法:Beta与Alpha测试详解
- 软件测试周期详解:从需求分析到维护测试
- CMMI模型详解:软件企业能力提升的关键
- 移动Web开发框架选择:jQueryMobile、jQTouch、SenchaTouch对比
- Java程序设计试题与复习指南
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)