Parallel Transition System是什么？

谢邀。本文书接上回：Sequential Transition System是什么？，继续介绍并行系统的建模方法，我们要求并行系统间也应该包含有互相通信的机制，包括没有通信、同步的通信和异步的通信三种情形。

我们假设系统存在可线性化的性质，即，对于该并行系统的任意一次执行，我们可以有一组线性的并行系统的action，按照该序列执行可以得到相同的Effect。——这使得我们在interleaving各个系统的时候，action可以视作不可分的原子操作。有时候我们需要系统的中间状态也能精确地反应现实系统存在的可能性，这需要我们确认好action中包含操作的粒度。

1. Interleaving Of Transition Systems

Interleaving将相互独立的TS组合起来，得到的并行TS的状态是各个组成部分状态的笛卡尔积，action是各个组成部分action的并集。

该并行TS在描述并行的action操作时因为是完全autonomously，可以视作对各个独立TS component的action进行non-deterministic的选择并进行相应状态转移的过程，这被称作one-processor view。

即，我们Interleaving两个并行执行的独立操作α和β的effect，是令它们以arbitrary order执行的两种effect的并集，arbitrary order即non-deterministic choice。

2. Communication via Shared Variables：Interleaving of Program Graph

Interleaving of Transition Systems的问题在于对各个TS components的状态做笛卡尔积，然而当存在共享变量的时候，如下例所示，得到的并行TS的状态中会存在多个共享变量副本，它们可能存在不一致的情形。

所以直观的解决办法是在Parallel TS的状态中，我们只对独立的Loc做笛卡尔积，而对于状态中的变量选取各个PG Component中变量的并集。如下例所示，TS(PG1 ||| PG2)正确地体现了两个action执行顺序的不同得到的是Parallel TS上两种不同的状态，并且状态中的（共享）变量不存在不一致的情形。

回忆在上一小节中介绍的PG和TS(PG)定义的差别，PG的状态只包含有Loc而不包含Eval(Var)，

所以我们先对PG做Interleaving，这样只会对Loc做笛卡尔积，然后基于Interleaving后、作用于Vars并集的PGs得到TS of Interleaved PGs，该系统的状态不会盲目地对变量做笛卡尔积。

把Definition 2.21应用到2.15，对比它和Definition 2.18的定义，可以理解TS of Interleaved PG1 and PG2区别于Interleaving TS(PG1) and TS(PG2)。

3. Handshaking

Handshaking意味着并行的系统以同步地方式同时进行一组操作。

这里操作指communication只考虑控制层面的同步（action），而非数据（content）的同步。

于是更类似与Interleaving of TS的定义，我们还是直接在TS上做Interleaving得到Handshaking System。

区别在于我们区分Interleaving和handshaking两类的action，它们的规则如下。

4. Channel System

相比于Interleaving of autonomous TS没有同步、Handshaking只同步action，Channel System的表现能力更强。

当channel capacity为0时，系统类似于handshaking可以同步action操作；

当channel capacity＞0时，系统更类似于communication via shared variables，不过该系统以FIFO buffer进行数据的同步。

相比于shared variables如果连续多次写入而没有被及时读取，数据会丢失，channel capacity＞0时channel可以缓存数据，接收者以异步的方式按照FIFO的数据依次读取，不必担心数据丢失。并且当channel满时，会阻塞transmit操作。

跟先前PG的定义相比，只是扩充了action的定义，区分于之前普通的action、以及新增的channel communication action。

下面是communication actions发生transition的条件及effect。

当channel capacity为0时，系统是同步的数据传输，类似于handshaking；

当channel capacity ＞ 0时，系统是异步的数据传输。

有了CS的定义，下面我们来定义TS(CS)。

类似于PG和TS(PG)，TS(CS)的状态也应包含Loc、对变量和[新增的Channel]的Evaluation，我们用ζ表示evaluation of channel (as sequence)，以及更新ζ的表示方法。

定义一个统一的符号τ代表所有的communication action，于是我们得到TS(CS)的定义如下所示，用红框标出的是相较于TS(PG)新增的部分。

下面是状态转移的规则。

5. 总结

我们想对并行系统建模，抽象出并行系统的动作（与通信），以及在该动作下状态转移的规则，于是得到transition system，我们用形式语义（SOS）表示出操作的语义，可以用model checker检测该TS是否满足我们预期的属性（spec）。

本文介绍了4种formal的建模并行系统的方式。

Interleaving可以用non-deterministic choices表示自发、独立的System Components的actions的并行执行，能这样做的依据在于并行系统的可线性化；

然而在Conflicting variables存在的情况下，我们需要用TS of interleaved PG的建模方式避免shared variables的不一致；

Handshaking用于建模描述多个系统同步地执行相同的action操作；

TS of Channel System可以通用地表示出系统间同步和异步的消息传递，具有很强的表现能力。当Channel capacity为0时CS退化为handshaking。（全文完）

6. 参考文献

[1] Baier C, Katoen J P. Principles of model checking[M]. MIT press, 2008.