一、Liveness Property

1、概念介紹

在系統的形式化驗證領域，活性屬性（Liveness Property）是一個至關重要的概念。與安全性質（Safety Property）側重于防止系統出現不良行為不同，活性屬性主要關注系統能否最終達成某些期望的目標或事件。

從定義上來說，活性屬性描述了系統在運行過程中，某些積極的、有益的事件最終必然會發生的特性。例如，在一個任務調度系統中，活性屬性可以是每個任務最終都能得到執行；在一個通信系統里，活性屬性可能意味著發送的消息最終會被接收。

活性屬性的核心在于“最終會發生”這一概念。它并不關心事件何時發生，也不關心在事件發生之前系統經歷了哪些中間狀態，只強調事件一定會在未來的某個時刻出現。這種特性使得活性屬性在描述系統的長期行為和目標達成方面具有獨特的價值。

以一個簡單的電梯控制系統為例，活性屬性可以表述為：“每一個樓層的電梯請求最終都會被響應”。在這個系統中，無論電梯當前處于何種狀態，是正在運行、停靠還是空閑，只要有新的樓