基于行为时序逻辑系统性质的发展效果

　　1 引言
　　行为时序逻辑（TLA：Temporal Logic of Actions）的主要贡献在于两个方面：一是在时序逻辑（TL）中引入“行为（Action）”，用以联接系统的前后两个状态；二是提出“顿步（Stuttering Step）”，允许系统在某一步的下一状态保持与前一状态相同。实际上，顿步就是行为的一种特殊形式。因此行为在TLA中作用应该是至关重要的。本文将主要从行为的视角，重新审视行为时序逻辑，深入探讨行为的性质，特别是行为活性和安全性与系统活性和安全性之间的关系，充分展现行为在行为时序逻辑中的重要地位。
　　2 行为的性质
　　我们研究行为性质的最终目的，当然是为了更好地揭示所要描述的系统的性质。提到系统的性质，一般是指系统运转（Behaviors）的性质。在探讨行为的性质之前，我们先给出运转（Behaviors）性质的定义。
　　运转的性质：设St和A分别是系统状态和行为的集合，一个（St，A）性质Φ就是一个无限状态序列（Behaviors）的集合：
　　。我们使用σ∈Φ或σ|=Φ来表示一个运转σ满足性质Φ。
　　对于有限状态序列
　　，我们记σ[..n]|=Φ，当且仅当若存在无限状态序列使得σ[..n]σ+n∈Φ。
　　以下我们讨论行为的性质。
　　行为活性：若行为A在某一状态s使能，则称A在状态s上是活的；若行为A在运转σ上的某一状态σi使能，则称行为A在σ上是活的。
　　行为的活性仅表示行为发生的可能性，它不能判断行为是否能真正发生。为了衡量这种可能性的大小，TLA从行为在运转上发生频次和使能频次的比例考虑，引入行为的公平性条件来保证行为的真实发生，从而保证系统的活性。
　　弱公平性（justice）：运转σ对行为A来说是弱公平的，当且仅当满足以下条件：如果对任意的m，在σm之后A总是使能的，则存在一些n≥m，使得An=A。
　　用TLA公式来描述弱公平性即为：
　　强公平性（compassion）：运转σ对行为A来说是强公平的，当且仅当满足以下条件：如果对任意的m，σm之后A有无限多次使能，则存在一些n≥m，使得An=A。
　　用TLA公式来描述强公平性即为：
　　另外，在弱公平性和强公平行的基础上，文献[4]对公平性进行了细分。
　　行为安全性：对任意的一个有限状态序列及系统的一个性质Φ，若行为A在状态σn使能，且满足ρ|=Φ则称行为A对性质Φ来说是安全的。此时我们称行为A是性质Φ的安全行为。
　　可持续性：对于运转σ上的任一状态s， 若行为A使能直到A发生，则称A在σ上是可持续的。
　　用TLA公式描述可持续性为：
　　可逆性：对于运转σ上的任一状态s， 若行为A使能，且行为A发生后，存在一个行为B在新状态使能，且B若发生系统又回到状态s，则称行为A在σ上是可逆的。
　　可逆性的形式化描述为：
　　3 行为之间的关系
　　引发关系：对于运转σ上的任一状态s， 若行为A使能而行为B不使能；当A发生后B在新状态使能，则称A和B在σ上有顺序关系，即B的使能以A的发生为前提。这一关系用TLA公式描述即为：
　　并发关系：对于运转σ上的任一个状态s， 若行为A和行为B都使能，且A发生后B在新状态仍使能，或B发生后A在新状态仍使能，则称A和B在σ上是并发关系。用TLA公式描述即为：
　　，或
　　竞争（互斥）关系：对于运转σ上的任一个状态s， 若行为A和行为B都使能，且A发生后B在新状态不使能，或B发生后A在新状态不使能，则称A和B在σ上是竞争关系。用TLA公式描述即为：
　　，或
　　互逆关系：对于运转σ上的任一状态s， 若行为A使能，且行为A发生后，存在一个行为B在新状态使能，且B若发生系统又回到状态s，则称行为A和B在σ上是互逆行为。若A和B是互逆的，则可以把B记为A-1或把A记为B-1。
　　4 行为与系统
　　系统的性质一般分为两种：安全性和活性。以下我们给出Alpern和Schneider 在1984年提出的安全性和活性定义。为了和上文提出的行为的安全性和活性相区别，我们称之为系统的安全性和活性。
　　定义1 一个性质Φ是系统的安全性质，当且仅当下面的条件成立：
　　σ|=Φ当且仅当对任意的n，存在σ+n使得σ[..n]σ+n |=Φ。
　　定义2 一个性质Φ是系统的活性性质，当且仅当任意的有限序列σ[..n]，存在σ+n使得σ[..n]σ+n |=Φ。
　　TLA在引入了行为这一概念之后，系统的一次运转σ在初始状态s0确定的情况下，其后的系统状态和性质完全决定于σ上可能发生的行为。从这个意义上我们可以说：在初始状态确定的情况下，系统的性质完全由后续行为决定。既然如此，本文提出行为视角下系统安全性和活性的定义。
　　定义3 一个性质Φ是系统的安全性质，当且仅当下面的条件成立：
　　当且仅当对任意的n，在σn都有性质Φ的安全行为是活的（使能的）。
　　定义4 一个性质Φ是系统的活性性质，当且仅当对任意的有限序列σ[..n]，在最后一个状态σn，都有性质Φ的安全行为是活的（使能的）。
　　在有了安全行为的定义之后，定义3和4给出的系统安全性和活性定义更加直观和容易理解。当然我们有必要证明定义1与3及定义2与4是分别等价的。这里我们给出定义1与3的等价性证明，定义2与4的等价性证明是类似的。
　　【证明】对照定义1和定义3，要证它们的等价性仅需证明“存在σ+n使得σ[..n]σ+n |=Φ”与“在σn有性质Φ的安全行为是活的（使能的）”等价。
　　先证必要性：
　　假设在σn有性质Φ的安全行为是活的（使能的），根据安全行为的定义，此行为发生后的有限序列满足ρ|=Φ；再由ρ|=Φ的含义：存在无限序列σ+n+1使得ρσ+n+1 |=Φ，显然此时对于来说，存在无限状态序列使得σ[..n]σ+n |=Φ。
　　再证充分性：
　　如果存在σ+n使得σ[..n]σ+n |=Φ ，显然，由安全行为的定义，在σn发生的行为An就是性质Φ的安全行为。证毕。
　　5 结束语
　　Lamport提出的行为时序逻辑（TLA）的主要贡献是在线性时序逻辑（LTL）中引入“行为（Action）”。然而前人在研究TLA时，很少对行为进行深入探讨和运用。特别是在研究基于TLA 所描述的系统性质，比如安全性与活性性质时，仍然沿用时序逻辑的方法，并没有利用所引入的行为这一重要概念，致使安全性和活性的定义依然晦涩难懂。本文通过对行为的深入研究，提出了安全行为的概念，并利用这一概念重新定义系统的安全性和活性，使得安全性和活性定义更加直观和容易理解，同时也为系统性质的证明提供新的思路。
　　参考文献
　　[1] Leslie Lamport. Specifying Systems[M]. Addison- Wesley Longman Publishing Co.， Inc. 2002.
　　[2] Stephan Merz. Modeling and Developing Systems Using TLA+[M]. Escuela de Verano， 2005. Vol.73， Iss.3 （June 1987）， pp207-244.
　　[3] Wolfgang Schreiner. The TLA Logic of Action I. http：//people/schreine.
　　[4] Juntao Li， Zhengyi Tang， Xiang Li， Description and Analysis of Fairness on Temporal Logic of Actions[C]， icnds， vol. 1， pp.41-44， 2009 International Conference on Networking and Digital Society， 2009.
　　[5] Leslie Lamport. The Temporal Logic of actions [M]. ACM Transactions on Programming Languages and Systems. 1994.5，16（3）：872-923.
　　[6] Bowen Alpern ， Fred B， Schneider. Defining Liveness， Cornell University， Ithaca， NY， 1984.
　　[7] ， der， Recognizing Safety and Liveness，TR 86-727， Computer Science Department， Cornell University， Jan 1986.
　　[8] ， t， Proving Liveness Properties of Concurrent Programs， ACM Transactions on Programming Languages and Systems 4， No.3， 1982.