行为时序逻辑

行为时序图 (TLA) 是由 Leslie Lamport 开发的一种逻辑，它结合了时间逻辑和动作逻辑。它用于描述并发和分布式系统的行为。 它是规范语言 TLA+ 的底层逻辑。

动作时序逻辑中的语句的形式为 [ A ] t {displaystyle [A]_{t}} ，其中 A 是一个动作，t 包含出现在 A 中的变量的子集。一个动作是一个表达式 包含素数和非素数变量，例如 x + x ′ ∗ y = y ′ {displaystyle x+x’*y=y’} 。 非启动变量的含义是该状态下变量的值。 primed variables 的意思是变量在下一个状态下的值。

上面的表达式表示今天x 的值加上明天x 的值乘以今天y 的值，等于明天y 的值。

[ A ] t {displaystyle [A]_{t}} 的意思是要么A现在有效，要么出现在t中的变量不变。 这允许出现断断续续的步骤，其中没有任何程序变量改变它们的值。