![](https://csdnimg.cn/release/download_crawler_static/88749347/bg4.jpg)
A.F. Donaldson
等人理论计算机科学电子笔记
128
(
2005
)
161
对于每个变量
x
∈
X
,以及对于每个
d
∈
D
,(
x=d
)∈
AP
(这些命题指程序中变
量的值)。对于P中的每个通道
c
i
,设
cap
(
c
i
)表示
c
i
可以保存的最大消息
数,
len
(
c
i
)
表示
c
i
在给定时间保存的消息数,
next
(
c
i
)表示要从
c
i
读取的下
一个消息。 那么对于值d
1
,
.
,
dk
∈D,<mi
≤
m + n,0
≤
k
≤
cap(c
i
),且对任
意k-元组[
d1
,
.
,
dk
] ∈
Dk
,(
ci
= [
d1
,
.
,
d
k
])∈AP,(next(c
i
)= d
1
)∈AP和
(len(c
i
)= k)∈AP(这些命题涉及节目中频道的内容和长度)。
这里[d
1
,
.
,
d
k
]表示包含k个元素的先进先出缓冲器(我们使用[ ]表示空缓
冲器)。当消息写入通道时,它会添加到缓冲器的右侧。当从通道读取消息
时,它将从缓冲器的左侧移除,所有消息将向左移动一个位置。
程序P的执行由它的语句集决定。对于语句
g
i
→
u
i
,在保护
g
i
评估为真的任何
系统状态中,程序可以执行更新u
i
,导致转换到另一个系统状态。保护g
i
是原
子命题的布尔组合,涉及进程p
i
的变量,或通道的长度或下一个值。更新u
i
是
对过程
p
i
的局部变量和系统通道的赋值。更新
u
i
可以具有
skip
(不更新变量或
通道的值)、x
i
:=d(x
i
∈X
i
,
d∈D)的形式,或者可以涉及
静态
通道更新
(从固定通道
c j
读取或写入固定通道
c
j
)或
动态
通道更新。动态通道更新涉及
从通道c x i读取或向通道c
x
i
写入,其中x
i
∈X
i
是c变量。 我们使用符号read
(c
j
),
write
(
d
,
c
j
)(
m j
≤
m
+
n
,
d
∈
D
)表示静态读取和写入
通道c
,
j(并且类似地用于动态读/写)。更新也可以由同时执行的一系列更新
组成
请注意,一个表示为语句
序列的
模型(例如,用Promela规范语言编写的模
型[10])仍然可以用这些术语来考虑。如果k是与由进程p
i
执行的Promela模型
的 语 句 相 关 联 的 程 序 计 数 器 值 , 则 与 该 语 句 相 关 联 的 保 护 包 含 命 题
(pc
i
=k),其中pc
i
是表示进程p
i
的程序计数器的局部变量。
2.1
从并发程序中导出
Kripke
结构
为了推理并发程序P的形式语义,我们使用
Kripke
结构
[4]
。
定义
2.2
设P是具有原子命题AP的并发程序。对于P,AP上的
Kripke
结构
M
是四元组
M
=
(
S
,
R
,
L
,
s
0
)