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]对公平性进行了细分。
行为安[dylW.NEt专业提供写作毕业论文的服务，欢迎光临wwW. DYlw.NEt]全性：对任意的一个有限状态序列及系统的一个性质Φ，若行为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：//www.risc.uni-linz.ac.at/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] B.Alpern， F.B.Schneider， Recognizing Safety and Liveness，TR 86-727， Computer Science Department， Cornell University， Jan 1986.
[8] S.Owicki， L.Lamport， Proving Liveness Properties of Concurrent Programs， ACM Transactions on Programming Languages and Systems 4， No.3， 1982.
