可重组模块化逻辑控制器的形式化分析

1.单个控制模块的属性分析

支持混流生产的可重组模块化逻辑控制器包括了基于Petri网的产品决策逻辑控制器以及加工设备逻辑控制器。首先，必须对单独的Petri网结构进行分析，然后给出支持混流生产的可重组模块化逻辑控制器的形式化分析结果。

定理5.1 一个状态机（N，M0）是活性的，当且仅当N是强连接的并且M0至少包括一个托肯。一个状态机是安全的，当且仅当M0至多包括一个托肯。一个活性的状态机（N，M0）是安全，当且仅当M0只有一个托肯[88]。

定理5.2 一个活性的状态机是可逆的[157]。

由上述定理5.1～5.2以及文献[110]中的引理2，可很容易的得知，本文构建的加工设备逻辑控制器是活性、安全和可逆的。由文献[110]的引理3，可知本文构建的产品决策逻辑控制器是活性、安全和可逆的。

2.操作时序条件(www.xing528.com)

虽然上述的定理保证了单个模块的活性，安全性和可逆性，但是某个模块不正确的内部变量条件将可能带来整个可重组模块化逻辑控制器的死锁（例如，操作B必须要在操作A完成之后才能进行，而操作A又必须在操作B完成之后才能进行将会导致死锁）。为了防止可能出现的系统死锁现象，引入操作时序条件的概念。

定义5.7（操作时序条件） 逻辑控制器的操作次序相互不冲突，则逻辑控制器满足操作时序条件。

定理5.3 模块化逻辑控制器是活性、安全和可逆的，当且仅当每个模块都是活性、安全和可逆的并且满足操作时序条件。

由文献[110]中的定理3可知，支持混流生产的可重组模块化逻辑控制器是活的，安全的和可逆的，当且仅当每个控制模块是活的，安全的和可逆的，并且满足操作时序条件。

由于支持混流生产的可重组模块化逻辑控制的每个控制模块的活性，安全性和可逆性都可以得到保证，所以整个控制器的控制逻辑只要检验操作时序条件就可以很容易得到验证。