![](https://csdnimg.cn/release/download_crawler_static/88745266/bg5.jpg)
A. Bouajjani
等人理论计算机科学电子笔记
175
(
2007
)
47
a∈Act.通过M(R)、Const(R)和Act(R),我们表示
在
R的重写规则中发生的控
制状态、过程常数和动作的集合。
一个(α
,
β)
-
wPRSR诱导出一个状态为对(p
,
t)的标号转移系统,使得p∈M
(R)是控制状态,t∈β是Const(R)上的过程项
.
转移关系→
R
是满足以下推理规则
的最小关系:
一
((
p
,
t1
)
<$
→
(
q
,
t2
))∈
R
一
(
p
,
t1
)→
R
(
q
,
t2
)
(p
,
t
)
→
a
(
q
,
t
)
一
(p
,
t1
<$t)→
R
(q
,
t2
<$t)
(p
,
t
)
→
a
(
q
,
t
)
一
(
p
,
t1
<$
t
)→
R
(
q
,
t2
<$t
)
我们以一种标准的方式将转换关系扩展到Act上的有限词的
∗
用→
R
表示→
R
的自反传递闭包。为了缩短我们的符号
我们用pt代替(p
,
t)。
一个(α
,
β)
-wPRS
(其中M(R)是单例)称为
(
α
,
β
)
-PRS
(进程重写系
统)
。在这样的系统中,我们从规则和状态中省略了单个控制状态
代替(S
,
G)-PRS、(S
,
G)-wPRS、(G
,
G)-PRS和(G
,
G)-wPRS,我
们分别使用更可读的名称
PAD
、
wPAD
、
PRS
和
wPRS
。让我们注意到,类
PAD
和
wPAD将无限状态系 统的 广泛已知模型作为
下推 过程
(PDA),
基本 并行过程
(BPP)和
过程代数
(PA)。PRS和wPRS类也
是
Petri
网
(PN)的子模型更多信息
关于(α
,
β)-wPRS和(α
,
β)-wPRS的表达性可以在[13,12]中找到。
给定wPRSR的状态pt,我们定义
P o
s
t
R
(pt
)
=
{
p
J
t
J
|
pt
→
a
R
p
J
t
J
for
s
o
m
e
a
}
P o
s
t
(pt
)
=
{
p
J
t
J
|
pt
→
R
p
J
t
J
}
后
向
(pt)和
前
向
(pt)集合称为
(向前和向后)可达性
R R
集
.
Post
R
(
pt
)和
Pre
R
(
pt
)被称为
1
步(向前和向后)
可达性
集 这些定义和符号可以以显而易见的方式扩展到状态集合。
2.3
佳能
PRS
规范
PRS R
是一组重写规则,其形式为:
一
X
1
X
2
... X
n
<$→ Y
1
(
1
)
一
X
1
X
2
... X
n
<$
→
Y
1
(
2
)
其中
n
,
m
≥
0
。式(
1
)和式(
2
)的规则称为
规则
和
规则
分别 用
R
ω
表示
R
的所有
ω-
规则的集合。 注意,集合
R
一
和R
′
不必像某些规则那样不相交(例如,X <$→Y)是两种类型。
设
α
,
β
∈ {
1
,
S
,
P
,
G
}是过程项的类一个规范的
PRS
被称为
规范的
一
(
α
,
β
)
-PRS
如果
R
的每个规则
t1
<$
→
t2
满足
t1
∈
α
和
t2
∈
β.
最后,
Canonic
PAD
代表
Canonic
(
S
,
G
)
-PRS
。
请注意,规范PRS不一定是PRS,因为我们允许使用0的规则