基于行为时序逻辑系统性质研究

【 摘 要 】 文章研究行为时序逻辑（TLA）中行为（Action）的性质及行为之间的关系，提出“行为活性”和“行为安全性”概念，从行为的视角重新给出系统活性和安全性的定义，使得安全性和活性定义更加直观和容易理解，并证明了新老定义的等价性。

【 关键词 】 行为时序逻辑；活性；安全性；安全行为 【 中图分类号 】 TP301.2

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在σ上是活的。……